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