src/HOL/NanoJava/Equivalence.thy
changeset 35355 613e133966ea
parent 27239 f2f42f9fa09d
child 35417 47ee18b6ae32
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Wed Feb 24 22:04:10 2010 +0100
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Feb 24 22:09:50 2010 +0100
     1.3 @@ -33,14 +33,14 @@
     1.4  cenvalid  :: "[triple set,etriple   ] => bool" ("_ ||=e/ _" [61,61] 60)
     1.5   "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
     1.6  
     1.7 -syntax (xsymbols)
     1.8 -   valid  :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
     1.9 -  evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    1.10 -  nvalid  :: "[nat, triple          ] => bool" ("\<Turnstile>_: _"  [61,61] 60)
    1.11 - envalid  :: "[nat,etriple          ] => bool" ("\<Turnstile>_:\<^sub>e _" [61,61] 60)
    1.12 -  nvalids :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
    1.13 - cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
    1.14 -cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
    1.15 +notation (xsymbols)
    1.16 +  valid  ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
    1.17 +  evalid  ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60) and
    1.18 +  nvalid  ("\<Turnstile>_: _" [61,61] 60) and
    1.19 +  envalid  ("\<Turnstile>_:\<^sub>e _" [61,61] 60) and
    1.20 +  nvalids  ("|\<Turnstile>_: _" [61,61] 60) and
    1.21 +  cnvalids  ("_ |\<Turnstile>/ _" [61,61] 60) and
    1.22 +  cenvalid  ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
    1.23  
    1.24  
    1.25  lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
    1.26 @@ -164,10 +164,10 @@
    1.27           "MGT  c Z \<equiv> (\<lambda>s. Z = s, c, \<lambda>  t. \<exists>n. Z -c-  n\<rightarrow> t)"
    1.28            MGTe   :: "expr => state => etriple"
    1.29           "MGTe e Z \<equiv> (\<lambda>s. Z = s, e, \<lambda>v t. \<exists>n. Z -e\<succ>v-n\<rightarrow> t)"
    1.30 -syntax (xsymbols)
    1.31 -         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
    1.32 -syntax (HTML output)
    1.33 -         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
    1.34 +notation (xsymbols)
    1.35 +  MGTe  ("MGT\<^sub>e")
    1.36 +notation (HTML output)
    1.37 +  MGTe  ("MGT\<^sub>e")
    1.38  
    1.39  lemma MGF_implies_complete:
    1.40   "\<forall>Z. {} |\<turnstile> { MGT c Z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"