--- a/src/HOL/Bali/AxCompl.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/AxCompl.thy Sat Jan 02 18:48:45 2016 +0100
@@ -2,18 +2,18 @@
Author: David von Oheimb and Norbert Schirmer
*)
-subsection {*
+subsection \<open>
Completeness proof for Axiomatic semantics of Java expressions and statements
-*}
+\<close>
theory AxCompl imports AxSem begin
-text {*
+text \<open>
design issues:
\begin{itemize}
\item proof structured by Most General Formulas (-> Thomas Kleymann)
\end{itemize}
-*}
+\<close>
@@ -170,10 +170,10 @@
done
lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"]
-text {* To derive the most general formula, we can always assume a normal
+text \<open>To derive the most general formula, we can always assume a normal
state in the precondition, since abrupt cases can be handled uniformally by
the abrupt rule.
-*}
+\<close>
lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>
G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
apply (unfold MGF_def)
@@ -191,8 +191,8 @@
apply clarsimp
done
-text {* Additionally to @{text MGFNormalI}, we also expand the definition of
-the most general formula here *}
+text \<open>Additionally to \<open>MGFNormalI\<close>, we also expand the definition of
+the most general formula here\<close>
lemma MGFn_NormalI:
"G,(A::state triple set)\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}t\<succ>
{\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
@@ -204,9 +204,9 @@
apply (clarsimp simp add: Let_def)
done
-text {* To derive the most general formula, we can restrict ourselves to
+text \<open>To derive the most general formula, we can restrict ourselves to
welltyped terms, since all others can be uniformally handled by the hazard
-rule. *}
+rule.\<close>
lemma MGFn_free_wt:
"(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T)
\<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>}
@@ -216,10 +216,10 @@
apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
done
-text {* To derive the most general formula, we can restrict ourselves to
+text \<open>To derive the most general formula, we can restrict ourselves to
welltyped terms and assume that the state in the precondition conforms to the
environment. All type violations can be uniformally handled by the hazard
-rule. *}
+rule.\<close>
lemma MGFn_free_wt_NormalConformI:
"(\<forall> T L C . \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T
\<longrightarrow> G,(A::state triple set)
@@ -240,10 +240,10 @@
apply blast
done
-text {* To derive the most general formula, we can restrict ourselves to
+text \<open>To derive the most general formula, we can restrict ourselves to
welltyped terms and assume that the state in the precondition conforms to the
environment and that the term is definetly assigned with respect to this state.
-All type violations can be uniformally handled by the hazard rule. *}
+All type violations can be uniformally handled by the hazard rule.\<close>
lemma MGFn_free_wt_da_NormalConformI:
"(\<forall> T L C B. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T
\<longrightarrow> G,(A::state triple set)
@@ -543,11 +543,11 @@
[where ?Env="\<lparr>prg=G, cls=C,lcl=L\<rparr>",simplified],auto)
-text {* To derive the most general formula for the loop statement, we need to
+text \<open>To derive the most general formula for the loop statement, we need to
come up with a proper loop invariant, which intuitively states that we are
currently inside the evaluation of the loop. To define such an invariant, we
unroll the loop in iterated evaluations of the expression and evaluations of
-the loop body. *}
+the loop body.\<close>
definition
unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times> state) set" where
@@ -719,7 +719,7 @@
show "Y' = \<diamondsuit> \<and> G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
proof -
from asm obtain v t where
- -- {* @{term "Z'"} gets instantiated with @{term "Norm s"} *}
+ \<comment> \<open>@{term "Z'"} gets instantiated with @{term "Norm s"}\<close>
unroll: "(Norm s, t) \<in> (unroll G l e c)\<^sup>*" and
eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" and
normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v" and
@@ -1037,13 +1037,13 @@
done
next
case (FVar accC statDeclC stat e fn)
- from MGFn_Init [OF hyp] and `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}` and wf
+ from MGFn_Init [OF hyp] and \<open>G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close> and wf
show ?case
by (rule MGFn_FVar)
next
case (AVar e1 e2)
- note mgf_e1 = `G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
- note mgf_e2 = `G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
+ note mgf_e1 = \<open>G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close>
+ note mgf_e2 = \<open>G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close>
show "G,A\<turnstile>{=:n} \<langle>e1.[e2]\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
apply (rule MGFn_NormalI)
apply (rule ax_derivs.AVar)
@@ -1186,8 +1186,8 @@
done
next
case (Call accC statT mode e mn pTs' ps)
- note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
- note mgf_ps = `G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}`
+ note mgf_e = \<open>G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close>
+ note mgf_ps = \<open>G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}\<close>
from mgf_methds mgf_e mgf_ps wf
show "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
by (rule MGFn_Call)
@@ -1198,7 +1198,7 @@
by simp
next
case (Body D c)
- note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
+ note mgf_c = \<open>G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close>
from wf MGFn_Init [OF hyp] mgf_c
show "G,A\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
by (rule MGFn_Body)
@@ -1266,8 +1266,8 @@
done
next
case (Loop l e c)
- note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
- note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
+ note mgf_e = \<open>G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close>
+ note mgf_c = \<open>G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close>
from mgf_e mgf_c wf
show "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
by (rule MGFn_Loop)
@@ -1303,8 +1303,8 @@
done
next
case (Fin c1 c2)
- note mgf_c1 = `G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
- note mgf_c2 = `G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
+ note mgf_c1 = \<open>G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close>
+ note mgf_c2 = \<open>G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close>
from wf mgf_c1 mgf_c2
show "G,A\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
by (rule MGFn_Fin)
@@ -1370,7 +1370,7 @@
apply -
apply (induct_tac "n")
apply (tactic "ALLGOALS (clarsimp_tac @{context})")
-apply (tactic {* dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1 *})
+apply (tactic \<open>dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1\<close>)
apply simp
apply (erule finite_imageI)
apply (simp add: MGF_asm ax_derivs_asm)
--- 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
--- a/src/HOL/Bali/AxSem.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/AxSem.thy Sat Jan 02 18:48:45 2016 +0100
@@ -2,12 +2,12 @@
Author: David von Oheimb
*)
-subsection {* Axiomatic semantics of Java expressions and statements
+subsection \<open>Axiomatic semantics of Java expressions and statements
(see also Eval.thy)
- *}
+\<close>
theory AxSem imports Evaln TypeSafe begin
-text {*
+text \<open>
design issues:
\begin{itemize}
\item a strong version of validity for triples with premises, namely one that
@@ -34,9 +34,9 @@
\item all triples in a derivation are of the same type (due to weak
polymorphism)
\end{itemize}
-*}
+\<close>
-type_synonym res = vals --{* result entry *}
+type_synonym res = vals \<comment>\<open>result entry\<close>
abbreviation (input)
Val where "Val x == In1 x"
@@ -57,7 +57,7 @@
"\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> CONST the_In2"
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
- --{* relation on result values, state and auxiliary variables *}
+ \<comment>\<open>relation on result values, state and auxiliary variables\<close>
type_synonym 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
(type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
@@ -464,8 +464,8 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
-setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
-setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
+setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
inductive
ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
@@ -496,7 +496,7 @@
| Abrupt: "G,A\<turnstile>{P\<leftarrow>(undefined3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
- --{* variables *}
+ \<comment>\<open>variables\<close>
| LVar: " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
| FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
@@ -506,7 +506,7 @@
| AVar: "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
\<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
- --{* expressions *}
+ \<comment>\<open>expressions\<close>
| NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
@@ -569,7 +569,7 @@
\<Longrightarrow>
G,A\<turnstile>{Normal P} Body D c-\<succ> {R}"
- --{* expression lists *}
+ \<comment>\<open>expression lists\<close>
| Nil: "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
@@ -577,7 +577,7 @@
\<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
- --{* statements *}
+ \<comment>\<open>statements\<close>
| Skip: "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
@@ -627,10 +627,10 @@
.init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
--- {* Some dummy rules for the intermediate terms @{text Callee},
-@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep
+\<comment> \<open>Some dummy rules for the intermediate terms \<open>Callee\<close>,
+\<open>InsInitE\<close>, \<open>InsInitV\<close>, \<open>FinA\<close> only used by the smallstep
semantics.
-*}
+\<close>
| InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
| InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
| Callee: " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
@@ -672,7 +672,7 @@
(* 37 subgoals *)
prefer 18 (* Methd *)
apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
-apply (tactic {* TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros})) *})
+apply (tactic \<open>TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros}))\<close>)
apply auto
done
@@ -692,9 +692,9 @@
apply (erule ax_derivs.induct)
(*42 subgoals*)
apply (tactic "ALLGOALS (strip_tac @{context})")
-apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dresolve_tac @{context} @{thms subset_singletonD},
+apply (tactic \<open>ALLGOALS(REPEAT o (EVERY'[dresolve_tac @{context} @{thms subset_singletonD},
eresolve_tac @{context} [disjE],
- fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
+ fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))\<close>)
apply (tactic "TRYALL (hyp_subst_tac @{context})")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)
@@ -704,8 +704,8 @@
apply (fast intro: ax_derivs.weaken)
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac @{context} 3 1", blast(* unused *))
(*37 subgoals*)
-apply (tactic {* TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros})
- THEN_ALL_NEW fast_tac @{context}) *})
+apply (tactic \<open>TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros})
+ THEN_ALL_NEW fast_tac @{context})\<close>)
(*1 subgoal*)
apply (clarsimp simp add: subset_mtriples_iff)
apply (rule ax_derivs.Methd)
@@ -719,16 +719,16 @@
subsubsection "rules derived from conseq"
-text {* In the following rules we often have to give some type annotations like:
+text \<open>In the following rules we often have to give some type annotations like:
@{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}.
Given only the term above without annotations, Isabelle would infer a more
general type were we could have
different types of auxiliary variables in the assumption set (@{term A}) and
in the triple itself (@{term P} and @{term Q}). But
-@{text "ax_derivs.Methd"} enforces the same type in the inductive definition of
+\<open>ax_derivs.Methd\<close> enforces the same type in the inductive definition of
the derivation. So we have to restrict the types to be able to apply the
rules.
-*}
+\<close>
lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};
\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
Q Y' s' Z)\<rbrakk>
@@ -738,7 +738,7 @@
apply blast
done
--- {* Nice variant, since it is so symmetric we might be able to memorise it. *}
+\<comment> \<open>Nice variant, since it is so symmetric we might be able to memorise it.\<close>
lemma conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; \<forall>s Y' s'.
(\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>
(\<forall>Y Z. P Y s Z \<longrightarrow> Q Y' s' Z)\<rbrakk>
@@ -1008,7 +1008,7 @@
apply (auto simp add: type_ok_def)
done
-ML {* ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *}
+ML \<open>ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt})\<close>
declare ax_Abrupts [intro!]
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
--- a/src/HOL/Bali/AxSound.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/AxSound.thy Sat Jan 02 18:48:45 2016 +0100
@@ -1,9 +1,9 @@
(* Title: HOL/Bali/AxSound.thy
Author: David von Oheimb and Norbert Schirmer
*)
-subsection {* Soundness proof for Axiomatic semantics of Java expressions and
+subsection \<open>Soundness proof for Axiomatic semantics of Java expressions and
statements
- *}
+\<close>
theory AxSound imports AxSem begin
@@ -19,13 +19,13 @@
\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
(\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))"
-text {* This definition differs from the ordinary @{text triple_valid_def}
+text \<open>This definition differs from the ordinary \<open>triple_valid_def\<close>
manly in the conclusion: We also ensures conformance of the result state. So
we don't have to apply the type soundness lemma all the time during
induction. This definition is only introduced for the soundness
proof of the axiomatic semantics, in the end we will conclude to
the ordinary definition.
-*}
+\<close>
definition
ax_valids2 :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
@@ -126,8 +126,8 @@
qed
next
case (Suc m)
- note hyp = `\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t`
- note prem = `\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t`
+ note hyp = \<open>\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>m\<Colon>t\<close>
+ note prem = \<open>\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t\<close>
show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}. G\<Turnstile>Suc m\<Colon>t"
proof -
{
@@ -350,9 +350,9 @@
by (simp add: ax_valids2_def triple_valid2_def2)
next
case (insert A t ts)
- note valid_t = `G,A|\<Turnstile>\<Colon>{t}`
+ note valid_t = \<open>G,A|\<Turnstile>\<Colon>{t}\<close>
moreover
- note valid_ts = `G,A|\<Turnstile>\<Colon>ts`
+ note valid_ts = \<open>G,A|\<Turnstile>\<Colon>ts\<close>
{
fix n assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
have "G\<Turnstile>n\<Colon>t" and "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
@@ -370,21 +370,21 @@
by (unfold ax_valids2_def) blast
next
case (asm ts A)
- from `ts \<subseteq> A`
+ from \<open>ts \<subseteq> A\<close>
show "G,A|\<Turnstile>\<Colon>ts"
by (auto simp add: ax_valids2_def triple_valid2_def)
next
case (weaken A ts' ts)
- note `G,A|\<Turnstile>\<Colon>ts'`
- moreover note `ts \<subseteq> ts'`
+ note \<open>G,A|\<Turnstile>\<Colon>ts'\<close>
+ moreover note \<open>ts \<subseteq> ts'\<close>
ultimately show "G,A|\<Turnstile>\<Colon>ts"
by (unfold ax_valids2_def triple_valid2_def) blast
next
case (conseq P A t Q)
- note con = `\<forall>Y s Z. P Y s Z \<longrightarrow>
+ note con = \<open>\<forall>Y s Z. P Y s Z \<longrightarrow>
(\<exists>P' Q'.
(G,A\<turnstile>{P'} t\<succ> {Q'} \<and> G,A|\<Turnstile>\<Colon>{ {P'} t\<succ> {Q'} }) \<and>
- (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))`
+ (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))\<close>
show "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
proof (rule validI)
fix n s0 L accC T C v s1 Y Z
@@ -469,8 +469,8 @@
qed
next
case (FVar A P statDeclC Q e stat fn R accC)
- note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }`
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }`
+ note valid_init = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }\<close>
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC,statDeclC,stat}e..fn=\<succ> {R} }"
proof (rule valid_var_NormalI)
fix n s0 L accC' T V vf s3 Y Z
@@ -564,7 +564,7 @@
qed
next
case (AVar A P e1 Q e2 R)
- note valid_e1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }`
+ note valid_e1 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }\<close>
have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
using AVar.hyps by simp
show "G,A|\<Turnstile>\<Colon>{ {Normal P} e1.[e2]=\<succ> {R} }"
@@ -628,7 +628,7 @@
qed
next
case (NewC A P C Q)
- note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init C. {Alloc G (CInst C) Q} }`
+ note valid_init = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .Init C. {Alloc G (CInst C) Q} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} NewC C-\<succ> {Q} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC T E v s2 Y Z
@@ -668,9 +668,9 @@
qed
next
case (NewA A P T Q e R)
- note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }`
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .;
- Alloc G (Arr T (the_Intg i)) R}}`
+ note valid_init = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }\<close>
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .;
+ Alloc G (Arr T (the_Intg i)) R}}\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} New T[e]-\<succ> {R} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC arrT E v s3 Y Z
@@ -741,9 +741,9 @@
qed
next
case (Cast A P e T Q)
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ>
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ>
{\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
- Q\<leftarrow>In1 v} }`
+ Q\<leftarrow>In1 v} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} Cast T e-\<succ> {Q} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC castT E v s2 Y Z
@@ -972,7 +972,7 @@
qed
next
case (Acc A P var Q)
- note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }`
+ note valid_var = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} Acc var-\<succ> {Q} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC T E v s1 Y Z
@@ -1008,7 +1008,7 @@
qed
next
case (Ass A P var Q e R)
- note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }`
+ note valid_var = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }\<close>
have valid_e: "\<And> vf.
G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In2 vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R} }"
using Ass.hyps by simp
@@ -1120,7 +1120,7 @@
qed
next
case (Cond A P e0 P' e1 e2 Q)
- note valid_e0 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }`
+ note valid_e0 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }\<close>
have valid_then_else:"\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q} }"
using Cond.hyps by simp
show "G,A|\<Turnstile>\<Colon>{ {Normal P} e0 ? e1 : e2-\<succ> {Q} }"
@@ -1210,7 +1210,7 @@
qed
next
case (Call A P e Q args R mode statT mn pTs' S accC')
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }`
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }\<close>
have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
using Call.hyps by simp
have valid_methd: "\<And> a vs invC declC l.
@@ -1594,14 +1594,14 @@
qed
next
case (Methd A P Q ms)
- note valid_body = `G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}`
+ note valid_body = \<open>G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}\<close>
show "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
by (rule Methd_sound) (rule Methd.hyps)
next
case (Body A P D Q c R)
- note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }`
- note valid_c = `G,A|\<Turnstile>\<Colon>{ {Q} .c.
- {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }`
+ note valid_init = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }\<close>
+ note valid_c = \<open>G,A|\<Turnstile>\<Colon>{ {Q} .c.
+ {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} Body D c-\<succ> {R} }"
proof (rule valid_expr_NormalI)
fix n s0 L accC T E v s4 Y Z
@@ -1692,7 +1692,7 @@
qed
next
case (Cons A P e Q es R)
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }`
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }\<close>
have valid_es: "\<And> v. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>\<lfloor>v\<rfloor>\<^sub>e} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>\<lfloor>(v # vs)\<rfloor>\<^sub>l} }"
using Cons.hyps by simp
show "G,A|\<Turnstile>\<Colon>{ {Normal P} e # es\<doteq>\<succ> {R} }"
@@ -1774,7 +1774,7 @@
qed
next
case (Expr A P e Q)
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }`
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Expr e. {Q} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s1 Y Z
@@ -1804,7 +1804,7 @@
qed
next
case (Lab A P c l Q)
- note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }`
+ note valid_c = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s2 Y Z
@@ -1841,8 +1841,8 @@
qed
next
case (Comp A P c1 Q c2 R)
- note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
- note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }`
+ note valid_c1 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }\<close>
+ note valid_c2 = \<open>G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1;; c2. {R} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s2 Y Z
@@ -1900,7 +1900,7 @@
qed
next
case (If A P e P' c1 c2 Q)
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }`
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }\<close>
have valid_then_else: "\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} .(if b then c1 else c2). {Q} }"
using If.hyps by simp
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .If(e) c1 Else c2. {Q} }"
@@ -1977,10 +1977,10 @@
qed
next
case (Loop A P e P' c l)
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }`
- note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)}
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }\<close>
+ note valid_c = \<open>G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)}
.c.
- {abupd (absorb (Cont l)) .; P} }`
+ {abupd (absorb (Cont l)) .; P} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {P} .l\<bullet> While(e) c. {P'\<leftarrow>=False\<down>=\<diamondsuit>} }"
proof (rule valid_stmtI)
fix n s0 L accC C s3 Y Z
@@ -1993,7 +1993,7 @@
assume P: "P Y s0 Z"
show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
proof -
- --{* From the given hypothesises @{text valid_e} and @{text valid_c}
+ \<comment>\<open>From the given hypothesises \<open>valid_e\<close> and \<open>valid_c\<close>
we can only reach the state after unfolding the loop once, i.e.
@{term "P \<diamondsuit> s2 Z"}, where @{term s2} is the state after executing
@{term c}. To gain validity of the further execution of while, to
@@ -2001,9 +2001,9 @@
a hypothesis about the subsequent unfoldings (the whole loop again),
too. We can achieve this, by performing induction on the
evaluation relation, with all
- the necessary preconditions to apply @{text valid_e} and
- @{text valid_c} in the goal.
- *}
+ the necessary preconditions to apply \<open>valid_e\<close> and
+ \<open>valid_c\<close> in the goal.
+\<close>
{
fix t s s' v
assume "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
@@ -2015,11 +2015,11 @@
(is "PROP ?Hyp n t s v s'")
proof (induct)
case (Loop s0' e' b n' s1' c' s2' l' s3' Y' T E)
- note while = `(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
+ note while = \<open>(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<close>
hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
- note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
- note P = `P Y' (Norm s0') Z`
- note conf_s0' = `Norm s0'\<Colon>\<preceq>(G, L)`
+ note valid_A = \<open>\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t\<close>
+ note P = \<open>P Y' (Norm s0') Z\<close>
+ note conf_s0' = \<open>Norm s0'\<Colon>\<preceq>(G, L)\<close>
have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
using Loop.prems eqs by simp
have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
@@ -2168,10 +2168,10 @@
qed
next
case (Abrupt abr s t' n' Y' T E)
- note t' = `t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
- note conf = `(Some abr, s)\<Colon>\<preceq>(G, L)`
- note P = `P Y' (Some abr, s) Z`
- note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
+ note t' = \<open>t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<close>
+ note conf = \<open>(Some abr, s)\<Colon>\<preceq>(G, L)\<close>
+ note P = \<open>P Y' (Some abr, s) Z\<close>
+ note valid_A = \<open>\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t\<close>
show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (undefined3 t') (Some abr, s) Z"
proof -
have eval_e:
@@ -2234,7 +2234,7 @@
qed
next
case (Throw A P e Q)
- note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }`
+ note valid_e = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Throw e. {Q} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC C s2 Y Z
@@ -2272,11 +2272,11 @@
qed
next
case (Try A P c1 Q C vn c2 R)
- note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }`
- note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn}
+ note valid_c1 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }\<close>
+ note valid_c2 = \<open>G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn}
.c2.
- {R} }`
- note Q_R = `(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R`
+ {R} }\<close>
+ note Q_R = \<open>(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R\<close>
show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Try c1 Catch(C vn) c2. {R} }"
proof (rule valid_stmt_NormalI)
fix n s0 L accC E s3 Y Z
@@ -2404,7 +2404,7 @@
qed
next
case (Fin A P c1 Q c2 R)
- note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
+ note valid_c1 = \<open>G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }\<close>
have valid_c2: "\<And> abr. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. abr = fst s) ;. abupd (\<lambda>x. None)}
.c2.
{abupd (abrupt_if (abr \<noteq> None) abr) .; R} }"
@@ -2501,11 +2501,11 @@
qed
next
case (Init C c A P Q R)
- note c = `the (class G C) = c`
+ note c = \<open>the (class G C) = c\<close>
note valid_super =
- `G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
+ \<open>G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
.(if C = Object then Skip else Init (super c)).
- {Q} }`
+ {Q} }\<close>
have valid_init:
"\<And> l. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty}
.init c.
--- a/src/HOL/Bali/Basis.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/Basis.thy Sat Jan 02 18:48:45 2016 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Basis.thy
Author: David von Oheimb
*)
-subsection {* Definitions extending HOL as logical basis of Bali *}
+subsection \<open>Definitions extending HOL as logical basis of Bali\<close>
theory Basis
imports Main "~~/src/HOL/Library/Old_Recdef"
@@ -9,10 +9,10 @@
subsubsection "misc"
-ML {* fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i) *}
+ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close>
declare split_if_asm [split] option.split [split] option.split_asm [split]
-setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
+setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
declare if_weak_cong [cong del] option.case_cong_weak [cong del]
declare length_Suc_conv [iff]
@@ -176,13 +176,13 @@
abbreviation the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"
where "the_In1r \<equiv> the_Inr \<circ> the_In1"
-ML {*
+ML \<open>
fun sum3_instantiate ctxt thm =
map (fn s =>
simplify (ctxt delsimps @{thms not_None_eq})
(Rule_Insts.read_instantiate ctxt [((("t", 0), Position.none), "In" ^ s ^ " x")] ["x"] thm))
["1l","2","3","1r"]
-*}
+\<close>
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
@@ -203,7 +203,7 @@
subsubsection "Special map update"
-text{* Deemed too special for theory Map. *}
+text\<open>Deemed too special for theory Map.\<close>
definition chg_map :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)"
where "chg_map f a m = (case m a of None \<Rightarrow> m | Some b \<Rightarrow> m(a\<mapsto>f b))"
@@ -255,7 +255,7 @@
definition lsplit :: "[['a, 'a list] \<Rightarrow> 'b, 'a list] \<Rightarrow> 'b"
where "lsplit = (\<lambda>f l. f (hd l) (tl l))"
-text {* list patterns -- extends pre-defined type "pttrn" used in abstractions *}
+text \<open>list patterns -- extends pre-defined type "pttrn" used in abstractions\<close>
syntax
"_lpttrn" :: "[pttrn, pttrn] \<Rightarrow> pttrn" ("_#/_" [901,900] 900)
translations
--- a/src/HOL/Bali/Conform.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/Conform.thy Sat Jan 02 18:48:45 2016 +0100
@@ -2,11 +2,11 @@
Author: David von Oheimb
*)
-subsection {* Conformance notions for the type soundness proof for Java *}
+subsection \<open>Conformance notions for the type soundness proof for Java\<close>
theory Conform imports State begin
-text {*
+text \<open>
design issues:
\begin{itemize}
\item lconf allows for (arbitrary) inaccessible values
@@ -14,7 +14,7 @@
objects on the heap are indeed existing classes. Yet this can be
inferred for all referenced objs.
\end{itemize}
-*}
+\<close>
type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
@@ -25,12 +25,12 @@
definition gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70) where
"s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj"
-text {* For the the proof of type soundness we will need the
+text \<open>For the the proof of type soundness we will need the
property that during execution, objects are not lost and moreover retain the
values of their tags. So the object store grows conservatively. Note that if
we considered garbage collection, we would have to restrict this property to
accessible objects.
-*}
+\<close>
lemma gext_objD:
"\<lbrakk>s\<le>|s'; globs s r = Some obj\<rbrakk>
@@ -250,7 +250,7 @@
subsubsection "weak value list conformance"
-text {* Only if the value is defined it has to conform to its type.
+text \<open>Only if the value is defined it has to conform to its type.
This is the contribution of the definite assignment analysis to
the notion of conformance. The definite assignment analysis ensures
that the program only attempts to access local variables that
@@ -258,7 +258,7 @@
So conformance must only ensure that the
defined values are of the right type, and not also that the value
is defined.
-*}
+\<close>
definition
--- a/src/HOL/Bali/Decl.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/Decl.thy Sat Jan 02 18:48:45 2016 +0100
@@ -1,15 +1,15 @@
(* Title: HOL/Bali/Decl.thy
Author: David von Oheimb and Norbert Schirmer
*)
-subsection {* Field, method, interface, and class declarations, whole Java programs
-*}
+subsection \<open>Field, method, interface, and class declarations, whole Java programs
+\<close>
theory Decl
imports Term Table
(** order is significant, because of clash for "var" **)
begin
-text {*
+text \<open>
improvements:
\begin{itemize}
\item clarification and correction of some aspects of the package/access concept
@@ -36,20 +36,20 @@
\item no main method
\end{itemize}
-*}
+\<close>
-subsection {* Modifier*}
+subsection \<open>Modifier\<close>
-subsubsection {* Access modifier *}
+subsubsection \<open>Access modifier\<close>
datatype acc_modi (* access modifier *)
= Private | Package | Protected | Public
-text {*
+text \<open>
We can define a linear order for the access modifiers. With Private yielding the
most restrictive access and public the most liberal access policy:
Private < Package < Protected < Public
-*}
+\<close>
instantiation acc_modi :: linorder
begin
@@ -70,14 +70,14 @@
fix x y z::acc_modi
show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)"
by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
- show "x \<le> x" -- reflexivity
+ show "x \<le> x" \<comment> reflexivity
by (auto simp add: le_acc_def)
{
- assume "x \<le> y" "y \<le> z" -- transitivity
+ assume "x \<le> y" "y \<le> z" \<comment> transitivity
then show "x \<le> z"
by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split)
next
- assume "x \<le> y" "y \<le> x" -- antisymmetry
+ assume "x \<le> y" "y \<le> x" \<comment> antisymmetry
moreover have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
by (auto simp add: less_acc_def split add: acc_modi.split)
ultimately show "x = y" by (unfold le_acc_def) iprover
@@ -137,11 +137,11 @@
using assms by (auto dest: acc_modi_Package_le)
-subsubsection {* Static Modifier *}
+subsubsection \<open>Static Modifier\<close>
type_synonym stat_modi = bool (* modifier: static *)
-subsection {* Declaration (base "class" for member,interface and class
- declarations *}
+subsection \<open>Declaration (base "class" for member,interface and class
+ declarations\<close>
record decl =
access :: acc_modi
@@ -150,7 +150,7 @@
(type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
(type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
-subsection {* Member (field or method)*}
+subsection \<open>Member (field or method)\<close>
record member = decl +
static :: stat_modi
@@ -158,7 +158,7 @@
(type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
(type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
-subsection {* Field *}
+subsection \<open>Field\<close>
record field = member +
type :: ty
@@ -173,7 +173,7 @@
translations
(type) "fdecl" <= (type) "vname \<times> field"
-subsection {* Method *}
+subsection \<open>Method\<close>
record mhead = member + (* method head (excluding signature) *)
pars ::"vname list" (* parameter names *)
@@ -219,9 +219,9 @@
lemma resT_mhead [simp]:"resT (mhead m) = resT m"
by (simp add: mhead_def)
-text {* To be able to talk uniformaly about field and method declarations we
+text \<open>To be able to talk uniformaly about field and method declarations we
introduce the notion of a member declaration (e.g. useful to define
-accessiblity ) *}
+accessiblity )\<close>
datatype memberdecl = fdecl fdecl | mdecl mdecl
@@ -293,16 +293,16 @@
by (simp add: is_method_def)
-subsection {* Interface *}
+subsection \<open>Interface\<close>
-record ibody = decl + --{* interface body *}
- imethods :: "(sig \<times> mhead) list" --{* method heads *}
+record ibody = decl + \<comment>\<open>interface body\<close>
+ imethods :: "(sig \<times> mhead) list" \<comment>\<open>method heads\<close>
-record iface = ibody + --{* interface *}
- isuperIfs:: "qtname list" --{* superinterface list *}
+record iface = ibody + \<comment>\<open>interface\<close>
+ isuperIfs:: "qtname list" \<comment>\<open>superinterface list\<close>
type_synonym
- idecl --{* interface declaration, cf. 9.1 *}
+ idecl \<comment>\<open>interface declaration, cf. 9.1\<close>
= "qtname \<times> iface"
translations
@@ -324,17 +324,17 @@
lemma imethods_ibody [simp]: "(imethods (ibody i)) = imethods i"
by (simp add: ibody_def)
-subsection {* Class *}
-record cbody = decl + --{* class body *}
+subsection \<open>Class\<close>
+record cbody = decl + \<comment>\<open>class body\<close>
cfields:: "fdecl list"
methods:: "mdecl list"
- init :: "stmt" --{* initializer *}
+ init :: "stmt" \<comment>\<open>initializer\<close>
-record "class" = cbody + --{* class *}
- super :: "qtname" --{* superclass *}
- superIfs:: "qtname list" --{* implemented interfaces *}
+record "class" = cbody + \<comment>\<open>class\<close>
+ super :: "qtname" \<comment>\<open>superclass\<close>
+ superIfs:: "qtname list" \<comment>\<open>implemented interfaces\<close>
type_synonym
- cdecl --{* class declaration, cf. 8.1 *}
+ cdecl \<comment>\<open>class declaration, cf. 8.1\<close>
= "qtname \<times> class"
translations
@@ -370,16 +370,16 @@
subsubsection "standard classes"
consts
- Object_mdecls :: "mdecl list" --{* methods of Object *}
- SXcpt_mdecls :: "mdecl list" --{* methods of SXcpts *}
+ Object_mdecls :: "mdecl list" \<comment>\<open>methods of Object\<close>
+ SXcpt_mdecls :: "mdecl list" \<comment>\<open>methods of SXcpts\<close>
definition
- ObjectC :: "cdecl" --{* declaration of root class *} where
+ ObjectC :: "cdecl" \<comment>\<open>declaration of root class\<close> where
"ObjectC = (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
init=Skip,super=undefined,superIfs=[]\<rparr>)"
definition
- SXcptC ::"xname \<Rightarrow> cdecl" --{* declarations of throwable classes *} where
+ SXcptC ::"xname \<Rightarrow> cdecl" \<comment>\<open>declarations of throwable classes\<close> where
"SXcptC xn = (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
init=Skip,
super=if xn = Throwable then Object
@@ -448,11 +448,11 @@
subsubsection "subinterface and subclass relation, in anticipation of TypeRel.thy"
definition
- subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subinterface *}
+ subint1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment>\<open>direct subinterface\<close>
where "subint1 G = {(I,J). \<exists>i\<in>iface G I: J\<in>set (isuperIfs i)}"
definition
- subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" --{* direct subclass *}
+ subcls1 :: "prog \<Rightarrow> (qtname \<times> qtname) set" \<comment>\<open>direct subclass\<close>
where "subcls1 G = {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
abbreviation
@@ -815,7 +815,7 @@
definition
imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
- --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
+ \<comment>\<open>methods of an interface, with overriding and inheritance, cf. 9.2\<close>
"imethds G I = iface_rec G I
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
(set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
--- a/src/HOL/Bali/DeclConcepts.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Sat Jan 02 18:48:45 2016 +0100
@@ -1,8 +1,8 @@
(* Title: HOL/Bali/DeclConcepts.thy
Author: Norbert Schirmer
*)
-subsection {* Advanced concepts on Java declarations like overriding, inheritance,
-dynamic method lookup*}
+subsection \<open>Advanced concepts on Java declarations like overriding, inheritance,
+dynamic method lookup\<close>
theory DeclConcepts imports TypeRel begin
@@ -16,10 +16,10 @@
| Some c \<Rightarrow> access c = Public)"
subsection "accessibility of types (cf. 6.6.1)"
-text {*
+text \<open>
Primitive types are always accessible, interfaces and classes are accessible
in their package or if they are defined public, an array type is accessible if
-its element type is accessible *}
+its element type is accessible\<close>
primrec
accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
@@ -71,16 +71,16 @@
by (simp add: is_acc_reftype_def)
subsection "accessibility of members"
-text {*
+text \<open>
The accessibility of members is more involved as the accessibility of types.
We have to distinguish several cases to model the different effects of
accessibility during inheritance, overriding and ordinary member access
-*}
+\<close>
-subsubsection {* Various technical conversion and selection functions *}
+subsubsection \<open>Various technical conversion and selection functions\<close>
-text {* overloaded selector @{text accmodi} to select the access modifier
-out of various HOL types *}
+text \<open>overloaded selector \<open>accmodi\<close> to select the access modifier
+out of various HOL types\<close>
class has_accmodi =
fixes accmodi:: "'a \<Rightarrow> acc_modi"
@@ -144,8 +144,8 @@
"accmodi (mdecl m) = accmodi m"
by (simp add: memberdecl_acc_modi_def)
-text {* overloaded selector @{text declclass} to select the declaring class
-out of various HOL types *}
+text \<open>overloaded selector \<open>declclass\<close> to select the declaring class
+out of various HOL types\<close>
class has_declclass =
fixes declclass:: "'a \<Rightarrow> qtname"
@@ -180,8 +180,8 @@
lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c"
by (simp add: pair_declclass_def)
-text {* overloaded selector @{text is_static} to select the static modifier
-out of various HOL types *}
+text \<open>overloaded selector \<open>is_static\<close> to select the static modifier
+out of various HOL types\<close>
class has_static =
fixes is_static :: "'a \<Rightarrow> bool"
@@ -246,32 +246,32 @@
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m"
by (cases m) (simp add: mhead_def member_is_static_simp)
--- {* some mnemotic selectors for various pairs *}
+\<comment> \<open>some mnemotic selectors for various pairs\<close>
definition
decliface :: "qtname \<times> 'a decl_scheme \<Rightarrow> qtname" where
- "decliface = fst" --{* get the interface component *}
+ "decliface = fst" \<comment>\<open>get the interface component\<close>
definition
mbr :: "qtname \<times> memberdecl \<Rightarrow> memberdecl" where
- "mbr = snd" --{* get the memberdecl component *}
+ "mbr = snd" \<comment>\<open>get the memberdecl component\<close>
definition
mthd :: "'b \<times> 'a \<Rightarrow> 'a" where
- "mthd = snd" --{* get the method component *}
- --{* also used for mdecl, mhead *}
+ "mthd = snd" \<comment>\<open>get the method component\<close>
+ \<comment>\<open>also used for mdecl, mhead\<close>
definition
fld :: "'b \<times> 'a decl_scheme \<Rightarrow> 'a decl_scheme" where
- "fld = snd" --{* get the field component *}
- --{* also used for @{text "((vname \<times> qtname)\<times> field)"} *}
+ "fld = snd" \<comment>\<open>get the field component\<close>
+ \<comment>\<open>also used for \<open>((vname \<times> qtname)\<times> field)\<close>\<close>
--- {* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
+\<comment> \<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close>
definition
fname:: "vname \<times> 'a \<Rightarrow> vname"
where "fname = fst"
- --{* also used for fdecl *}
+ \<comment>\<open>also used for fdecl\<close>
definition
declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname"
@@ -326,7 +326,7 @@
lemma declclassf_simp[simp]:"declclassf (n,c) = c"
by (simp add: declclassf_def)
- --{* some mnemotic selectors for @{text "(vname \<times> qtname)"} *}
+ \<comment>\<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close>
definition
fldname :: "vname \<times> qtname \<Rightarrow> vname"
@@ -345,8 +345,8 @@
lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f"
by (simp add: fldname_def fldclass_def)
-text {* Convert a qualified method declaration (qualified with its declaring
-class) to a qualified member declaration: @{text methdMembr} *}
+text \<open>Convert a qualified method declaration (qualified with its declaring
+class) to a qualified member declaration: \<open>methdMembr\<close>\<close>
definition
methdMembr :: "qtname \<times> mdecl \<Rightarrow> qtname \<times> memberdecl"
@@ -364,8 +364,8 @@
lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m"
by (cases m) (simp add: methdMembr_def)
-text {* Convert a qualified method (qualified with its declaring
-class) to a qualified member declaration: @{text method} *}
+text \<open>Convert a qualified method (qualified with its declaring
+class) to a qualified member declaration: \<open>method\<close>\<close>
definition
"method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
@@ -411,8 +411,8 @@
lemma memberid_fieldm_simp[simp]: "memberid (fieldm n f) = fid n"
by (simp add: fieldm_def)
-text {* Select the signature out of a qualified method declaration:
- @{text msig} *}
+text \<open>Select the signature out of a qualified method declaration:
+ \<open>msig\<close>\<close>
definition
msig :: "(qtname \<times> mdecl) \<Rightarrow> sig"
@@ -421,8 +421,8 @@
lemma msig_simp[simp]: "msig (c,(s,m)) = s"
by (simp add: msig_def)
-text {* Convert a qualified method (qualified with its declaring
-class) to a qualified method declaration: @{text qmdecl} *}
+text \<open>Convert a qualified method (qualified with its declaring
+class) to a qualified method declaration: \<open>qmdecl\<close>\<close>
definition
qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)"
@@ -451,8 +451,8 @@
"methdMembr (qmdecl sig old) = method sig old"
by (simp add: methdMembr_def qmdecl_def method_def)
-text {* overloaded selector @{text resTy} to select the result type
-out of various HOL types *}
+text \<open>overloaded selector \<open>resTy\<close> to select the result type
+out of various HOL types\<close>
class has_resTy =
fixes resTy:: "'a \<Rightarrow> ty"
@@ -507,8 +507,8 @@
by (cases m) (simp add: mthd_def )
subsubsection "inheritable-in"
-text {*
-@{text "G\<turnstile>m inheritable_in P"}: m can be inherited by
+text \<open>
+\<open>G\<turnstile>m inheritable_in P\<close>: m can be inherited by
classes in package P if:
\begin{itemize}
\item the declaration class of m is accessible in P and
@@ -517,7 +517,7 @@
class of m is also P. If the member m is declared with private access
it is not accessible for inheritance at all.
\end{itemize}
-*}
+\<close>
definition
inheritable_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60)
where
@@ -603,14 +603,14 @@
| Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C;
G\<turnstile>C \<prec>\<^sub>C1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S
\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C"
-text {* Note that in the case of an inherited member only the members of the
+text \<open>Note that in the case of an inherited member only the members of the
direct superclass are concerned. If a member of a superclass of the direct
superclass isn't inherited in the direct superclass (not member of the
direct superclass) than it can't be a member of the class. E.g. If a
member of a class A is defined with package access it isn't member of a
subclass S if S isn't in the same package as A. Any further subclasses
of S will not inherit the member, regardless if they are in the same
-package as A or not.*}
+package as A or not.\<close>
abbreviation
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -641,10 +641,10 @@
definition
member_in :: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" ("_ \<turnstile> _ member'_in _" [61,61,61] 60)
where "G\<turnstile>m member_in C = (\<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC)"
-text {* A member is in a class if it is member of the class or a superclass.
+text \<open>A member is in a class if it is member of the class or a superclass.
If a member is in a class we can select this member. This additional notion
is necessary since not all members are inherited to subclasses. So such
-members are not member-of the subclass but member-in the subclass.*}
+members are not member-of the subclass but member-in the subclass.\<close>
abbreviation
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -669,12 +669,12 @@
subsubsection "overriding"
-text {* Unfortunately the static notion of overriding (used during the
+text \<open>Unfortunately the static notion of overriding (used during the
typecheck of the compiler) and the dynamic notion of overriding (used during
execution in the JVM) are not exactly the same.
-*}
+\<close>
-text {* Static overriding (used during the typecheck of the compiler) *}
+text \<open>Static overriding (used during the typecheck of the compiler)\<close>
inductive
stat_overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
@@ -693,7 +693,7 @@
| Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S intr; G\<turnstile>intr overrides\<^sub>S old\<rbrakk>
\<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
-text {* Dynamic overriding (used during the typecheck of the compiler) *}
+text \<open>Dynamic overriding (used during the typecheck of the compiler)\<close>
inductive
overridesR :: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool"
@@ -799,15 +799,15 @@
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr
\<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr))
| Public \<Rightarrow> True)"
-text {*
+text \<open>
The subcondition of the @{term "Protected"} case:
@{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to:
@{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the
same the other condition @{term "(pid (declclass membr) = pid accclass)"}
holds anyway.
-*}
+\<close>
-text {* Like in case of overriding, the static and dynamic accessibility
+text \<open>Like in case of overriding, the static and dynamic accessibility
of members is not uniform.
\begin{itemize}
\item Statically the class/interface of the member must be accessible for the
@@ -819,7 +819,7 @@
\item Statically the member we want to access must be "member of" the class.
Dynamically it must only be "member in" the class.
\end{itemize}
-*}
+\<close>
inductive
accessible_fromR :: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool"
@@ -1403,7 +1403,7 @@
"imethds G I =
iface_rec G I (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
(set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
-text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
+text \<open>methods of an interface, with overriding and inheritance, cf. 9.2\<close>
definition
accimethds :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
@@ -1411,7 +1411,7 @@
(if G\<turnstile>Iface I accessible_in pack
then imethds G I
else (\<lambda> k. {}))"
-text {* only returns imethds if the interface is accessible *}
+text \<open>only returns imethds if the interface is accessible\<close>
definition
methd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
@@ -1422,25 +1422,25 @@
subcls_mthds
++
table_of (map (\<lambda>(s,m). (s,C,m)) (methods c)))"
-text {* @{term "methd G C"}: methods of a class C (statically visible from C),
+text \<open>@{term "methd G C"}: methods of a class C (statically visible from C),
with inheritance and hiding cf. 8.4.6;
- Overriding is captured by @{text dynmethd}.
+ Overriding is captured by \<open>dynmethd\<close>.
Every new method with the same signature coalesces the
- method of a superclass. *}
+ method of a superclass.\<close>
definition
accmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
"accmethd G S C =
filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) (methd G C)"
-text {* @{term "accmethd G S C"}: only those methods of @{term "methd G C"},
- accessible from S *}
+text \<open>@{term "accmethd G S C"}: only those methods of @{term "methd G C"},
+ accessible from S\<close>
-text {* Note the class component in the accessibility filter. The class where
+text \<open>Note the class component in the accessibility filter. The class where
method @{term m} is declared (@{term declC}) isn't necessarily accessible
from the current scope @{term S}. The method can be made accessible
through inheritance, too.
So we must test accessibility of method @{term m} of class @{term C}
- (not @{term "declclass m"}) *}
+ (not @{term "declclass m"})\<close>
definition
dynmethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
@@ -1461,13 +1461,13 @@
)
else None))"
-text {* @{term "dynmethd G statC dynC"}: dynamic method lookup of a reference
- with dynamic class @{term dynC} and static class @{term statC} *}
-text {* Note some kind of duality between @{term methd} and @{term dynmethd}
+text \<open>@{term "dynmethd G statC dynC"}: dynamic method lookup of a reference
+ with dynamic class @{term dynC} and static class @{term statC}\<close>
+text \<open>Note some kind of duality between @{term methd} and @{term dynmethd}
in the @{term class_rec} arguments. Whereas @{term methd} filters the
subclass methods (to get only the inherited ones), @{term dynmethd}
filters the new methods (to get only those methods which actually
- override the methods of the static class) *}
+ override the methods of the static class)\<close>
definition
dynimethd :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
@@ -1475,9 +1475,9 @@
(\<lambda>sig. if imethds G I sig \<noteq> {}
then methd G dynC sig
else dynmethd G Object dynC sig)"
-text {* @{term "dynimethd G I dynC"}: dynamic method lookup of a reference with
- dynamic class dynC and static interface type I *}
-text {*
+text \<open>@{term "dynimethd G I dynC"}: dynamic method lookup of a reference with
+ dynamic class dynC and static interface type I\<close>
+text \<open>
When calling an interface method, we must distinguish if the method signature
was defined in the interface or if it must be an Object method in the other
case. If it was an interface method we search the class hierarchy
@@ -1487,7 +1487,7 @@
effects like in case of dynmethd. The method will be inherited or
overridden in all classes from the first class implementing the interface
down to the actual dynamic class.
- *}
+\<close>
definition
dynlookup :: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
@@ -1497,19 +1497,19 @@
| IfaceT I \<Rightarrow> dynimethd G I dynC
| ClassT statC \<Rightarrow> dynmethd G statC dynC
| ArrayT ty \<Rightarrow> dynmethd G Object dynC)"
-text {* @{term "dynlookup G statT dynC"}: dynamic lookup of a method within the
+text \<open>@{term "dynlookup G statT dynC"}: dynamic lookup of a method within the
static reference type statT and the dynamic class dynC.
In a wellformd context statT will not be NullT and in case
- statT is an array type, dynC=Object *}
+ statT is an array type, dynC=Object\<close>
definition
fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
"fields G C =
class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
-text {* @{term "fields G C"}
+text \<open>@{term "fields G C"}
list of fields of a class, including all the fields of the superclasses
(private, inherited and hidden ones) not only the accessible ones
- (an instance of a object allocates all these fields *}
+ (an instance of a object allocates all these fields\<close>
definition
accfield :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> (vname, qtname \<times> field) table" where
@@ -1517,15 +1517,15 @@
(let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C))
in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
field_tab)"
-text {* @{term "accfield G C S"}: fields of a class @{term C} which are
+text \<open>@{term "accfield G C S"}: fields of a class @{term C} which are
accessible from scope of class
- @{term S} with inheritance and hiding, cf. 8.3 *}
-text {* note the class component in the accessibility filter (see also
+ @{term S} with inheritance and hiding, cf. 8.3\<close>
+text \<open>note the class component in the accessibility filter (see also
@{term methd}).
The class declaring field @{term f} (@{term declC}) isn't necessarily
accessible from scope @{term S}. The field can be made visible through
inheritance, too. So we must test accessibility of field @{term f} of class
- @{term C} (not @{term "declclass f"}) *}
+ @{term C} (not @{term "declclass f"})\<close>
definition
is_methd :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> bool"
--- a/src/HOL/Bali/DefiniteAssignment.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sat Jan 02 18:48:45 2016 +0100
@@ -1,8 +1,8 @@
-subsection {* Definite Assignment *}
+subsection \<open>Definite Assignment\<close>
theory DefiniteAssignment imports WellType begin
-text {* Definite Assignment Analysis (cf. 16)
+text \<open>Definite Assignment Analysis (cf. 16)
The definite assignment analysis approximates the sets of local
variables that will be assigned at a certain point of evaluation, and ensures
@@ -37,17 +37,17 @@
\item analysis of definite unassigned
\item special treatment of final fields
\end{itemize}
-*}
+\<close>
-subsubsection {* Correct nesting of jump statements *}
+subsubsection \<open>Correct nesting of jump statements\<close>
-text {* For definite assignment it becomes crucial, that jumps (break,
+text \<open>For definite assignment it becomes crucial, that jumps (break,
continue, return) are nested correctly i.e. a continue jump is nested in a
matching while statement, a break jump is nested in a proper label statement,
a class initialiser does not terminate abruptly with a return. With this we
can for example ensure that evaluation of an expression will never end up
with a jump, since no breaks, continues or returns are allowed in an
-expression. *}
+expression.\<close>
primrec jumpNestingOkS :: "jump set \<Rightarrow> stmt \<Rightarrow> bool"
where
@@ -59,8 +59,8 @@
| "jumpNestingOkS jmps (If(e) c1 Else c2) = (jumpNestingOkS jmps c1 \<and>
jumpNestingOkS jmps c2)"
| "jumpNestingOkS jmps (l\<bullet> While(e) c) = jumpNestingOkS ({Cont l} \<union> jmps) c"
---{* The label of the while loop only handles continue jumps. Breaks are only
- handled by @{term Lab} *}
+\<comment>\<open>The label of the while loop only handles continue jumps. Breaks are only
+ handled by @{term Lab}\<close>
| "jumpNestingOkS jmps (Jmp j) = (j \<in> jmps)"
| "jumpNestingOkS jmps (Throw e) = True"
| "jumpNestingOkS jmps (Try c1 Catch(C vn) c2) = (jumpNestingOkS jmps c1 \<and>
@@ -68,9 +68,9 @@
| "jumpNestingOkS jmps (c1 Finally c2) = (jumpNestingOkS jmps c1 \<and>
jumpNestingOkS jmps c2)"
| "jumpNestingOkS jmps (Init C) = True"
- --{* wellformedness of the program must enshure that for all initializers
- jumpNestingOkS {} holds *}
---{* Dummy analysis for intermediate smallstep term @{term FinA} *}
+ \<comment>\<open>wellformedness of the program must enshure that for all initializers
+ jumpNestingOkS {} holds\<close>
+\<comment>\<open>Dummy analysis for intermediate smallstep term @{term FinA}\<close>
| "jumpNestingOkS jmps (FinA a c) = False"
@@ -111,10 +111,10 @@
-subsubsection {* Calculation of assigned variables for boolean expressions*}
+subsubsection \<open>Calculation of assigned variables for boolean expressions\<close>
-subsection {* Very restricted calculation fallback calculation *}
+subsection \<open>Very restricted calculation fallback calculation\<close>
primrec the_LVar_name :: "var \<Rightarrow> lname"
where "the_LVar_name (LVar n) = n"
@@ -140,8 +140,8 @@
| "assignsE (b? e1 : e2) = (assignsE b) \<union> ((assignsE e1) \<inter> (assignsE e2))"
| "assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args))
= (assignsE objRef) \<union> (assignsEs args)"
--- {* Only dummy analysis for intermediate expressions
- @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
+\<comment> \<open>Only dummy analysis for intermediate expressions
+ @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee}\<close>
| "assignsE (Methd C sig) = {}"
| "assignsE (Body C s) = {}"
| "assignsE (InsInitE s e) = {}"
@@ -216,9 +216,9 @@
| False\<Rightarrow> (case (constVal e1) of
None \<Rightarrow> None
| Some v \<Rightarrow> constVal e2)))"
---{* Note that @{text "constVal (Cond b e1 e2)"} is stricter as it could be.
+\<comment>\<open>Note that \<open>constVal (Cond b e1 e2)\<close> is stricter as it could be.
It requires that all tree expressions are constant even if we can decide
- which branch to choose, provided the constant value of @{term b} *}
+ which branch to choose, provided the constant value of @{term b}\<close>
| "constVal (Call accC statT mode objRef mn pTs args) = None"
| "constVal (Methd C sig) = None"
| "constVal (Body C s) = None"
@@ -274,19 +274,19 @@
by (induct rule: constVal_Some_induct) simp_all
-subsection {* Main analysis for boolean expressions *}
+subsection \<open>Main analysis for boolean expressions\<close>
-text {* Assigned local variables after evaluating the expression if it evaluates
+text \<open>Assigned local variables after evaluating the expression if it evaluates
to a specific boolean value. If the expression cannot evaluate to a
@{term Boolean} value UNIV is returned. If we expect true/false the opposite
-constant false/true will also lead to UNIV. *}
+constant false/true will also lead to UNIV.\<close>
primrec assigns_if :: "bool \<Rightarrow> expr \<Rightarrow> lname set"
where
- "assigns_if b (NewC c) = UNIV" --{*can never evaluate to Boolean*}
-| "assigns_if b (NewA t e) = UNIV" --{*can never evaluate to Boolean*}
+ "assigns_if b (NewC c) = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>
+| "assigns_if b (NewA t e) = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>
| "assigns_if b (Cast t e) = assigns_if b e"
-| "assigns_if b (Inst e r) = assignsE e" --{*Inst has type Boolean but
- e is a reference type*}
+| "assigns_if b (Inst e r) = assignsE e" \<comment>\<open>Inst has type Boolean but
+ e is a reference type\<close>
| "assigns_if b (Lit val) = (if val=Bool b then {} else UNIV)"
| "assigns_if b (UnOp unop e) = (case constVal (UnOp unop e) of
None \<Rightarrow> (if unop = UNot
@@ -311,7 +311,7 @@
else assignsE e1 \<union> assignsE e2))
| Some v \<Rightarrow> (if v=Bool b then {} else UNIV))"
-| "assigns_if b (Super) = UNIV" --{*can never evaluate to Boolean*}
+| "assigns_if b (Super) = UNIV" \<comment>\<open>can never evaluate to Boolean\<close>
| "assigns_if b (Acc v) = (assignsV v)"
| "assigns_if b (v := e) = (assignsE (Ass v e))"
| "assigns_if b (c? e1 : e2) = (assignsE c) \<union>
@@ -323,8 +323,8 @@
| False \<Rightarrow> assigns_if b e2))"
| "assigns_if b ({accC,statT,mode}objRef\<cdot>mn({pTs}args))
= assignsE ({accC,statT,mode}objRef\<cdot>mn({pTs}args)) "
--- {* Only dummy analysis for intermediate expressions
- @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee} *}
+\<comment> \<open>Only dummy analysis for intermediate expressions
+ @{term Methd}, @{term Body}, @{term InsInitE} and @{term Callee}\<close>
| "assigns_if b (Methd C sig) = {}"
| "assigns_if b (Body C s) = {}"
| "assigns_if b (InsInitE s e) = {}"
@@ -347,10 +347,10 @@
by (cases binop) (simp_all)
next
case (Cond c e1 e2 b)
- note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
- note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
- note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
- note const = `constVal (c ? e1 : e2) = Some (Bool b)`
+ note hyp_c = \<open>\<And> b. ?Const b c \<Longrightarrow> ?Ass b c\<close>
+ note hyp_e1 = \<open>\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1\<close>
+ note hyp_e2 = \<open>\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2\<close>
+ note const = \<open>constVal (c ? e1 : e2) = Some (Bool b)\<close>
then obtain bv where bv: "constVal c = Some bv"
by simp
hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp)
@@ -395,10 +395,10 @@
by (cases binop) (simp_all)
next
case (Cond c e1 e2 b)
- note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
- note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
- note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
- note const = `constVal (c ? e1 : e2) = Some (Bool b)`
+ note hyp_c = \<open>\<And> b. ?Const b c \<Longrightarrow> ?Ass b c\<close>
+ note hyp_e1 = \<open>\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1\<close>
+ note hyp_e2 = \<open>\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2\<close>
+ note const = \<open>constVal (c ? e1 : e2) = Some (Bool b)\<close>
then obtain bv where bv: "constVal c = Some bv"
by simp
show ?case
@@ -425,7 +425,7 @@
by blast
qed
-subsection {* Lifting set operations to range of tables (map to a set) *}
+subsection \<open>Lifting set operations to range of tables (map to a set)\<close>
definition
union_ts :: "('a,'b) tables \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables" ("_ \<Rightarrow>\<union> _" [67,67] 65)
@@ -439,7 +439,7 @@
all_union_ts :: "('a,'b) tables \<Rightarrow> 'b set \<Rightarrow> ('a,'b) tables" (infixl "\<Rightarrow>\<union>\<^sub>\<forall>" 40)
where "(A \<Rightarrow>\<union>\<^sub>\<forall> B) = (\<lambda> k. A k \<union> B)"
-subsubsection {* Binary union of tables *}
+subsubsection \<open>Binary union of tables\<close>
lemma union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union> B) k) = (c \<in> A k \<or> c \<in> B k)"
by (unfold union_ts_def) blast
@@ -457,7 +457,7 @@
"\<lbrakk>c \<in> (A \<Rightarrow>\<union> B) k; (c \<in> A k \<Longrightarrow> P); (c \<in> B k \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
by (unfold union_ts_def) blast
-subsubsection {* Binary intersection of tables *}
+subsubsection \<open>Binary intersection of tables\<close>
lemma intersect_ts_iff [simp]: "c \<in> (A \<Rightarrow>\<inter> B) k = (c \<in> A k \<and> c \<in> B k)"
by (unfold intersect_ts_def) blast
@@ -476,7 +476,7 @@
by simp
-subsubsection {* All-Union of tables and set *}
+subsubsection \<open>All-Union of tables and set\<close>
lemma all_union_ts_iff [simp]: "(c \<in> (A \<Rightarrow>\<union>\<^sub>\<forall> B) k) = (c \<in> A k \<or> c \<in> B)"
by (unfold all_union_ts_def) blast
@@ -499,14 +499,14 @@
type_synonym breakass = "(label, lname) tables"
---{* Mapping from a break label, to the set of variables that will be assigned
- if the evaluation terminates with this break *}
+\<comment>\<open>Mapping from a break label, to the set of variables that will be assigned
+ if the evaluation terminates with this break\<close>
record assigned =
- nrm :: "lname set" --{* Definetly assigned variables
- for normal completion*}
- brk :: "breakass" --{* Definetly assigned variables for
- abrupt completion with a break *}
+ nrm :: "lname set" \<comment>\<open>Definetly assigned variables
+ for normal completion\<close>
+ brk :: "breakass" \<comment>\<open>Definetly assigned variables for
+ abrupt completion with a break\<close>
definition
rmlab :: "'a \<Rightarrow> ('a,'b) tables \<Rightarrow> ('a,'b) tables"
@@ -522,14 +522,14 @@
range_inter_ts :: "('a,'b) tables \<Rightarrow> 'b set" ("\<Rightarrow>\<Inter>_" 80)
where "\<Rightarrow>\<Inter>A = {x |x. \<forall> k. x \<in> A k}"
-text {*
-In @{text "E\<turnstile> B \<guillemotright>t\<guillemotright> A"},
-@{text B} denotes the ''assigned'' variables before evaluating term @{text t},
-whereas @{text A} denotes the ''assigned'' variables after evaluating term @{text t}.
-The environment @{term E} is only needed for the conditional @{text "_ ? _ : _"}.
+text \<open>
+In \<open>E\<turnstile> B \<guillemotright>t\<guillemotright> A\<close>,
+\<open>B\<close> denotes the ''assigned'' variables before evaluating term \<open>t\<close>,
+whereas \<open>A\<close> denotes the ''assigned'' variables after evaluating term \<open>t\<close>.
+The environment @{term E} is only needed for the conditional \<open>_ ? _ : _\<close>.
The definite assignment rules refer to the typing rules here to
distinguish boolean and other expressions.
-*}
+\<close>
inductive
da :: "env \<Rightarrow> lname set \<Rightarrow> term \<Rightarrow> assigned \<Rightarrow> bool" ("_\<turnstile> _ \<guillemotright>_\<guillemotright> _" [65,65,65,65] 71)
@@ -556,7 +556,7 @@
\<Longrightarrow>
Env\<turnstile> B \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A"
---{* Note that @{term E} is not further used, because we take the specialized
+\<comment>\<open>Note that @{term E} is not further used, because we take the specialized
sets that also consider if the expression evaluates to true or false.
Inside of @{term e} there is no {\tt break} or {\tt finally}, so the break
map of @{term E} will be the trivial one. So
@@ -572,7 +572,7 @@
to @{term UNIV} too, because @{term "assigns_if False e = UNIV"}. So
in the intersection of the break maps the path @{term c2} will have no
contribution.
- *}
+\<close>
| Loop: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E;
Env\<turnstile> (B \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C;
@@ -580,7 +580,7 @@
brk A = brk C\<rbrakk>
\<Longrightarrow>
Env\<turnstile> B \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
---{* The @{text Loop} rule resembles some of the ideas of the @{text If} rule.
+\<comment>\<open>The \<open>Loop\<close> rule resembles some of the ideas of the \<open>If\<close> rule.
For the @{term "nrm A"} the set @{term "B \<union> assigns_if False e"}
will be @{term UNIV} if the condition is constantly true. To normally exit
the while loop, we must consider the body @{term c} to be completed
@@ -589,7 +589,7 @@
only handles continue labels, not break labels. The break label will be
handled by an enclosing @{term Lab} statement. So we don't have to
handle the breaks specially.
- *}
+\<close>
| Jmp: "\<lbrakk>jump=Ret \<longrightarrow> Result \<in> B;
nrm A = UNIV;
@@ -599,13 +599,13 @@
| Ret \<Rightarrow> \<lambda> k. UNIV)\<rbrakk>
\<Longrightarrow>
Env\<turnstile> B \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A"
---{* In case of a break to label @{term l} the corresponding break set is all
+\<comment>\<open>In case of a break to label @{term l} the corresponding break set is all
variables assigned before the break. The assigned variables for normal
completion of the @{term Jmp} is @{term UNIV}, because the statement will
never complete normally. For continue and return the break map is the
trivial one. In case of a return we enshure that the result value is
assigned.
- *}
+\<close>
| Throw: "\<lbrakk>Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E; nrm A = UNIV; brk A = (\<lambda> l. UNIV)\<rbrakk>
\<Longrightarrow> Env\<turnstile> B \<guillemotright>\<langle>Throw e\<rangle>\<guillemotright> A"
@@ -622,23 +622,23 @@
brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)\<rbrakk>
\<Longrightarrow>
Env\<turnstile> B \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A"
---{* The set of assigned variables before execution @{term c2} are the same
+\<comment>\<open>The set of assigned variables before execution @{term c2} are the same
as before execution @{term c1}, because @{term c1} could throw an exception
and so we can't guarantee that any variable will be assigned in @{term c1}.
- The @{text Finally} statement completes
+ The \<open>Finally\<close> statement completes
normally if both @{term c1} and @{term c2} complete normally. If @{term c1}
completes abruptly with a break, then @{term c2} also will be executed
and may terminate normally or with a break. The overall break map then is
the intersection of the maps of both paths. If @{term c2} terminates
normally we have to extend all break sets in @{term "brk C1"} with
- @{term "nrm C2"} (@{text "\<Rightarrow>\<union>\<^sub>\<forall>"}). If @{term c2} exits with a break this
+ @{term "nrm C2"} (\<open>\<Rightarrow>\<union>\<^sub>\<forall>\<close>). If @{term c2} exits with a break this
break will appear in the overall result state. We don't know if
@{term c1} completed normally or abruptly (maybe with an exception not only
a break) so @{term c1} has no contribution to the break map following this
path.
- *}
+\<close>
---{* Evaluation of expressions and the break sets of definite assignment:
+\<comment>\<open>Evaluation of expressions and the break sets of definite assignment:
Thinking of a Java expression we assume that we can never have
a break statement inside of a expression. So for all expressions the
break sets could be set to the trivial one: @{term "\<lambda> l. UNIV"}.
@@ -656,18 +656,18 @@
the analysis of the correct nesting of breaks in the typing judgments
right now. So we have decided to adjust the rules of definite assignment
to fit to these circumstances. If an initialization is involved during
- evaluation of the expression (evaluation rules @{text FVar}, @{text NewC}
- and @{text NewA}
-*}
+ evaluation of the expression (evaluation rules \<open>FVar\<close>, \<open>NewC\<close>
+ and \<open>NewA\<close>
+\<close>
| Init: "Env\<turnstile> B \<guillemotright>\<langle>Init C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
---{* Wellformedness of a program will ensure, that every static initialiser
+\<comment>\<open>Wellformedness of a program will ensure, that every static initialiser
is definetly assigned and the jumps are nested correctly. The case here
for @{term Init} is just for convenience, to get a proper precondition
for the induction hypothesis in various proofs, so that we don't have to
expand the initialisation on every point where it is triggerred by the
evaluation rules.
- *}
+\<close>
| NewC: "Env\<turnstile> B \<guillemotright>\<langle>NewC C\<rangle>\<guillemotright> \<lparr>nrm=B,brk=\<lambda> l. UNIV\<rparr>"
| NewA: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
@@ -715,9 +715,9 @@
nrm A = B; brk A = (\<lambda> k. UNIV)\<rbrakk>
\<Longrightarrow>
Env\<turnstile> B \<guillemotright>\<langle>Acc (LVar vn)\<rangle>\<guillemotright> A"
---{* To properly access a local variable we have to test the definite
+\<comment>\<open>To properly access a local variable we have to test the definite
assignment here. The variable must occur in the set @{term B}
- *}
+\<close>
| Acc: "\<lbrakk>\<forall> vn. v \<noteq> LVar vn;
Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> A\<rbrakk>
@@ -754,7 +754,7 @@
\<Longrightarrow>
Env\<turnstile> B \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>\<guillemotright> A"
--- {* The interplay of @{term Call}, @{term Methd} and @{term Body}:
+\<comment> \<open>The interplay of @{term Call}, @{term Methd} and @{term Body}:
Why rules for @{term Methd} and @{term Body} at all? Note that a
Java source program will not include bare @{term Methd} or @{term Body}
terms. These terms are just introduced during evaluation. So definite
@@ -774,7 +774,7 @@
sub-evaluation during the type-safety proof. Note that well-typedness is
also a precondition for type-safety and so we can omit some assertion
that are already ensured by well-typedness.
- *}
+\<close>
| Methd: "\<lbrakk>methd (prg Env) D sig = Some m;
Env\<turnstile> B \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A
\<rbrakk>
@@ -785,7 +785,7 @@
nrm A = B; brk A = (\<lambda> l. UNIV)\<rbrakk>
\<Longrightarrow>
Env\<turnstile> B \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A"
--- {* Note that @{term A} is not correlated to @{term C}. If the body
+\<comment> \<open>Note that @{term A} is not correlated to @{term C}. If the body
statement returns abruptly with return, evaluation of @{term Body}
will absorb this return and complete normally. So we cannot trivially
get the assigned variables of the body statement since it has not
@@ -797,7 +797,7 @@
for a return the @{term Jump} rule ensures that the result variable is
set and then this information must be carried over to the @{term Body}
rule by the conformance predicate of the state.
- *}
+\<close>
| LVar: "Env\<turnstile> B \<guillemotright>\<langle>LVar vn\<rangle>\<guillemotright> \<lparr>nrm=B, brk=\<lambda> l. UNIV\<rparr>"
| FVar: "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> A
@@ -818,7 +818,7 @@
declare inj_term_sym_simps [simp]
declare assigns_if.simps [simp del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
+setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
inductive_cases da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
@@ -884,7 +884,7 @@
declare inj_term_sym_simps [simp del]
declare assigns_if.simps [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
-setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
+setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
(* To be able to eliminate both the versions with the overloaded brackets:
(B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A),
@@ -956,7 +956,7 @@
case (Cast T e)
have "E\<turnstile>e\<Colon>- (PrimT Boolean)"
proof -
- from `E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)`
+ from \<open>E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)\<close>
obtain Te where "E\<turnstile>e\<Colon>-Te"
"prg E\<turnstile>Te\<preceq>? PrimT Boolean"
by cases simp
@@ -986,10 +986,10 @@
by - (cases binop, auto simp add: assignsE_const_simp)
next
case (Cond c e1 e2)
- note hyp_c = `?Boolean c \<Longrightarrow> ?Incl c`
- note hyp_e1 = `?Boolean e1 \<Longrightarrow> ?Incl e1`
- note hyp_e2 = `?Boolean e2 \<Longrightarrow> ?Incl e2`
- note wt = `E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean`
+ note hyp_c = \<open>?Boolean c \<Longrightarrow> ?Incl c\<close>
+ note hyp_e1 = \<open>?Boolean e1 \<Longrightarrow> ?Incl e1\<close>
+ note hyp_e2 = \<open>?Boolean e2 \<Longrightarrow> ?Incl e2\<close>
+ note wt = \<open>E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean\<close>
then obtain
boolean_c: "E\<turnstile>c\<Colon>-PrimT Boolean" and
boolean_e1: "E\<turnstile>e1\<Colon>-PrimT Boolean" and
@@ -1067,10 +1067,10 @@
show ?case by cases simp
next
case (Lab Env B c C A l B' A')
- note A = `nrm A = nrm C \<inter> brk C l` `brk A = rmlab l (brk C)`
- note `PROP ?Hyp Env B \<langle>c\<rangle> C`
+ note A = \<open>nrm A = nrm C \<inter> brk C l\<close> \<open>brk A = rmlab l (brk C)\<close>
+ note \<open>PROP ?Hyp Env B \<langle>c\<rangle> C\<close>
moreover
- note `B \<subseteq> B'`
+ note \<open>B \<subseteq> B'\<close>
moreover
obtain C'
where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
@@ -1093,19 +1093,19 @@
by simp
next
case (Comp Env B c1 C1 c2 C2 A B' A')
- note A = `nrm A = nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2`
- from `Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'`
+ note A = \<open>nrm A = nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter> brk C2\<close>
+ from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'\<close>
obtain C1' C2'
where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
by cases auto
- note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
- moreover note `B \<subseteq> B'`
+ note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>
+ moreover note \<open>B \<subseteq> B'\<close>
moreover note da_c1
ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by auto
- note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2`
+ note \<open>PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2\<close>
with da_c2 C1'
have C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
by auto
@@ -1114,19 +1114,19 @@
by auto
next
case (If Env B e E c1 C1 c2 C2 A B' A')
- note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2`
- from `Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'`
+ note A = \<open>nrm A = nrm C1 \<inter> nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter> brk C2\<close>
+ from \<open>Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'\<close>
obtain C1' C2'
where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
by cases auto
- note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1`
- moreover note B' = `B \<subseteq> B'`
+ note \<open>PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1\<close>
+ moreover note B' = \<open>B \<subseteq> B'\<close>
moreover note da_c1
ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by blast
- note `PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2`
+ note \<open>PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2\<close>
with da_c2 B'
obtain C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
by blast
@@ -1135,16 +1135,16 @@
by auto
next
case (Loop Env B e E c C A l B' A')
- note A = `nrm A = nrm C \<inter> (B \<union> assigns_if False e)` `brk A = brk C`
- from `Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'`
+ note A = \<open>nrm A = nrm C \<inter> (B \<union> assigns_if False e)\<close> \<open>brk A = brk C\<close>
+ from \<open>Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'\<close>
obtain C'
where
da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)"
"brk A' = brk C'"
by cases auto
- note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C`
- moreover note B' = `B \<subseteq> B'`
+ note \<open>PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C\<close>
+ moreover note B' = \<open>B \<subseteq> B'\<close>
moreover note da_c'
ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)"
by blast
@@ -1175,8 +1175,8 @@
case Throw thus ?case by (elim da_elim_cases) auto
next
case (Try Env B c1 C1 vn C c2 C2 A B' A')
- note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter> brk C2`
- from `Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'`
+ note A = \<open>nrm A = nrm C1 \<inter> nrm C2\<close> \<open>brk A = brk C1 \<Rightarrow>\<inter> brk C2\<close>
+ from \<open>Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'\<close>
obtain C1' C2'
where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn}
@@ -1184,13 +1184,13 @@
A': "nrm A' = nrm C1' \<inter> nrm C2'"
"brk A' = brk C1' \<Rightarrow>\<inter> brk C2'"
by cases auto
- note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
- moreover note B' = `B \<subseteq> B'`
+ note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>
+ moreover note B' = \<open>B \<subseteq> B'\<close>
moreover note da_c1'
ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by blast
- note `PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
- (B \<union> {VName vn}) \<langle>c2\<rangle> C2`
+ note \<open>PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
+ (B \<union> {VName vn}) \<langle>c2\<rangle> C2\<close>
with B' da_c2'
obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
by blast
@@ -1199,21 +1199,21 @@
by auto
next
case (Fin Env B c1 C1 c2 C2 A B' A')
- note A = `nrm A = nrm C1 \<union> nrm C2`
- `brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)`
- from `Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'`
+ note A = \<open>nrm A = nrm C1 \<union> nrm C2\<close>
+ \<open>brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)\<close>
+ from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'\<close>
obtain C1' C2'
where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
A': "nrm A' = nrm C1' \<union> nrm C2'"
"brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')"
by cases auto
- note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
- moreover note B' = `B \<subseteq> B'`
+ note \<open>PROP ?Hyp Env B \<langle>c1\<rangle> C1\<close>
+ moreover note B' = \<open>B \<subseteq> B'\<close>
moreover note da_c1'
ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
by blast
- note hyp_c2 = `PROP ?Hyp Env B \<langle>c2\<rangle> C2`
+ note hyp_c2 = \<open>PROP ?Hyp Env B \<langle>c2\<rangle> C2\<close>
from da_c2' B'
obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
by - (drule hyp_c2,auto)
@@ -1236,17 +1236,17 @@
case UnOp thus ?case by (elim da_elim_cases) auto
next
case (CondAnd Env B e1 E1 e2 E2 A B' A')
- note A = `nrm A = B \<union>
+ note A = \<open>nrm A = B \<union>
assigns_if True (BinOp CondAnd e1 e2) \<inter>
- assigns_if False (BinOp CondAnd e1 e2)`
- `brk A = (\<lambda>l. UNIV)`
- from `Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'`
+ assigns_if False (BinOp CondAnd e1 e2)\<close>
+ \<open>brk A = (\<lambda>l. UNIV)\<close>
+ from \<open>Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'\<close>
obtain A': "nrm A' = B' \<union>
assigns_if True (BinOp CondAnd e1 e2) \<inter>
assigns_if False (BinOp CondAnd e1 e2)"
"brk A' = (\<lambda>l. UNIV)"
by cases auto
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
with A A' show ?case
by auto
next
@@ -1265,13 +1265,13 @@
case Ass thus ?case by (elim da_elim_cases) auto
next
case (CondBool Env c e1 e2 B C E1 E2 A B' A')
- note A = `nrm A = B \<union>
+ note A = \<open>nrm A = B \<union>
assigns_if True (c ? e1 : e2) \<inter>
- assigns_if False (c ? e1 : e2)`
- `brk A = (\<lambda>l. UNIV)`
- note `Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
+ assigns_if False (c ? e1 : e2)\<close>
+ \<open>brk A = (\<lambda>l. UNIV)\<close>
+ note \<open>Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)\<close>
moreover
- note `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
+ note \<open>Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'\<close>
ultimately
obtain A': "nrm A' = B' \<union>
assigns_if True (c ? e1 : e2) \<inter>
@@ -1279,14 +1279,14 @@
"brk A' = (\<lambda>l. UNIV)"
by (elim da_elim_cases) (auto simp add: inj_term_simps)
(* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
with A A' show ?case
by auto
next
case (Cond Env c e1 e2 B C E1 E2 A B' A')
- note A = `nrm A = nrm E1 \<inter> nrm E2` `brk A = (\<lambda>l. UNIV)`
- note not_bool = `\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
- from `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
+ note A = \<open>nrm A = nrm E1 \<inter> nrm E2\<close> \<open>brk A = (\<lambda>l. UNIV)\<close>
+ note not_bool = \<open>\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)\<close>
+ from \<open>Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'\<close>
obtain E1' E2'
where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
@@ -1295,12 +1295,12 @@
using not_bool
by (elim da_elim_cases) (auto simp add: inj_term_simps)
(* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
- note `PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1`
- moreover note B' = `B \<subseteq> B'`
+ note \<open>PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1\<close>
+ moreover note B' = \<open>B \<subseteq> B'\<close>
moreover note da_e1'
ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)"
by blast
- note `PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2`
+ note \<open>PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2\<close>
with B' da_e2'
obtain "nrm E2 \<subseteq> nrm E2'" "(\<forall>l. brk E2 l \<subseteq> brk E2' l)"
by blast
@@ -1326,7 +1326,7 @@
next
case Cons thus ?case by (elim da_elim_cases) auto
qed
- from this [OF da' `B \<subseteq> B'`] show ?thesis .
+ from this [OF da' \<open>B \<subseteq> B'\<close>] show ?thesis .
qed
lemma da_weaken:
@@ -1342,9 +1342,9 @@
case Expr thus ?case by (iprover intro: da.Expr)
next
case (Lab Env B c C A l B')
- note `PROP ?Hyp Env B \<langle>c\<rangle>`
+ note \<open>PROP ?Hyp Env B \<langle>c\<rangle>\<close>
moreover
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
by iprover
then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
@@ -1352,10 +1352,10 @@
thus ?case ..
next
case (Comp Env B c1 C1 c2 C2 A B')
- note da_c1 = `Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1`
- note `PROP ?Hyp Env B \<langle>c1\<rangle>`
+ note da_c1 = \<open>Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1\<close>
+ note \<open>PROP ?Hyp Env B \<langle>c1\<rangle>\<close>
moreover
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
by iprover
with da_c1 B'
@@ -1363,7 +1363,7 @@
"nrm C1 \<subseteq> nrm C1'"
by (rule da_monotone [elim_format]) simp
moreover
- note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>`
+ note \<open>PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>\<close>
ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
by iprover
with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
@@ -1371,7 +1371,7 @@
thus ?case ..
next
case (If Env B e E c1 C1 c2 C2 A B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
@@ -1405,7 +1405,7 @@
thus ?case ..
next
case (Loop Env B e E c C A l B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
@@ -1429,7 +1429,7 @@
thus ?case ..
next
case (Jmp jump B A Env B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' "
by auto
moreover
@@ -1448,7 +1448,7 @@
case Throw thus ?case by (iprover intro: da.Throw )
next
case (Try Env B c1 C1 vn C c2 C2 A B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
proof -
have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
@@ -1473,7 +1473,7 @@
thus ?case ..
next
case (Fin Env B c1 C1 c2 C2 A B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
proof -
have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
@@ -1507,7 +1507,7 @@
case UnOp thus ?case by (iprover intro: da.UnOp)
next
case (CondAnd Env B e1 E1 e2 E2 A B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
@@ -1529,7 +1529,7 @@
thus ?case ..
next
case (CondOr Env B e1 E1 e2 E2 A B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
@@ -1551,7 +1551,7 @@
thus ?case ..
next
case (BinOp Env B e1 E1 e2 A binop B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
@@ -1575,22 +1575,22 @@
thus ?case ..
next
case (Super B Env B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
with Super.hyps have "This \<in> B'"
by auto
thus ?case by (iprover intro: da.Super)
next
case (AccLVar vn B A Env B')
- note `vn \<in> B`
+ note \<open>vn \<in> B\<close>
moreover
- note `B \<subseteq> B'`
+ note \<open>B \<subseteq> B'\<close>
ultimately have "vn \<in> B'" by auto
thus ?case by (iprover intro: da.AccLVar)
next
case Acc thus ?case by (iprover intro: da.Acc)
next
case (AssLVar Env B e E A vn B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
by (rule AssLVar.hyps [elim_format]) iprover
then obtain A' where
@@ -1599,8 +1599,8 @@
thus ?case ..
next
case (Ass v Env B V e A B')
- note B' = `B \<subseteq> B'`
- note `\<forall>vn. v \<noteq> LVar vn`
+ note B' = \<open>B \<subseteq> B'\<close>
+ note \<open>\<forall>vn. v \<noteq> LVar vn\<close>
moreover
obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'"
proof -
@@ -1625,8 +1625,8 @@
thus ?case ..
next
case (CondBool Env c e1 e2 B C E1 E2 A B')
- note B' = `B \<subseteq> B'`
- note `Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
+ note B' = \<open>B \<subseteq> B'\<close>
+ note \<open>Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)\<close>
moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
proof -
have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
@@ -1661,8 +1661,8 @@
thus ?case ..
next
case (Cond Env c e1 e2 B C E1 E2 A B')
- note B' = `B \<subseteq> B'`
- note `\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
+ note B' = \<open>B \<subseteq> B'\<close>
+ note \<open>\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)\<close>
moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
proof -
have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
@@ -1697,7 +1697,7 @@
thus ?case ..
next
case (Call Env B e E args A accC statT mode mn pTs B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
@@ -1723,7 +1723,7 @@
case Methd thus ?case by (iprover intro: da.Methd)
next
case (Body Env B c C A D B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'"
proof -
have "Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" by (rule Body.hyps)
@@ -1737,10 +1737,10 @@
with da_c that show ?thesis by iprover
qed
moreover
- note `Result \<in> nrm C`
+ note \<open>Result \<in> nrm C\<close>
with nrm_C' have "Result \<in> nrm C'"
by blast
- moreover note `jumpNestingOkS {Ret} c`
+ moreover note \<open>jumpNestingOkS {Ret} c\<close>
ultimately obtain A' where
"Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
by (iprover intro: da.Body)
@@ -1751,7 +1751,7 @@
case FVar thus ?case by (iprover intro: da.FVar)
next
case (AVar Env B e1 E1 e2 A B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
proof -
have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
@@ -1777,7 +1777,7 @@
case Nil thus ?case by (iprover intro: da.Nil)
next
case (Cons Env B e E es A B')
- note B' = `B \<subseteq> B'`
+ note B' = \<open>B \<subseteq> B'\<close>
obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
proof -
have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
@@ -1800,7 +1800,7 @@
by (iprover intro: da.Cons)
thus ?case ..
qed
- from this [OF `B \<subseteq> B'`] show ?thesis .
+ from this [OF \<open>B \<subseteq> B'\<close>] show ?thesis .
qed
(* Remarks about the proof style:
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sat Jan 02 18:48:45 2016 +0100
@@ -1,4 +1,4 @@
-subsection {* Correctness of Definite Assignment *}
+subsection \<open>Correctness of Definite Assignment\<close>
theory DefiniteAssignmentCorrect imports WellForm Eval begin
@@ -104,8 +104,8 @@
"\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c"
proof (induct rule: var.induct expr.induct stmt.induct)
case (Lab j c jmps' jmps)
- note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
- note jmps = `jmps' \<subseteq> jmps`
+ note jmpOk = \<open>jumpNestingOkS jmps' (j\<bullet> c)\<close>
+ note jmps = \<open>jmps' \<subseteq> jmps\<close>
with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp
moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto
ultimately
@@ -135,10 +135,10 @@
by simp
next
case (Loop l e c jmps' jmps)
- from `jumpNestingOkS jmps' (l\<bullet> While(e) c)`
+ from \<open>jumpNestingOkS jmps' (l\<bullet> While(e) c)\<close>
have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
moreover
- from `jmps' \<subseteq> jmps`
+ from \<open>jmps' \<subseteq> jmps\<close>
have "{Cont l} \<union> jmps' \<subseteq> {Cont l} \<union> jmps" by auto
ultimately
have "jumpNestingOkS ({Cont l} \<union> jmps) c"
@@ -240,7 +240,7 @@
by (cases s) (simp add: avar_def2 abrupt_if_def)
-text {*
+text \<open>
The next theorem expresses: If jumps (breaks, continues, returns) are nested
correctly, we won't find an unexpected jump in the result state of the
evaluation. For exeample, a break can't leave its enclosing loop, an return
@@ -266,7 +266,7 @@
The wellformedness of the program is used to enshure that for all
classinitialisations and methods the nesting of jumps is wellformed, too.
-*}
+\<close>
theorem jumpNestingOk_eval:
assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
and jmpOk: "jumpNestingOk jmps t"
@@ -287,19 +287,19 @@
(\<forall> jmps T Env.
?Jmp jmps s0 \<longrightarrow> jumpNestingOk jmps t \<longrightarrow> Env\<turnstile>t\<Colon>T \<longrightarrow> prg Env=G\<longrightarrow>
?Jmp jmps s1 \<and> ?Upd v s1)"
- -- {* Variable @{text ?HypObj} is the following goal spelled in terms of
+ \<comment> \<open>Variable \<open>?HypObj\<close> is the following goal spelled in terms of
the object logic, instead of the meta logic. It is needed in some
cases of the induction were, the atomize-rulify process of induct
does not work fine, because the eval rules mix up object and meta
- logic. See for example the case for the loop. *}
+ logic. See for example the case for the loop.\<close>
from eval
have "\<And> jmps T Env. \<lbrakk>?Jmp jmps s0; jumpNestingOk jmps t; Env\<turnstile>t\<Colon>T;prg Env=G\<rbrakk>
\<Longrightarrow> ?Jmp jmps s1 \<and> ?Upd v s1"
(is "PROP ?Hyp t s0 s1 v")
- -- {* We need to abstract over @{term jmps} since @{term jmps} are extended
+ \<comment> \<open>We need to abstract over @{term jmps} since @{term jmps} are extended
during analysis of @{term Lab}. Also we need to abstract over
@{term T} and @{term Env} since they are altered in various
- typing judgements. *}
+ typing judgements.\<close>
proof (induct)
case Abrupt thus ?case by simp
next
@@ -308,8 +308,8 @@
case Expr thus ?case by (elim wt_elim_cases) simp
next
case (Lab s0 c s1 jmp jmps T Env)
- note jmpOK = `jumpNestingOk jmps (In1r (jmp\<bullet> c))`
- note G = `prg Env = G`
+ note jmpOK = \<open>jumpNestingOk jmps (In1r (jmp\<bullet> c))\<close>
+ note G = \<open>prg Env = G\<close>
have wt_c: "Env\<turnstile>c\<Colon>\<surd>"
using Lab.prems by (elim wt_elim_cases)
{
@@ -319,7 +319,7 @@
proof -
from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
by (cases s1) (simp add: absorb_def)
- note hyp_c = `PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>`
+ note hyp_c = \<open>PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>\<close>
from ab_s1 have "j \<noteq> jmp"
by (cases s1) (simp add: absorb_def)
moreover have "j \<in> {jmp} \<union> jmps"
@@ -337,8 +337,8 @@
thus ?case by simp
next
case (Comp s0 c1 s1 c2 s2 jmps T Env)
- note jmpOk = `jumpNestingOk jmps (In1r (c1;; c2))`
- note G = `prg Env = G`
+ note jmpOk = \<open>jumpNestingOk jmps (In1r (c1;; c2))\<close>
+ note G = \<open>prg Env = G\<close>
from Comp.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
@@ -349,11 +349,11 @@
proof -
have jmp: "?Jmp jmps s1"
proof -
- note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>`
+ note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>\<close>
with wt_c1 jmpOk G
show ?thesis by simp
qed
- moreover note hyp_c2 = `PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)`
+ moreover note hyp_c2 = \<open>PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)\<close>
have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
moreover note wt_c2 G abr_s2
ultimately show "j \<in> jmps"
@@ -362,8 +362,8 @@
} thus ?case by simp
next
case (If s0 e b s1 c1 c2 s2 jmps T Env)
- note jmpOk = `jumpNestingOk jmps (In1r (If(e) c1 Else c2))`
- note G = `prg Env = G`
+ note jmpOk = \<open>jumpNestingOk jmps (In1r (If(e) c1 Else c2))\<close>
+ note G = \<open>prg Env = G\<close>
from If.prems obtain
wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and
wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
@@ -373,11 +373,11 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
+ note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
with wt_e G have "?Jmp jmps s1"
by simp
moreover note hyp_then_else =
- `PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>`
+ \<open>PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>\<close>
have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
using jmpOk by (cases "the_Bool b") simp_all
moreover note wt_then_else G jmp
@@ -388,9 +388,9 @@
thus ?case by simp
next
case (Loop s0 e b s1 c s2 l s3 jmps T Env)
- note jmpOk = `jumpNestingOk jmps (In1r (l\<bullet> While(e) c))`
- note G = `prg Env = G`
- note wt = `Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
+ note jmpOk = \<open>jumpNestingOk jmps (In1r (l\<bullet> While(e) c))\<close>
+ note G = \<open>prg Env = G\<close>
+ note wt = \<open>Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T\<close>
then obtain
wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and
wt_c: "Env\<turnstile>c\<Colon>\<surd>"
@@ -400,7 +400,7 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
+ note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
with wt_e G have jmp_s1: "?Jmp jmps s1"
by simp
show ?thesis
@@ -468,8 +468,8 @@
case (Jmp s j jmps T Env) thus ?case by simp
next
case (Throw s0 e a s1 jmps T Env)
- note jmpOk = `jumpNestingOk jmps (In1r (Throw e))`
- note G = `prg Env = G`
+ note jmpOk = \<open>jumpNestingOk jmps (In1r (Throw e))\<close>
+ note G = \<open>prg Env = G\<close>
from Throw.prems obtain Te where
wt_e: "Env\<turnstile>e\<Colon>-Te"
by (elim wt_elim_cases)
@@ -478,7 +478,7 @@
assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
have "j\<in>jmps"
proof -
- from `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
+ from \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
have "?Jmp jmps s1" using wt_e G by simp
moreover
from jmp
@@ -490,8 +490,8 @@
thus ?case by simp
next
case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
- note jmpOk = `jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))`
- note G = `prg Env = G`
+ note jmpOk = \<open>jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))\<close>
+ note G = \<open>prg Env = G\<close>
from Try.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
@@ -501,10 +501,10 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note `PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)`
+ note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)\<close>
with jmpOk wt_c1 G
have jmp_s1: "?Jmp jmps s1" by simp
- note s2 = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
+ note s2 = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
show "j \<in> jmps"
proof (cases "G,s2\<turnstile>catch C")
case False
@@ -542,8 +542,8 @@
thus ?case by simp
next
case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
- note jmpOk = `jumpNestingOk jmps (In1r (c1 Finally c2))`
- note G = `prg Env = G`
+ note jmpOk = \<open>jumpNestingOk jmps (In1r (c1 Finally c2))\<close>
+ note G = \<open>prg Env = G\<close>
from Fin.prems obtain
wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases)
@@ -553,14 +553,14 @@
have "j \<in> jmps"
proof (cases "x1=Some (Jump j)")
case True
- note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>`
+ note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>\<close>
with True jmpOk wt_c1 G show ?thesis
by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
next
case False
- note hyp_c2 = `PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>`
- note `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
- else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
+ note hyp_c2 = \<open>PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>\<close>
+ note \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+ else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>
with False jmp have "abrupt s2 = Some (Jump j)"
by (cases s2) (simp add: abrupt_if_def)
with jmpOk wt_c2 G show ?thesis
@@ -570,9 +570,9 @@
thus ?case by simp
next
case (Init C c s0 s3 s1 s2 jmps T Env)
- note `jumpNestingOk jmps (In1r (Init C))`
- note G = `prg Env = G`
- note `the (class G C) = c`
+ note \<open>jumpNestingOk jmps (In1r (Init C))\<close>
+ note G = \<open>prg Env = G\<close>
+ note \<open>the (class G C) = c\<close>
with Init.prems have c: "class G C = Some c"
by (elim wt_elim_cases) auto
{
@@ -640,15 +640,15 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note `prg Env = G`
- moreover note hyp_init = `PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>`
+ note \<open>prg Env = G\<close>
+ moreover note hyp_init = \<open>PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>\<close>
moreover from wf NewC.prems
have "Env\<turnstile>(Init C)\<Colon>\<surd>"
by (elim wt_elim_cases) (drule is_acc_classD,simp)
moreover
have "abrupt s1 = Some (Jump j)"
proof -
- from `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2` and jmp show ?thesis
+ from \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> and jmp show ?thesis
by (rule halloc_no_jump')
qed
ultimately show "j \<in> jmps"
@@ -663,20 +663,20 @@
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from NewA.prems
obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
by (elim wt_elim_cases) (auto dest: wt_init_comp_ty')
- note `PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>`
+ note \<open>PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>\<close>
with wt_init G
have "?Jmp jmps s1"
by (simp add: init_comp_ty_def)
moreover
- note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 i)`
+ note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 i)\<close>
have "abrupt s2 = Some (Jump j)"
proof -
- note `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
+ note \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3\<close>
moreover note jmp
ultimately
have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
@@ -695,14 +695,14 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
- note `prg Env = G`
+ note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
+ note \<open>prg Env = G\<close>
moreover from Cast.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover
have "abrupt s1 = Some (Jump j)"
proof -
- note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
+ note \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>
moreover note jmp
ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
qed
@@ -718,8 +718,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
- note `prg Env = G`
+ note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
+ note \<open>prg Env = G\<close>
moreover from Inst.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover note jmp
@@ -737,8 +737,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
- note `prg Env = G`
+ note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
+ note \<open>prg Env = G\<close>
moreover from UnOp.prems
obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
moreover note jmp
@@ -754,17 +754,17 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from BinOp.prems
obtain e1T e2T where
wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
by (elim wt_elim_cases)
- note `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)`
+ note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)\<close>
with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
note hyp_e2 =
- `PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
- s1 s2 (In1 v2)`
+ \<open>PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
+ s1 s2 (In1 v2)\<close>
show "j\<in>jmps"
proof (cases "need_second_arg binop v1")
case True with jmp_s1 wt_e2 jmp G
@@ -787,8 +787,8 @@
assume jmp: "abrupt s1 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_va = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))`
- note `prg Env = G`
+ note hyp_va = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))\<close>
+ note \<open>prg Env = G\<close>
moreover from Acc.prems
obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
moreover note jmp
@@ -799,14 +799,14 @@
thus ?case by simp
next
case (Ass s0 va w f s1 e v s2 jmps T Env)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from Ass.prems
obtain vT eT where
wt_va: "Env\<turnstile>va\<Colon>=vT" and
wt_e: "Env\<turnstile>e\<Colon>-eT"
by (elim wt_elim_cases)
- note hyp_v = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))`
- note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 v)`
+ note hyp_v = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))\<close>
+ note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 v)\<close>
{
fix j
assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
@@ -815,7 +815,7 @@
have "abrupt s2 = Some (Jump j)"
proof (cases "normal s2")
case True
- from `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2` and True have nrm_s1: "normal s1"
+ from \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> and True have nrm_s1: "normal s1"
by (rule eval_no_abrupt_lemma [rule_format])
with nrm_s1 wt_va G True
have "abrupt (f v s2) \<noteq> Some (Jump j)"
@@ -838,9 +838,9 @@
thus ?case by simp
next
case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)
- note G = `prg Env = G`
- note hyp_e0 = `PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)`
- note hyp_e1_e2 = `PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)`
+ note G = \<open>prg Env = G\<close>
+ note hyp_e0 = \<open>PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)\<close>
+ note hyp_e1_e2 = \<open>PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)\<close>
from Cond.prems
obtain e1T e2T
where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"
@@ -873,7 +873,7 @@
next
case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
jmps T Env)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from Call.prems
obtain eT argsT
where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
@@ -884,26 +884,26 @@
= Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
+ note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
from wt_e G
have jmp_s1: "?Jmp jmps s1"
by - (rule hyp_e [THEN conjunct1],simp_all)
- note hyp_args = `PROP ?Hyp (In3 args) s1 s2 (In3 vs)`
+ note hyp_args = \<open>PROP ?Hyp (In3 args) s1 s2 (In3 vs)\<close>
have "abrupt s2 = Some (Jump j)"
proof -
- note `G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4`
+ note \<open>G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4\<close>
moreover
from jmp have "abrupt s4 = Some (Jump j)"
by (cases s4) simp
ultimately have "abrupt s3' = Some (Jump j)"
by - (rule ccontr,drule (1) Methd_no_jump,simp)
- moreover note `s3' = check_method_access G accC statT mode
- \<lparr>name = mn, parTs = pTs\<rparr> a s3`
+ moreover note \<open>s3' = check_method_access G accC statT mode
+ \<lparr>name = mn, parTs = pTs\<rparr> a s3\<close>
ultimately have "abrupt s3 = Some (Jump j)"
by (cases s3)
(simp add: check_method_access_def abrupt_if_def Let_def)
moreover
- note `s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2`
+ note \<open>s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2\<close>
ultimately show ?thesis
by (cases s2) (auto simp add: init_lvars_def2)
qed
@@ -915,7 +915,7 @@
thus ?case by simp
next
case (Methd s0 D sig v s1 jmps T Env)
- from `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
+ from \<open>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<close>
have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
by (rule eval.Methd)
hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
@@ -934,7 +934,7 @@
thus ?case by (simp add: lvar_def Let_def)
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from wf FVar.prems
obtain statC f where
wt_e: "Env\<turnstile>e\<Colon>-Class statC" and
@@ -951,21 +951,21 @@
thus ?thesis
by simp
qed
- note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
+ note fvar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>
{
fix j
assume jmp: "abrupt s3 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_init = `PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>`
+ note hyp_init = \<open>PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>\<close>
from G wt_init
have "?Jmp jmps s1"
by - (rule hyp_init [THEN conjunct1],auto)
moreover
- note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 a)`
+ note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 a)\<close>
have "abrupt s2 = Some (Jump j)"
proof -
- note `s3 = check_field_access G accC statDeclC fn stat a s2'`
+ note \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
with jmp have "abrupt s2' = Some (Jump j)"
by (cases s2')
(simp add: check_field_access_def abrupt_if_def Let_def)
@@ -993,23 +993,23 @@
ultimately show ?case using v by simp
next
case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from AVar.prems
obtain e1T e2T where
wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
by (elim wt_elim_cases) simp
- note avar = `(v, s2') = avar G i a s2`
+ note avar = \<open>(v, s2') = avar G i a s2\<close>
{
fix j
assume jmp: "abrupt s2' = Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_e1 = `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)`
+ note hyp_e1 = \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)\<close>
from G wt_e1
have "?Jmp jmps s1"
by - (rule hyp_e1 [THEN conjunct1], auto)
moreover
- note hyp_e2 = `PROP ?Hyp (In1l e2) s1 s2 (In1 i)`
+ note hyp_e2 = \<open>PROP ?Hyp (In1l e2) s1 s2 (In1 i)\<close>
have "abrupt s2 = Some (Jump j)"
proof -
from avar have "s2' = snd (avar G i a s2)"
@@ -1039,7 +1039,7 @@
case Nil thus ?case by simp
next
case (Cons s0 e v s1 es vs s2 jmps T Env)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from Cons.prems obtain eT esT
where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_e2: "Env\<turnstile>es\<Colon>\<doteq>esT"
by (elim wt_elim_cases) simp
@@ -1048,12 +1048,12 @@
assume jmp: "abrupt s2 = Some (Jump j)"
have "j\<in>jmps"
proof -
- note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+ note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
from G wt_e
have "?Jmp jmps s1"
by - (rule hyp_e [THEN conjunct1],simp_all)
moreover
- note hyp_es = `PROP ?Hyp (In3 es) s1 s2 (In3 vs)`
+ note hyp_es = \<open>PROP ?Hyp (In3 es) s1 s2 (In3 vs)\<close>
ultimately show ?thesis
using wt_e2 G jmp
by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
@@ -1255,7 +1255,7 @@
\<subseteq> dom (locals (store (snd (avar G i a s))))"
by (cases s, simp add: avar_def2)
- text {*
+ text \<open>
Since assignments are modelled as functions from states to states, we
must take into account these functions. They appear only in the assignment
rule and as result from evaluating a variable. Thats why we need the
@@ -1268,7 +1268,7 @@
could also think of a pair of a value and a reference in the store, instead of
the generic update function. But as only array updates can cause a special
exception (if the types mismatch) and not array reads we then have to introduce
-two different rules to handle array reads and updates *}
+two different rules to handle array reads and updates\<close>
lemma dom_locals_eval_mono:
assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1)) \<and>
@@ -1334,7 +1334,7 @@
then
have s0_s1: "dom (locals (store ((Norm s0)::state)))
\<subseteq> dom (locals (store s1))" by simp
- from `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
+ from \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
by (rule dom_locals_sxalloc_mono)
thus ?case
@@ -1402,7 +1402,7 @@
qed
next
case (NewC s0 C s1 a s2)
- note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
+ note halloc = \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close>
from NewC.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1412,7 +1412,7 @@
finally show ?case by simp
next
case (NewA s0 T s1 e i s2 a s3)
- note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
+ note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>
from NewA.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1470,7 +1470,7 @@
finally show ?thesis by simp
next
case False
- with `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
+ with \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close>
have "s2=s1"
by auto
with s0_s1 False
@@ -1492,7 +1492,7 @@
finally show ?case by simp
next
case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
- note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
+ note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>
from Call.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1521,10 +1521,10 @@
also
have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
proof -
- from `s3 =
+ from \<open>s3 =
(if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
abrupt s2 = Some (Jump (Cont l))
- then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
+ then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)\<close>
show ?thesis
by simp
qed
@@ -1546,7 +1546,7 @@
by (simp add: dom_locals_fvar_vvar_mono)
hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s3 \<longrightarrow> ?V_ok)"
by - (intro strip, simp)
- note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
+ note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
from FVar.hyps
have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
by simp
@@ -1659,7 +1659,7 @@
from eval normal show ?thesis
proof (induct)
case Abrupt thus ?case by simp
- next -- {* For statements its trivial, since then @{term "assigns t = {}"} *}
+ next \<comment> \<open>For statements its trivial, since then @{term "assigns t = {}"}\<close>
case Skip show ?case by simp
next
case Expr show ?case by simp
@@ -1685,7 +1685,7 @@
case NewC show ?case by simp
next
case (NewA s0 T s1 e i s2 a s3)
- note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
+ note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>
have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
proof -
from NewA
@@ -1728,8 +1728,8 @@
also
have "\<dots> \<subseteq> dom (locals (store s2))"
proof -
- note `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
- else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
+ note \<open>G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+ else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)\<close>
thus ?thesis
by (rule dom_locals_eval_mono_elim)
qed
@@ -1752,7 +1752,7 @@
case Acc thus ?case by simp
next
case (Ass s0 va w f s1 e v s2)
- note nrm_ass_s2 = `normal (assign f v s2)`
+ note nrm_ass_s2 = \<open>normal (assign f v s2)\<close>
hence nrm_s2: "normal s2"
by (cases s2, simp add: assign_def Let_def)
with Ass.hyps
@@ -1843,16 +1843,16 @@
case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
have nrm_s2: "normal s2"
proof -
- from `normal ((set_lvars (locals (snd s2))) s4)`
+ from \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>
have normal_s4: "normal s4" by simp
hence "normal s3'" using Call.hyps
by - (erule eval_no_abrupt_lemma [rule_format])
moreover note
- `s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3`
+ \<open>s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3\<close>
ultimately have "normal s3"
by (cases s3) (simp add: check_method_access_def Let_def)
moreover
- note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
+ note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>
ultimately show "normal s2"
by (cases s2) (simp add: init_lvars_def2)
qed
@@ -1883,11 +1883,11 @@
case LVar thus ?case by simp
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
- note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
- note avar = `(v, s2') = fvar statDeclC stat fn a s2`
+ note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
+ note avar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>
have nrm_s2: "normal s2"
proof -
- note `normal s3`
+ note \<open>normal s3\<close>
with s3 have "normal s2'"
by (cases s2') (simp add: check_field_access_def Let_def)
with avar show "normal s2"
@@ -1912,10 +1912,10 @@
by simp
next
case (AVar s0 e1 a s1 e2 i s2 v s2')
- note avar = `(v, s2') = avar G i a s2`
+ note avar = \<open>(v, s2') = avar G i a s2\<close>
have nrm_s2: "normal s2"
proof -
- from avar and `normal s2'`
+ from avar and \<open>normal s2'\<close>
show ?thesis by (cases s2) (simp add: avar_def2)
qed
with AVar.hyps
@@ -2018,17 +2018,17 @@
case Inst hence False by simp thus ?case ..
next
case (Lit val c v s0 s)
- note `constVal (Lit val) = Some c`
+ note \<open>constVal (Lit val) = Some c\<close>
moreover
- from `G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s`
+ from \<open>G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s\<close>
obtain "v=val" and "normal s"
by cases simp
ultimately show "v=c \<and> normal s" by simp
next
case (UnOp unop e c v s0 s)
- note const = `constVal (UnOp unop e) = Some c`
+ note const = \<open>constVal (UnOp unop e) = Some c\<close>
then obtain ce where ce: "constVal e = Some ce" by simp
- from `G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s`
+ from \<open>G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s\<close>
obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
v: "v = eval_unop unop ve"
by cases simp
@@ -2042,12 +2042,12 @@
show ?case ..
next
case (BinOp binop e1 e2 c v s0 s)
- note const = `constVal (BinOp binop e1 e2) = Some c`
+ note const = \<open>constVal (BinOp binop e1 e2) = Some c\<close>
then obtain c1 c2 where c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2" and
c: "c = eval_binop binop c1 c2"
by simp
- from `G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s`
+ from \<open>G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s\<close>
obtain v1 s1 v2
where v1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
v2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
@@ -2089,13 +2089,13 @@
case Ass hence False by simp thus ?case ..
next
case (Cond b e1 e2 c v s0 s)
- note c = `constVal (b ? e1 : e2) = Some c`
+ note c = \<open>constVal (b ? e1 : e2) = Some c\<close>
then obtain cb c1 c2 where
cb: "constVal b = Some cb" and
c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2"
by (auto split: bool.splits)
- from `G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s`
+ from \<open>G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s\<close>
obtain vb s1
where vb: "G\<turnstile>Norm s0 \<midarrow>b-\<succ>vb\<rightarrow> s1" and
eval_v: "G\<turnstile>s1 \<midarrow>(if the_Bool vb then e1 else e2)-\<succ>v\<rightarrow> s"
@@ -2166,27 +2166,27 @@
case Inst hence False by simp thus ?case ..
next
case (Lit v c)
- from `constVal (Lit v) = Some c`
+ from \<open>constVal (Lit v) = Some c\<close>
have "c=v" by simp
moreover
- from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>
have "typeof empty_dt v = Some (PrimT Boolean)"
by cases simp
ultimately show ?case by simp
next
case (UnOp unop e c)
- from `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>
have "Boolean = unop_type unop" by cases simp
moreover
- from `constVal (UnOp unop e) = Some c`
+ from \<open>constVal (UnOp unop e) = Some c\<close>
obtain ce where "c = eval_unop unop ce" by auto
ultimately show ?case by (simp add: eval_unop_type)
next
case (BinOp binop e1 e2 c)
- from `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>
have "Boolean = binop_type binop" by cases simp
moreover
- from `constVal (BinOp binop e1 e2) = Some c`
+ from \<open>constVal (BinOp binop e1 e2) = Some c\<close>
obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
ultimately show ?case by (simp add: eval_binop_type)
next
@@ -2197,13 +2197,13 @@
case Ass hence False by simp thus ?case ..
next
case (Cond b e1 e2 c)
- note c = `constVal (b ? e1 : e2) = Some c`
+ note c = \<open>constVal (b ? e1 : e2) = Some c\<close>
then obtain cb c1 c2 where
cb: "constVal b = Some cb" and
c1: "constVal e1 = Some c1" and
c2: "constVal e2 = Some c2"
by (auto split: bool.splits)
- note wt = `Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean`
+ note wt = \<open>Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean\<close>
then
obtain T1 T2
where "Env\<turnstile>b\<Colon>-PrimT Boolean" and
@@ -2239,8 +2239,8 @@
bool: "Env\<turnstile> e\<Colon>-PrimT Boolean"
shows "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
proof -
- -- {* To properly perform induction on the evaluation relation we have to
- generalize the lemma to terms not only expressions. *}
+ \<comment> \<open>To properly perform induction on the evaluation relation we have to
+ generalize the lemma to terms not only expressions.\<close>
{ fix t val
assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"
assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
@@ -2252,26 +2252,26 @@
case Abrupt thus ?case by simp
next
case (NewC s0 C s1 a s2)
- from `Env\<turnstile>NewC C\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>NewC C\<Colon>-PrimT Boolean\<close>
have False
by cases simp
thus ?case ..
next
case (NewA s0 T s1 e i s2 a s3)
- from `Env\<turnstile>New T[e]\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>New T[e]\<Colon>-PrimT Boolean\<close>
have False
by cases simp
thus ?case ..
next
case (Cast s0 e b s1 s2 T)
- note s2 = `s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1`
+ note s2 = \<open>s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1\<close>
have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
proof -
- from s2 and `normal s2`
+ from s2 and \<open>normal s2\<close>
have "normal s1"
by (cases s1) simp
moreover
- from `Env\<turnstile>Cast T e\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>Cast T e\<Colon>-PrimT Boolean\<close>
have "Env\<turnstile>e\<Colon>- PrimT Boolean"
by cases (auto dest: cast_Boolean2)
ultimately show ?thesis
@@ -2283,14 +2283,14 @@
finally show ?case by simp
next
case (Inst s0 e v s1 b T)
- from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1` and `normal s1`
+ from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close> and \<open>normal s1\<close>
have "assignsE e \<subseteq> dom (locals (store s1))"
by (rule assignsE_good_approx)
thus ?case
by simp
next
case (Lit s v)
- from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>
have "typeof empty_dt v = Some (PrimT Boolean)"
by cases simp
then obtain b where "v=Bool b"
@@ -2299,13 +2299,13 @@
by simp
next
case (UnOp s0 e v s1 unop)
- note bool = `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
+ note bool = \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>
hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean"
by cases (cases unop,simp_all)
show ?case
proof (cases "constVal (UnOp unop e)")
case None
- note `normal s1`
+ note \<open>normal s1\<close>
moreover note bool_e
ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
by (rule UnOp.hyps [elim_format]) auto
@@ -2321,7 +2321,7 @@
next
case (Some c)
moreover
- from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+ from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>
have "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1"
by (rule eval.UnOp)
with Some
@@ -2339,7 +2339,7 @@
qed
next
case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
- note bool = `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
+ note bool = \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>
show ?case
proof (cases "constVal (BinOp binop e1 e2)")
case (Some c)
@@ -2392,7 +2392,7 @@
with condAnd
have need_second: "need_second_arg binop v1"
by (simp add: need_second_arg_def)
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format])
(simp add: need_second bool_e2)+
@@ -2412,7 +2412,7 @@
obtain "the_Bool v1=True" and "the_Bool v2 = False"
by (simp add: need_second_arg_def)
moreover
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
with e1_s2
@@ -2440,7 +2440,7 @@
with condOr
have need_second: "need_second_arg binop v1"
by (simp add: need_second_arg_def)
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format])
(simp add: need_second bool_e2)+
@@ -2460,7 +2460,7 @@
obtain "the_Bool v1=False" and "the_Bool v2 = True"
by (simp add: need_second_arg_def)
moreover
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
with e1_s2
@@ -2483,12 +2483,12 @@
qed
next
case False
- note `\<not> (binop = CondAnd \<or> binop = CondOr)`
+ note \<open>\<not> (binop = CondAnd \<or> binop = CondOr)\<close>
from BinOp.hyps
have
"prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
by - (rule eval.BinOp)
- moreover note `normal s2`
+ moreover note \<open>normal s2\<close>
ultimately
have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
by (rule assignsE_good_approx)
@@ -2499,13 +2499,13 @@
qed
next
case Super
- note `Env\<turnstile>Super\<Colon>-PrimT Boolean`
+ note \<open>Env\<turnstile>Super\<Colon>-PrimT Boolean\<close>
hence False
by cases simp
thus ?case ..
next
case (Acc s0 va v f s1)
- from `prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1` and `normal s1`
+ from \<open>prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1\<close> and \<open>normal s1\<close>
have "assignsV va \<subseteq> dom (locals (store s1))"
by (rule assignsV_good_approx)
thus ?case by simp
@@ -2513,23 +2513,23 @@
case (Ass s0 va w f s1 e v s2)
hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"
by - (rule eval.Ass)
- moreover note `normal (assign f v s2)`
+ moreover note \<open>normal (assign f v s2)\<close>
ultimately
have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"
by (rule assignsE_good_approx)
thus ?case by simp
next
case (Cond s0 e0 b s1 e1 e2 v s2)
- from `Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean`
+ from \<open>Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean\<close>
obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
by cases (auto dest: widen_Boolean2)
- note eval_e0 = `prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
+ note eval_e0 = \<open>prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1\<close>
have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
proof -
note eval_e0
moreover
- from Cond.hyps and `normal s2` have "normal s1"
+ from Cond.hyps and \<open>normal s2\<close> have "normal s1"
by - (erule eval_no_abrupt_lemma [rule_format],simp)
ultimately
have "assignsE e0 \<subseteq> dom (locals (store s1))"
@@ -2547,14 +2547,14 @@
\<subseteq> dom (locals (store s2))"
proof (cases "the_Bool b")
case True
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)
thus ?thesis
by blast
next
case False
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)
thus ?thesis
@@ -2574,7 +2574,7 @@
show ?thesis
proof (cases "the_Bool c")
case True
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)
with e0_s2
@@ -2584,7 +2584,7 @@
by simp
next
case False
- from `normal s2`
+ from \<open>normal s2\<close>
have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"
by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)
with e0_s2
@@ -2602,14 +2602,14 @@
by - (rule eval.Call)
hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args))
\<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"
- using `normal ((set_lvars (locals (snd s2))) s4)`
+ using \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>
by (rule assignsE_good_approx)
thus ?case by simp
next
case Methd show ?case by simp
next
case Body show ?case by simp
- qed simp+ -- {* all the statements and variables *}
+ qed simp+ \<comment> \<open>all the statements and variables\<close>
}
note generalized = this
from eval bool show ?thesis
@@ -2653,7 +2653,7 @@
let ?HypObj = "\<lambda> t s0 s1.
\<forall> Env T A. ?Wt Env t T \<longrightarrow> ?Da Env s0 t A \<longrightarrow> prg Env = G
\<longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1"
- -- {* Goal in object logic variant *}
+ \<comment> \<open>Goal in object logic variant\<close>
let ?Hyp = "\<lambda>t s0 s1. (\<And> Env T A. \<lbrakk>?Wt Env t T; ?Da Env s0 t A; prg Env = G\<rbrakk>
\<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1)"
from eval and wt da G
@@ -2692,7 +2692,7 @@
(rule Expr.hyps, auto)
next
case (Lab s0 c s1 j Env T A)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from Lab.prems
obtain C l where
da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
@@ -2751,7 +2751,7 @@
ultimately show ?case by (intro conjI)
next
case (Comp s0 c1 s1 c2 s2 Env T A)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from Comp.prems
obtain C1 C2
where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
@@ -2762,7 +2762,7 @@
obtain wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
by (elim wt_elim_cases) simp
- note `PROP ?Hyp (In1r c1) (Norm s0) s1`
+ note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1\<close>
with wt_c1 da_c1 G
obtain nrm_c1: "?NormalAssigned s1 C1" and
brk_c1: "?BreakAssigned (Norm s0) s1 C1" and
@@ -2777,7 +2777,7 @@
nrm_c2: "nrm C2 \<subseteq> nrm C2'" and
brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
by (rule da_weakenE) iprover
- note `PROP ?Hyp (In1r c2) s1 s2`
+ note \<open>PROP ?Hyp (In1r c2) s1 s2\<close>
with wt_c2 da_c2' G
obtain nrm_c2': "?NormalAssigned s2 C2'" and
brk_c2': "?BreakAssigned s1 s2 C2'" and
@@ -2797,7 +2797,7 @@
ultimately show ?thesis by (intro conjI)
next
case False
- with `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
+ with \<open>G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<close>
have eq_s1_s2: "s2=s1" by auto
with False have "?NormalAssigned s2 A" by blast
moreover
@@ -2824,7 +2824,7 @@
qed
next
case (If s0 e b s1 c1 c2 s2 Env T A)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
from If.prems
obtain E C1 C2 where
@@ -2920,7 +2920,7 @@
moreover
have "s2 = s1"
proof -
- from abr and `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
+ from abr and \<open>G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<close>
show ?thesis
by (cases s1) simp
qed
@@ -2928,7 +2928,7 @@
qed
next
case (Loop s0 e b s1 c s2 l s3 Env T A)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
by (simp (no_asm_simp))
from Loop.prems
@@ -3134,7 +3134,7 @@
ultimately show ?case by (intro conjI)
next
case (Throw s0 e a s1 Env T A)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from Throw.prems obtain E where
da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"
by (elim da_elim_cases)
@@ -3164,7 +3164,7 @@
ultimately show ?case by (intro conjI)
next
case (Try s0 c1 s1 s2 C vn c2 s3 Env T A)
- note G = `prg Env = G`
+ note G = \<open>prg Env = G\<close>
from Try.prems obtain C1 C2 where
da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and