1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory CToCRefine 12 13imports 14 "CSpec.Substitute" 15 "CLib.SimplRewrite" 16 "CLib.TypHeapLib" 17begin 18 19lemma spec_statefn_simulates_lookup_tree_Node: 20 "\<lbrakk> exec_statefn_simulates g UNIV UNIV v v'; 21 spec_statefn_simulates g (lookup_tree a f) (lookup_tree c f); 22 spec_statefn_simulates g (lookup_tree b f) (lookup_tree d f) \<rbrakk> 23 \<Longrightarrow> spec_statefn_simulates g (lookup_tree (Node n v a b) f) (lookup_tree (Node n v' c d) f)" 24 by (simp add: spec_statefn_simulates_def) 25 26lemma spec_statefn_simulates_lookup_tree_Leaf: 27 "spec_statefn_simulates g (lookup_tree Leaf f) (lookup_tree Leaf f')" 28 by (simp add: spec_statefn_simulates_def) 29 30ML {* 31fun mk_meta_eq_safe t = mk_meta_eq t 32 handle THM _ => t; 33 34val unfold_bodies = Simplifier.make_simproc @{context} "unfold constants named *_body" 35 {lhss = [@{term "v"}], 36 proc= fn _ => 37 (fn ctxt => (fn t => case head_of (Thm.term_of t) of 38 Const (s, _) => if String.isSuffix "_body" s 39 then try (Global_Theory.get_thm (Proof_Context.theory_of ctxt) #> mk_meta_eq_safe) (suffix "_def" s) 40 else NONE 41 | _ => NONE))} 42*} 43 44theorem spec_refine: 45 notes if_split[split del] 46 shows 47 "spec_statefn_simulates id (kernel_all_global_addresses.\<Gamma> symbol_table) 48 (kernel_all_substitute.\<Gamma> symbol_table domain)" 49 apply (simp add: kernel_all_global_addresses.\<Gamma>_def kernel_all_substitute.\<Gamma>_def) 50 apply (intro spec_statefn_simulates_lookup_tree_Node spec_statefn_simulates_lookup_tree_Leaf) 51 apply (tactic {* ALLGOALS (asm_simp_tac (put_simpset HOL_ss @{context} addsimps @{thms switch.simps fst_conv snd_conv} 52 addsimprocs [unfold_bodies] |> Splitter.del_split @{thm if_split})) 53 THEN ALLGOALS (TRY o resolve_tac @{context} @{thms exec_statefn_simulates_refl}) *}) 54 55 apply (tactic {* ALLGOALS (REPEAT_ALL_NEW (resolve_tac @{context} @{thms exec_statefn_simulates_comI 56 exec_statefn_simulates_additionals})) *}) 57 apply (unfold id_apply) 58 apply (tactic {* ALLGOALS (TRY o resolve_tac @{context} @{thms refl bij_id}) *}) 59 apply (tactic {* ALLGOALS (TRY o (resolve_tac @{context} @{thms subsetI} THEN' resolve_tac @{context} @{thms CollectI} 60 THEN' REPEAT_ALL_NEW (eresolve_tac @{context} @{thms IntE CollectE conjE exE h_t_valid_c_guard conjI} ORELSE' assume_tac @{context}))) *}) 61 (* 62 apply (tactic {* ALLGOALS (TRY o ((REPEAT_ALL_NEW (rtac @{thm c_guard_field}) THEN' etac @{thm h_t_valid_c_guard}) 63 THEN_ALL_NEW simp_tac @{simpset} 64 THEN_ALL_NEW simp_tac @{simpset} 65 THEN_ALL_NEW K no_tac)) *}) 66 *) 67 apply (rule bij_id[simplified id_def])+ 68 done (* Woo! *) 69 70end 71 72