# HG changeset patch
# User wenzelm
# Date 1451502479 -3600
# Node ID 39e4a93ad36e11751b0fe4108fb18f926512144b
# Parent  ba8c284d47251a49482d7b5539513e1fcbf8c5bb
more symbols;

diff -r ba8c284d4725 -r 39e4a93ad36e src/HOL/NanoJava/AxSem.thy
--- 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}"
diff -r ba8c284d4725 -r 39e4a93ad36e src/HOL/NanoJava/Equivalence.thy
--- 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)
 
diff -r ba8c284d4725 -r 39e4a93ad36e src/HOL/NanoJava/State.thy
--- 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)))"
 
diff -r ba8c284d4725 -r 39e4a93ad36e src/HOL/NanoJava/TypeRel.thy
--- 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"