| (* |
| * Copyright 2016, NICTA |
| * |
| * This software may be distributed and modified according to the terms of |
| * the GNU General Public License version 2. Note that NO WARRANTY is provided. |
| * See "LICENSE_GPLv2.txt" for details. |
| * |
| * @TAG(NICTA_GPL) |
| *) |
| |
| (* |
| * Slightly nontrivial testcase for C refinement. |
| * Program specification generated from: |
| * cogent -Od --fnormalisation=knf --flet-in-if pass_middle-size-example.cogent -gpass_middle-size-example |
| * cogent -Od --fnormalisation=knf --flet-in-if pass_middle-size-example.cogent --type-proof=Middle --fml-typing-tree |
| *) |
| |
| theory Middle_C |
| imports |
| "../Deep_Embedding_Auto" |
| "../Cogent_Corres" |
| "../Corres_Tac" |
| "../TypeProofGen" |
| "../Tidy" |
| begin |
| |
| definition |
| "abbreviatedType1 \<equiv> TRecord [(TRecord [(TRecord [(TPrim (Num U32), False), (TPrim (Num U32), False)] Writable, True), (TPrim Bool, False)] Writable, False), (TRecord [(TPrim (Num U32), False), (TPrim (Num U32), False)] Writable, False), (TPrim Bool, False), (TPrim (Num U32), False)] Unboxed" |
| |
| definition |
| "abbreviatedType2 \<equiv> TRecord [(TPrim (Num U32), False), (TPrim (Num U32), False)] Writable" |
| |
| definition |
| "abbreviatedType3 \<equiv> TRecord [(abbreviatedType2, True), (TPrim Bool, False)] Writable" |
| |
| definition |
| "abbreviatedType4 \<equiv> TRecord [(TRecord [(abbreviatedType2, False), (TPrim Bool, False)] Writable, False), (TPrim Bool, False)] Unboxed" |
| |
| definition |
| "abbreviatedType5 \<equiv> TRecord [(abbreviatedType2, False), (TPrim Bool, False)] Writable" |
| |
| lemmas abbreviated_type_defs = |
| abbreviatedType3_def |
| abbreviatedType5_def |
| abbreviatedType2_def |
| abbreviatedType4_def |
| abbreviatedType1_def |
| |
| definition |
| "foo_type \<equiv> ([], (TRecord [(abbreviatedType5, False), (TPrim Bool, False)] Unboxed, TRecord [(abbreviatedType3, False), (abbreviatedType2, False), (TPrim Bool, False), (TPrim (Num U32), False)] Unboxed))" |
| |
| definition |
| "foo \<equiv> Take (Var 0) 0 (Take (Var 1) 1 (Take (Var 2) 1 (If (Var 2) (Let (Put (Var 1) 1 (Var 2)) (Take (Var 0) 0 (Take (Var 0) 1 (Let (Lit (LU8 0)) (Let (Cast U32 (Var 0)) (Let (Put (Var 3) 1 (Var 0)) (Struct [abbreviatedType3, abbreviatedType2, TPrim Bool, TPrim (Num U32)] [Var 6, Var 0, Var 8, Var 3]))))))) (Let (Lit (LBool True)) (Let (Put (Var 2) 1 (Var 0)) (Take (Var 0) 0 (Let (Lit (LU8 0)) (Let (Cast U32 (Var 0)) (Let (Put (Var 2) 0 (Var 0)) (Let (Put (Var 4) 0 (Var 0)) (Take (Var 0) 0 (Take (Var 0) 1 (Let (Lit (LU8 0)) (Let (Cast U32 (Var 0)) (Let (Put (Var 3) 1 (Var 0)) (Struct [abbreviatedType3, abbreviatedType2, TPrim Bool, TPrim (Num U32)] [Var 6, Var 0, Var 15, Var 3]))))))))))))))))" |
| |
| ML {* |
| val Cogent_functions = ["foo"] |
| val Cogent_abstract_functions = [] |
| *} |
| |
| definition |
| "\<Xi> func_name' \<equiv> case func_name' of ''foo'' \<Rightarrow> foo_type" |
| |
| definition |
| "foo_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some abbreviatedType5, Some (TRecord [(abbreviatedType5, True), (TPrim Bool, False)] Unboxed)] (TyTrSplit (Cons None (Cons (Some TSK_L) (Cons None []))) [] TyTrLeaf [Some (TPrim Bool), Some (TRecord [(abbreviatedType5, True), (TPrim Bool, True)] Unboxed)] (TyTrSplit (Cons None (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 2 None) [])))) [] TyTrLeaf [Some (TPrim Bool), Some (TRecord [(abbreviatedType2, False), (TPrim Bool, True)] Writable)] (TyTrSplit (append (replicate 2 None) (Cons (Some TSK_S) (append (replicate 4 None) []))) [] TyTrLeaf [] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons (Some TSK_S) (append (replicate 4 None) [])))) [] (TyTrSplit (Cons None (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 4 None) [])))) [] TyTrLeaf [Some abbreviatedType5] (TyTrSplit (Cons (Some TSK_L) (append (replicate 7 None) [])) [] TyTrLeaf [Some abbreviatedType2, Some abbreviatedType3] (TyTrSplit (Cons (Some TSK_L) (append (replicate 9 None) [])) [] TyTrLeaf [Some (TPrim (Num U32)), Some (TRecord [(TPrim (Num U32), False), (TPrim (Num U32), True)] Writable)] (TyTrSplit (append (replicate 12 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 12 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 10 None) [])))) [] TyTrLeaf [Some abbreviatedType2] TyTrLeaf)))))) [] (TyTrSplit (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 4 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 5 None) [])))) [] TyTrLeaf [Some abbreviatedType5] (TyTrSplit (Cons (Some TSK_L) (append (replicate 8 None) [])) [] TyTrLeaf [Some abbreviatedType2, Some abbreviatedType3] (TyTrSplit (append (replicate 11 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 11 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 10 None) [])))) [] TyTrLeaf [Some abbreviatedType2] (TyTrSplit (Cons (Some TSK_L) (append (replicate 3 None) (Cons (Some TSK_L) (append (replicate 9 None) [])))) [] TyTrLeaf [Some abbreviatedType5] (TyTrSplit (Cons (Some TSK_L) (append (replicate 14 None) [])) [] TyTrLeaf [Some abbreviatedType2, Some abbreviatedType3] (TyTrSplit (Cons (Some TSK_L) (append (replicate 16 None) [])) [] TyTrLeaf [Some (TPrim (Num U32)), Some (TRecord [(TPrim (Num U32), False), (TPrim (Num U32), True)] Writable)] (TyTrSplit (append (replicate 19 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 19 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 17 None) [])))) [] TyTrLeaf [Some abbreviatedType2] TyTrLeaf))))))))))))))))" |
| |
| ML {* open TTyping_Tactics *} |
| |
| ML_quiet {* |
| val typing_helper_1_script : tac list = [ |
| (RTac @{thm kind_tprim}) |
| ] *} |
| |
| |
| lemma typing_helper_1[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U32)) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_1_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_2_script : tac list = [ |
| (RTac @{thm kind_trec}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_1}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_1}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_2[unfolded abbreviated_type_defs] : |
| "kinding [] abbreviatedType2 {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_2_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_3_script : tac list = [ |
| (RTac @{thm kind_tprim}) |
| ] *} |
| |
| |
| lemma typing_helper_3[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim Bool) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_3_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_4_script : tac list = [ |
| (RTac @{thm kind_trec}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_2}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_3}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_4[unfolded abbreviated_type_defs] : |
| "kinding [] abbreviatedType5 {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_4_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_5_script : tac list = [ |
| (RTac @{thm kind_trec[where k = "{E}"]}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_4}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_3}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_5[unfolded abbreviated_type_defs] : |
| "kinding [] (TRecord [(abbreviatedType5, False), (TPrim Bool, False)] Unboxed) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_5_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_6_script : tac list = [ |
| (RTac @{thm kind_tprim}) |
| ] *} |
| |
| |
| lemma typing_helper_6[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim Bool) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_6_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_7_script : tac list = [ |
| (RTac @{thm kind_trec[where k = "{E,S,D}"]}), |
| (RTac @{thm kind_record_cons2}), |
| (RTac @{thm typing_helper_4}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_6}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_7[unfolded abbreviated_type_defs] : |
| "kinding [] (TRecord [(abbreviatedType5, True), (TPrim Bool, False)] Unboxed) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_7_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_8_script : tac list = [ |
| (RTac @{thm kind_trec[where k = "{E,S,D}"]}), |
| (RTac @{thm kind_record_cons2}), |
| (RTac @{thm typing_helper_4}), |
| (RTac @{thm kind_record_cons2}), |
| (RTac @{thm typing_helper_6}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_8[unfolded abbreviated_type_defs] : |
| "kinding [] (TRecord [(abbreviatedType5, True), (TPrim Bool, True)] Unboxed) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_8_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_9_script : tac list = [ |
| (RTac @{thm kind_trec[where k = "{E}"]}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_2}), |
| (RTac @{thm kind_record_cons2}), |
| (RTac @{thm typing_helper_6}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_9[unfolded abbreviated_type_defs] : |
| "kinding [] (TRecord [(abbreviatedType2, False), (TPrim Bool, True)] Writable) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_9_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_10_script : tac list = [ |
| (RTac @{thm kind_trec[where k = "{E}"]}), |
| (RTac @{thm kind_record_cons2}), |
| (RTac @{thm typing_helper_2}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_3}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_10[unfolded abbreviated_type_defs] : |
| "kinding [] abbreviatedType3 {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_10_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_11_script : tac list = [ |
| (RTac @{thm kind_tprim[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_11[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U32)) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_11_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_12_script : tac list = [ |
| (RTac @{thm kind_trec[where k = "{E}"]}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_1}), |
| (RTac @{thm kind_record_cons2}), |
| (RTac @{thm typing_helper_11}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_12[unfolded abbreviated_type_defs] : |
| "kinding [] (TRecord [(TPrim (Num U32), False), (TPrim (Num U32), True)] Writable) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_12_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val typing_helper_13_script : tac list = [ |
| (RTac @{thm kind_tprim[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_13[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U8)) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_13_script |> EVERY *}) |
| done |
| |
| ML_quiet {* |
| val foo_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_4})], |
| KindingTacs [(RTac @{thm typing_helper_7})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_4})], |
| KindingTacs [(RTac @{thm typing_helper_6})], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_6})], |
| KindingTacs [(RTac @{thm typing_helper_6})], |
| KindingTacs [(RTac @{thm typing_helper_9})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_6})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_4})], |
| TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (7,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_9})]),(2,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_6})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_9}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_6}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_6}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| KindingTacs [(RTac @{thm typing_helper_11})], |
| KindingTacs [(RTac @{thm typing_helper_12})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_11})], |
| KindingTacs [(RTac @{thm typing_helper_13})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_11})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_13}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (14,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_11})]),(3,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_12})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_12}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_11}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_11}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_6})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_6}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_4})], |
| TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (8,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_6})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_9})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_9}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_6}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_6}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| KindingTacs [(RTac @{thm typing_helper_13})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_11})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_13}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (13,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_11})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_2})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_2}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_11}),(RTac @{thm disjI1}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_11}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_4})], |
| TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (14,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_2})]),(4,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_10})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_2}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_2}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| KindingTacs [(RTac @{thm typing_helper_11})], |
| KindingTacs [(RTac @{thm typing_helper_12})], |
| TypingTacs [], |
| KindingTacs [(RTac @{thm typing_helper_11})], |
| KindingTacs [(RTac @{thm typing_helper_13})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_11})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_13}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_2})], |
| TypingTacs [(RTac @{thm typing_put'}),(SplitsTac (21,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_11})]),(3,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_12})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_12}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[@{thm Product_Type.prod.inject}])),(RTac @{thm typing_helper_11}),(RTac @{thm disjI2[where Q = "True"]}),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_11}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| TypingTacs [] |
| ] *} |
| |
| |
| ML_quiet {* |
| val foo_ttyping_details_future = get_all_typing_details_future @{context} "foo" |
| foo_typecorrect_script*} |
| |
| lemma foo_typecorrect : |
| "\<Xi>, fst foo_type, (foo_typetree, [Some (fst (snd foo_type))]) T\<turnstile> foo : snd (snd foo_type)" |
| apply (tactic {* resolve_future_typecorrect @{context} foo_ttyping_details_future *}) |
| done |
| |
| ML_quiet {* |
| val (_, foo_typing_tree, foo_typing_bucket) |
| = Future.join foo_ttyping_details_future |
| *} |
| |
| |
| |
| (* C semantics, generated by C parser *) |
| new_C_include_dir "../../cogent/tests" |
| install_C_file "pass_middle-size-example.c" |
| |
| autocorres [ts_rules=nondet, no_opt, gen_word_heaps, skip_word_abs] "pass_middle-size-example.c" |
| |
| instantiation bool_t_C :: cogent_C_val |
| begin |
| definition type_rel_bool_t_C_def: |
| "type_rel typ (_ :: bool_t_C itself) \<equiv> (typ = RPrim Bool)" |
| |
| definition val_rel_bool_t_C_def: |
| "val_rel uv (x :: bool_t_C) \<equiv> (boolean_C x = 0 \<or> boolean_C x = 1) \<and> |
| uv = UPrim (LBool (boolean_C x \<noteq> 0))" |
| instance .. |
| end |
| |
| (* Relation between Cogent and C data *) |
| local_setup{* local_setup_val_rel_type_rel_put_them_in_buckets "pass_middle-size-example.c" *} |
| |
| (* Lemma bucket.*) |
| ML{* TypeRelSimp.get @{context} *} |
| ML{* ValRelSimp.get @{context} *} |
| |
| lemmas val_rel_simps[ValRelSimp] = val_rel_word val_rel_ptr_def val_rel_bool_t_C_def |
| lemmas type_rel_simps[TypeRelSimp] = type_rel_word type_rel_ptr_def type_rel_bool_t_C_def |
| |
| class cogent_C_heap = cogent_C_val + |
| fixes is_valid :: "lifted_globals \<Rightarrow> 'a ptr \<Rightarrow> bool" |
| fixes heap :: "lifted_globals \<Rightarrow> 'a ptr \<Rightarrow> 'a" |
| fixes heap_update :: "(('a ptr \<Rightarrow> 'a) \<Rightarrow> 'a ptr \<Rightarrow> 'a) \<Rightarrow> lifted_globals \<Rightarrow> lifted_globals" |
| |
| local_setup{* local_setup_instantiate_cogent_C_heaps_store_them_in_buckets "pass_middle-size-example.c"*} |
| ML{* HeapSimp.get @{context}; IsValidSimp.get @{context} *} |
| |
| locale middle_cogent = "pass_middle-size-example" + update_sem_init |
| begin |
| |
| (* Relation between program heaps *) |
| definition |
| heap_rel_ptr :: |
| "(funtyp, abstyp, ptrtyp) store \<Rightarrow> lifted_globals \<Rightarrow> |
| ('a :: cogent_C_heap) ptr \<Rightarrow> bool" |
| where |
| "heap_rel_ptr \<sigma> h p \<equiv> |
| (\<forall>uv. |
| \<sigma> (ptr_val p) = Some uv \<longrightarrow> |
| type_rel (uval_repr uv) TYPE('a) \<longrightarrow> |
| is_valid h p \<and> val_rel uv (heap h p))" |
| |
| lemma heap_rel_ptr_meta: |
| "heap_rel_ptr = heap_rel_meta is_valid heap" |
| by (simp add: heap_rel_ptr_def[abs_def] heap_rel_meta_def[abs_def]) |
| |
| local_setup{* local_setup_heap_rel "pass_middle-size-example.c" *} |
| print_theorems |
| |
| definition state_rel :: "((funtyp, abstyp, ptrtyp) store \<times> lifted_globals) set" |
| where |
| "state_rel = {(\<sigma>, h). heap_rel \<sigma> h}" |
| |
| local_setup{* local_setup_take_put_member_case_esac_specialised_lemmas "pass_middle-size-example.c" *} |
| print_theorems |
| |
| (* Lemma buckets are generated in the above local_setup.*) |
| ML{* TakeBoxed.get @{context} *} |
| ML{* TakeUnboxed.get @{context} *} |
| ML{* PutBoxed.get @{context} *} |
| ML{* LetPutBoxed.get @{context} *} |
| ML{* MemberBoxed.get @{context} *} |
| ML{* Case.get @{context} *} |
| ML{* MemberReadOnly.get @{context} *} |
| |
| (* The set of thms the automation did not manage to prove.*) |
| ML{* Unborn_Thms.get @{context} *} |
| |
| (* You can add new proofs using attributes.*) |
| declare TrueI[MemberReadOnly] |
| (* MemberBoxed is now augmented with True.*) |
| ML{* MemberReadOnly.get @{context} *} |
| declare TrueI[MemberReadOnly del] |
| |
| |
| (* Preprocess AutoCorres output *) |
| local_setup {* tidy_C_fun_def' "foo" *} |
| thm foo'_def foo'_def' |
| |
| (* Defined late because it relies on bool_t_C *) |
| lemmas corres_if = corres_if_base[where bool_val' = boolean_C, |
| OF _ _ val_rel_bool_t_C_def[THEN meta_eq_to_obj_eq, THEN iffD1]] |
| |
| (* Defined late because it relies on LET_TRUE *) |
| lemmas corres_nested_let = corres_nested_let_base[OF LET_TRUE_def] |
| |
| (* Corres tactic *) |
| lemmas list_to_map_simps = list_to_map_more[where f=Var] list_to_map_singleton[where f=Var] |
| |
| (* Proof using corres_tac *) |
| lemma foo_corres: |
| "val_rel a a' \<Longrightarrow> corres state_rel foo (foo' a') \<xi> [a] \<Xi> [Some (fst (snd foo_type))] \<sigma> s" |
| apply (tactic {* corres_tac @{context} |
| (peel_two foo_typing_tree) |
| @{thms foo_def foo'_def' foo_type_def abbreviated_type_defs} [] [] |
| @{thm corres_if} [] @{thms } @{thms } [] |
| @{thm LETBANG_TRUE_def} @{thms list_to_map_simps} true *}) |
| done |
| end |
| end |
