| |
| # C-Refinement Proofs |
| |
| These proofs are currently being updated |
| |
| ## Proof Dependencies |
| |
| These proofs depend on the Cogent Type-system proofs, and AutoCorres. |
| |
| ``` |
| file depends on |
| ├── Cogent_C_Heap_Auto.thy (Read_Table) |
| ├── Cogent_C_Val_Auto.thy (Value_Relation_Generation, Type_Relation_Generation) |
| ├── Cogent_Corres_Sanity_Check.thy |
| ├── Cogent_Corres_Shallow_C.thy (Deep_Embedding_Auto, Cogent_Corres, Corres_Tac, TypeProofGen, Tidy) |
| ├── Cogent_Corres.thy (Value_Relation) |
| ├── CogentHigherOrder.thy (TypeProofGen) |
| ├── Corres_Tac.thy (Cogent_Corres, Value_Relation_Generation) |
| ├── Deep_Embedding_Auto.thy (Specialised_Lemma, Cogent_C_Val_Auto, Cogent_C_Heap_Auto, Heap_Relation_Generation) |
| ├── Heap_Relation_Generation.thy (Read_Table) |
| ├── Read_Table.thy (Specialised_Lemma_Utils) |
| ├── SpecialisedLemmaTactic.thy (Cogent_Corres, Specialised_Lemma_Utils) |
| ├── Specialised_Lemma.thy (Read_Table, SpecialisedLemmaTactic) |
| ├── Specialised_Lemma_URecord.thy (Read_Table, SpecialisedLemmaTactic) |
| ├── Specialised_Lemma_USum.thy (Read_Table, SpecialisedLemmaTactic) |
| ├── Specialised_Lemma_Utils.thy (Utils) |
| ├── Tidy.thy |
| ├── Type_Args.thy |
| ├── Type_Relation_Generation.thy (Cogent_Corres, Read_Table) |
| ├── TypeProofGen.thy |
| ├── Utils.thy |
| ├── Value_Relation_Generation.thy (Cogent_Corres, Specialised_Lemma_Utils) |
| └── Value_Relation.thy (Type_Args) |
| ``` |
