38 |
38 |
39 declare split_if_asm [split del] |
39 declare split_if_asm [split del] |
40 declare lvar_def [simp] |
40 declare lvar_def [simp] |
41 |
41 |
42 ML {* |
42 ML {* |
43 fun inst1_tac s t st = case AList.lookup (op =) (rev (term_varnames (prop_of st))) s of |
43 local |
|
44 val ax_Skip = thm "ax_Skip"; |
|
45 val ax_StatRef = thm "ax_StatRef"; |
|
46 val ax_MethdN = thm "ax_MethdN"; |
|
47 val ax_Alloc = thm "ax_Alloc"; |
|
48 val ax_Alloc_Arr = thm "ax_Alloc_Arr"; |
|
49 val ax_SXAlloc_Normal = thm "ax_SXAlloc_Normal"; |
|
50 val ax_derivs_intros = funpow 7 tl (thms "ax_derivs.intros"); |
|
51 in |
|
52 |
|
53 fun inst1_tac s t st = |
|
54 case AList.lookup (op =) (rev (Term.add_varnames (prop_of st) [])) s of |
44 SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty; |
55 SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty; |
45 val ax_tac = REPEAT o rtac allI THEN' |
56 |
46 resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN":: |
57 val ax_tac = |
47 thm "ax_Alloc"::thm "ax_Alloc_Arr":: |
58 REPEAT o rtac allI THEN' |
48 thm "ax_SXAlloc_Normal":: |
59 resolve_tac (ax_Skip :: ax_StatRef :: ax_MethdN :: ax_Alloc :: |
49 funpow 7 tl (thms "ax_derivs.intros")) |
60 ax_Alloc_Arr :: ax_SXAlloc_Normal :: ax_derivs_intros); |
|
61 end; |
50 *} |
62 *} |
51 |
63 |
52 |
64 |
53 theorem ax_test: "tprg,({}::'a triple set)\<turnstile> |
65 theorem ax_test: "tprg,({}::'a triple set)\<turnstile> |
54 {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)} |
66 {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)} |