--- a/src/HOL/NanoJava/AxSem.thy Wed Dec 30 19:57:37 2015 +0100
+++ b/src/HOL/NanoJava/AxSem.thy Wed Dec 30 20:07:59 2015 +0100
@@ -58,7 +58,7 @@
new C {P}"
| Cast: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. (case v of Null => True
- | Addr a => obj_class s a <=C C) --> Q v s} ==>
+ | Addr a => obj_class s a \<preceq>C C) --> Q v s} ==>
A \<turnstile>\<^sub>e {P} Cast C e {Q}"
| Call: "[| A \<turnstile>\<^sub>e {P} e1 {Q}; \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {R a};
@@ -67,7 +67,7 @@
Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}"
-| Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and>
+| Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D \<preceq>C C \<and>
P s \<and> s' = init_locs D m s}
Impl (D,m) {Q} ==>
A \<turnstile> {P} Meth (C,m) {Q}"
--- a/src/HOL/NanoJava/Equivalence.thy Wed Dec 30 19:57:37 2015 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Wed Dec 30 20:07:59 2015 +0100
@@ -9,36 +9,26 @@
subsection "Validity"
-definition valid :: "[assn,stmt, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
- "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c -n\<rightarrow> t) --> Q t"
-
-definition evalid :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
- "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e\<succ>v-n\<rightarrow> t) --> Q v t"
+definition valid :: "[assn,stmt, assn] => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
+ "\<Turnstile> {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c -n\<rightarrow> t) --> Q t"
-definition nvalid :: "[nat, triple ] => bool" ("|=_: _" [61,61] 60) where
- "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c -n\<rightarrow> t --> P s --> Q t"
+definition evalid :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) where
+ "\<Turnstile>\<^sub>e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e\<succ>v-n\<rightarrow> t) --> Q v t"
-definition envalid :: "[nat,etriple ] => bool" ("|=_:e _" [61,61] 60) where
- "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e\<succ>v-n\<rightarrow> t --> P s --> Q v t"
-
-definition nvalids :: "[nat, triple set] => bool" ("||=_: _" [61,61] 60) where
- "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
+definition nvalid :: "[nat, triple ] => bool" ("\<Turnstile>_: _" [61,61] 60) where
+ "\<Turnstile>n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c -n\<rightarrow> t --> P s --> Q t"
-definition cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _" [61,61] 60) where
- "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
+definition envalid :: "[nat,etriple ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60) where
+ "\<Turnstile>n:\<^sub>e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e\<succ>v-n\<rightarrow> t --> P s --> Q v t"
-definition cenvalid :: "[triple set,etriple ] => bool" ("_ ||=e/ _" [61,61] 60) where
- "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
+definition nvalids :: "[nat, triple set] => bool" ("|\<Turnstile>_: _" [61,61] 60) where
+ "|\<Turnstile>n: T \<equiv> \<forall>t\<in>T. \<Turnstile>n: t"
-notation (xsymbols)
- valid ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
- evalid ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
- nvalid ("\<Turnstile>_: _" [61,61] 60) and
- envalid ("\<Turnstile>_:\<^sub>e _" [61,61] 60) and
- nvalids ("|\<Turnstile>_: _" [61,61] 60) and
- cnvalids ("_ |\<Turnstile>/ _" [61,61] 60) and
- cenvalid ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
+definition cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60) where
+ "A |\<Turnstile> C \<equiv> \<forall>n. |\<Turnstile>n: A --> |\<Turnstile>n: C"
+definition cenvalid :: "[triple set,etriple ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60) where
+ "A |\<Turnstile>\<^sub>e t \<equiv> \<forall>n. |\<Turnstile>n: A --> \<Turnstile>n:\<^sub>e t"
lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
by (simp add: nvalid_def Let_def)
@@ -160,11 +150,8 @@
definition MGT :: "stmt => state => triple" where
"MGT c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda> t. \<exists>n. Z -c- n\<rightarrow> t)"
-definition MGTe :: "expr => state => etriple" where
- "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
-
-notation (xsymbols)
- MGTe ("MGT\<^sub>e")
+definition MGT\<^sub>e :: "expr => state => etriple" where
+ "MGT\<^sub>e e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
lemma MGF_implies_complete:
"\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
@@ -177,7 +164,7 @@
lemma eMGF_implies_complete:
"\<forall>Z. {} |\<turnstile>\<^sub>e MGT\<^sub>e e Z \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
apply (simp only: evalid_def2)
-apply (unfold MGTe_def)
+apply (unfold MGT\<^sub>e_def)
apply (erule hoare_ehoare.eConseq)
apply (clarsimp simp add: envalid_def2)
done
@@ -206,7 +193,7 @@
lemma MGF_lemma: "\<forall>M Z. A |\<turnstile> {MGT (Impl M) Z} \<Longrightarrow>
(\<forall>Z. A |\<turnstile> {MGT c Z}) \<and> (\<forall>Z. A |\<turnstile>\<^sub>e MGT\<^sub>e e Z)"
-apply (simp add: MGT_def MGTe_def)
+apply (simp add: MGT_def MGT\<^sub>e_def)
apply (rule stmt_expr.induct)
apply (rule_tac [!] allI)
--- a/src/HOL/NanoJava/State.thy Wed Dec 30 19:57:37 2015 +0100
+++ b/src/HOL/NanoJava/State.thy Wed Dec 30 20:07:59 2015 +0100
@@ -70,16 +70,12 @@
"get_field s a f \<equiv> the (snd (get_obj s a) f)"
--{* local function: *}
-definition hupd :: "loc => obj => state => state" ("hupd'(_|->_')" [10,10] 1000) where
+definition hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000) where
"hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)"
-definition lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000) where
+definition lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000) where
"lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)"
-notation (xsymbols)
- hupd ("hupd'(_\<mapsto>_')" [10,10] 1000) and
- lupd ("lupd'(_\<mapsto>_')" [10,10] 1000)
-
definition new_obj :: "loc => cname => state => state" where
"new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
--- a/src/HOL/NanoJava/TypeRel.thy Wed Dec 30 19:57:37 2015 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Wed Dec 30 20:07:59 2015 +0100
@@ -15,15 +15,11 @@
"subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
abbreviation
- subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
- where "C <=C1 D == (C,D) \<in> subcls1"
+ subcls1_syntax :: "[cname, cname] => bool" ("_ \<prec>C1 _" [71,71] 70)
+ where "C \<prec>C1 D == (C,D) \<in> subcls1"
abbreviation
- subcls_syntax :: "[cname, cname] => bool" ("_ <=C _" [71,71] 70)
- where "C <=C D == (C,D) \<in> subcls1^*"
-
-notation (xsymbols)
- subcls1_syntax ("_ \<prec>C1 _" [71,71] 70) and
- subcls_syntax ("_ \<preceq>C _" [71,71] 70)
+ subcls_syntax :: "[cname, cname] => bool" ("_ \<preceq>C _" [71,71] 70)
+ where "C \<preceq>C D == (C,D) \<in> subcls1^*"
subsection "Declarations and properties not used in the meta theory"