--- a/src/HOL/Bali/AxExample.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/AxExample.thy Sat Jan 02 18:48:45 2016 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb
*)
-subsection {* Example of a proof based on the Bali axiomatic semantics *}
+subsection \<open>Example of a proof based on the Bali axiomatic semantics\<close>
theory AxExample
imports AxSem Example
@@ -40,7 +40,7 @@
declare split_if_asm [split del]
declare lvar_def [simp]
-ML {*
+ML \<open>
fun inst1_tac ctxt s t xs st =
(case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st
@@ -50,7 +50,7 @@
REPEAT o resolve_tac ctxt [allI] THEN'
resolve_tac ctxt
@{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)};
-*}
+\<close>
theorem ax_test: "tprg,({}::'a triple set)\<turnstile>
@@ -64,8 +64,8 @@
precondition. *)
apply (tactic "ax_tac @{context} 1" (* Try *))
defer
-apply (tactic {* inst1_tac @{context} "Q"
- "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *})
+apply (tactic \<open>inst1_tac @{context} "Q"
+ "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" []\<close>)
prefer 2
apply simp
apply (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
@@ -84,7 +84,7 @@
apply (tactic "ax_tac @{context} 1" (* AVar *))
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
+apply (tactic \<open>inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"]\<close>)
apply (simp del: avar_def2 peek_and_def2)
apply (tactic "ax_tac @{context} 1")
apply (tactic "ax_tac @{context} 1")
@@ -125,25 +125,25 @@
apply (tactic "ax_tac @{context} 1") (* Ass *)
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *})
+apply (tactic \<open>inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"]\<close>)
apply (rule allI)
-apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
+apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1\<close>)
apply (rule ax_derivs.Abrupt)
apply (simp (no_asm))
apply (tactic "ax_tac @{context} 1" (* FVar *))
apply (tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2", tactic "ax_tac @{context} 2")
apply (tactic "ax_tac @{context} 1")
-apply (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" [] *})
+apply (tactic \<open>inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" []\<close>)
apply fastforce
prefer 4
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
+apply (tactic \<open>inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"]\<close>)
apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
apply (tactic "ax_tac @{context} 1")
prefer 2
apply (rule ax_subst_Val_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *})
+apply (tactic \<open>inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"]\<close>)
apply (simp del: peek_and_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac @{context} 1")
apply (tactic "ax_tac @{context} 1")
@@ -162,7 +162,7 @@
apply (tactic "ax_tac @{context} 1")
defer
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *})
+apply (tactic \<open>inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"]\<close>)
apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac @{context} 1" (* NewC *))
apply (tactic "ax_tac @{context} 1" (* ax_Alloc *))
@@ -177,43 +177,43 @@
apply (rule ax_InitS)
apply force
apply (simp (no_asm))
-apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
+apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
apply (rule ax_Init_Skip_lemma)
-apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
+apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
apply (rule ax_InitS [THEN conseq1] (* init Base *))
apply force
apply (simp (no_asm))
apply (unfold arr_viewed_from_def)
apply (rule allI)
apply (rule_tac P' = "Normal P" and P = P for P in conseq1)
-apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
+apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
apply (tactic "ax_tac @{context} 1")
apply (tactic "ax_tac @{context} 1")
apply (rule_tac [2] ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *})
-apply (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
+apply (tactic \<open>inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"]\<close>)
+apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2\<close>)
apply (tactic "ax_tac @{context} 2" (* NewA *))
apply (tactic "ax_tac @{context} 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac @{context} 3")
-apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *})
-apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *})
+apply (tactic \<open>inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"]\<close>)
+apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 2\<close>)
apply (tactic "ax_tac @{context} 2")
apply (tactic "ax_tac @{context} 1" (* FVar *))
apply (tactic "ax_tac @{context} 2" (* StatRef *))
apply (rule ax_derivs.Done [THEN conseq1])
-apply (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" [] *})
+apply (tactic \<open>inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" []\<close>)
apply (clarsimp split del: split_if)
apply (frule atleast_free_weaken [THEN atleast_free_weaken])
apply (drule initedD)
apply (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
apply force
-apply (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
+apply (tactic \<open>simp_tac (@{context} delloop "split_all_tac") 1\<close>)
apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply (rule wf_tprg)
apply clarsimp
-apply (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" [] *})
+apply (tactic \<open>inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" []\<close>)
apply clarsimp
-apply (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" [] *})
+apply (tactic \<open>inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" []\<close>)
apply clarsimp
(* end init *)
apply (rule conseq1)
@@ -245,7 +245,7 @@
apply clarsimp
apply (tactic "ax_tac @{context} 1" (* If *))
apply (tactic
- {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *})
+ \<open>inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" []\<close>)
apply (tactic "ax_tac @{context} 1")
apply (rule conseq1)
apply (tactic "ax_tac @{context} 1")
@@ -266,7 +266,7 @@
apply (tactic "ax_tac @{context} 1")
prefer 2
apply (rule ax_subst_Var_allI)
-apply (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *})
+apply (tactic \<open>inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" []\<close>)
apply (rule allI)
apply (rule_tac P' = "Normal P" and P = P for P in conseq1)
prefer 2