src/HOL/NanoJava/Equivalence.thy
changeset 11486 8f32860eac3a
parent 11476 06c1998340a8
child 11497 0e66e0114d9a
     1.1 --- a/src/HOL/NanoJava/Equivalence.thy	Wed Aug 08 15:16:38 2001 +0200
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Wed Aug 08 16:57:43 2001 +0200
     1.3 @@ -35,12 +35,12 @@
     1.4  
     1.5  syntax (xsymbols)
     1.6     valid  :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
     1.7 -  evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
     1.8 +  evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>\<^sub>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
     1.9    nvalid  :: "[nat, triple          ] => bool" ("\<Turnstile>_: _"  [61,61] 60)
    1.10 - envalid  :: "[nat,etriple          ] => bool" ("\<Turnstile>_:e _" [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>e/ _"[61,61] 60)
    1.15 +cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>\<^sub>e/ _"[61,61] 60)
    1.16  
    1.17  
    1.18  lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
    1.19 @@ -51,16 +51,16 @@
    1.20  apply blast
    1.21  done
    1.22  
    1.23 -lemma envalid_def2: "\<Turnstile>n:e (P,e,Q) \<equiv> \<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t"
    1.24 +lemma envalid_def2: "\<Turnstile>n:\<^sub>e (P,e,Q) \<equiv> \<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t"
    1.25  by (simp add: envalid_def Let_def)
    1.26  
    1.27 -lemma evalid_def2: "\<Turnstile>e {P} e {Q} = (\<forall>n. \<Turnstile>n:e (P,e,Q))"
    1.28 +lemma evalid_def2: "\<Turnstile>\<^sub>e {P} e {Q} = (\<forall>n. \<Turnstile>n:\<^sub>e (P,e,Q))"
    1.29  apply (simp add: evalid_def envalid_def2)
    1.30  apply blast
    1.31  done
    1.32  
    1.33  lemma cenvalid_def2: 
    1.34 -  "A|\<Turnstile>e (P,e,Q) = (\<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t))"
    1.35 +  "A|\<Turnstile>\<^sub>e (P,e,Q) = (\<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s v t. s -e\<succ>v-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q v t))"
    1.36  by(simp add: cenvalid_def envalid_def2) 
    1.37  
    1.38  
    1.39 @@ -103,7 +103,7 @@
    1.40    "A |\<Turnstile> {(P,c,Q)} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
    1.41  by(simp add: cnvalids_def nvalids_def nvalid_def2)
    1.42  
    1.43 -lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>e t \<longrightarrow> A |\<Turnstile>e t)"
    1.44 +lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>\<^sub>e t \<longrightarrow> A |\<Turnstile>\<^sub>e t)"
    1.45  apply (tactic "split_all_tac 1", rename_tac P e Q)
    1.46  apply (rule hoare_ehoare.induct)
    1.47  apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
    1.48 @@ -149,7 +149,7 @@
    1.49  apply fast
    1.50  done
    1.51  
    1.52 -theorem ehoare_sound: "{} \<turnstile>e {P} e {Q} \<Longrightarrow> \<Turnstile>e {P} e {Q}"
    1.53 +theorem ehoare_sound: "{} \<turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q}"
    1.54  apply (simp only: evalid_def2)
    1.55  apply (drule hoare_sound_main [THEN conjunct2, rule_format])
    1.56  apply (unfold cenvalid_def nvalids_def)
    1.57 @@ -160,9 +160,11 @@
    1.58  subsection "(Relative) Completeness"
    1.59  
    1.60  constdefs MGT    :: "stmt => state =>  triple"
    1.61 -         "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda>  t. \<exists>n. z -c-  n-> t)"
    1.62 -         eMGT    :: "expr => state => etriple"
    1.63 -        "eMGT e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
    1.64 +         "MGT  c z \<equiv> (\<lambda>s. z = s, c, \<lambda>  t. \<exists>n. z -c-  n-> t)"
    1.65 +          MGTe   :: "expr => state => etriple"
    1.66 +         "MGTe e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
    1.67 +syntax (xsymbols)
    1.68 +         MGTe    :: "expr => state => etriple" ("MGT\<^sub>e")
    1.69  
    1.70  lemma MGF_implies_complete:
    1.71   "\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
    1.72 @@ -173,9 +175,9 @@
    1.73  done
    1.74  
    1.75  lemma eMGF_implies_complete:
    1.76 - "\<forall>z. {} |\<turnstile>e eMGT e z \<Longrightarrow> \<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
    1.77 + "\<forall>z. {} |\<turnstile>\<^sub>e MGT\<^sub>e e z \<Longrightarrow> \<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
    1.78  apply (simp only: evalid_def2)
    1.79 -apply (unfold eMGT_def)
    1.80 +apply (unfold MGTe_def)
    1.81  apply (erule hoare_ehoare.eConseq)
    1.82  apply (clarsimp simp add: envalid_def2)
    1.83  done
    1.84 @@ -183,8 +185,8 @@
    1.85  declare exec_eval.intros[intro!]
    1.86  
    1.87  lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> 
    1.88 -  A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
    1.89 -apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
    1.90 +  A \<turnstile> {op = z} While (x) c {\<lambda>t. \<exists>n. z -While (x) c-n\<rightarrow> t}"
    1.91 +apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<x> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
    1.92         in hoare_ehoare.Conseq)
    1.93  apply  (rule allI)
    1.94  apply  (rule hoare_ehoare.Loop)
    1.95 @@ -203,8 +205,8 @@
    1.96  done
    1.97  
    1.98  lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> 
    1.99 - (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>e eMGT e z)"
   1.100 -apply (simp add: MGT_def eMGT_def)
   1.101 + (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)"
   1.102 +apply (simp add: MGT_def MGTe_def)
   1.103  apply (rule stmt_expr.induct)
   1.104  apply (rule_tac [!] allI)
   1.105  
   1.106 @@ -301,7 +303,7 @@
   1.107  apply (rule MGF_Impl)
   1.108  done
   1.109  
   1.110 -theorem ehoare_relative_complete: "\<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
   1.111 +theorem ehoare_relative_complete: "\<Turnstile>\<^sub>e {P} e {Q} \<Longrightarrow> {} \<turnstile>\<^sub>e {P} e {Q}"
   1.112  apply (rule eMGF_implies_complete)
   1.113  apply  (erule_tac [2] asm_rl)
   1.114  apply (rule allI)