src/HOL/NanoJava/Equivalence.thy
changeset 11376 bf98ad1c22c6
child 11476 06c1998340a8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Sat Jun 16 20:06:42 2001 +0200
     1.3 @@ -0,0 +1,237 @@
     1.4 +(*  Title:      HOL/NanoJava/Equivalence.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   2001 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +
    1.10 +header "Equivalence of Operational and Axiomatic Semantics"
    1.11 +
    1.12 +theory Equivalence = OpSem + AxSem:
    1.13 +
    1.14 +subsection "Validity"
    1.15 +
    1.16 +constdefs
    1.17 +  valid   :: "[assn,stmt,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    1.18 + "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c-n-> t) --> Q t"
    1.19 +
    1.20 + nvalid   :: "[nat,       triple    ] => bool" ("|=_: _"  [61,61] 60)
    1.21 + "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c-n-> t --> P s --> Q t"
    1.22 +
    1.23 + nvalids  :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
    1.24 + "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
    1.25 +
    1.26 + cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"[61,61] 60)
    1.27 + "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
    1.28 +
    1.29 +syntax (xsymbols)
    1.30 +  valid   :: "[assn,stmt,assn] => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    1.31 + nvalid   :: "[nat,       triple    ] => bool" ("\<Turnstile>_: _"   [61,61] 60)
    1.32 + nvalids  :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
    1.33 + cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
    1.34 +
    1.35 +syntax
    1.36 +  nvalid1::"[nat,        assn,stmt,assn] => bool" ( "|=_:.{(1_)}/ (_)/ {(1_)}"
    1.37 +                                                         [61,3,90,3] 60)
    1.38 + cnvalid1::"[triple set, assn,stmt,assn] => bool" ("_ ||=.{(1_)}/ (_)/ {(1_)}"
    1.39 +                                                         [61,3,90,3] 60)
    1.40 +syntax (xsymbols)
    1.41 +  nvalid1::"[nat,        assn,stmt,assn] => bool" (  "\<Turnstile>_:.{(1_)}/ (_)/ {(1_)}"
    1.42 +                                                         [61,3,90,3] 60)
    1.43 + cnvalid1::"[triple set, assn,stmt,assn] => bool" ( "_ |\<Turnstile>.{(1_)}/ (_)/ {(1_)}"
    1.44 +                                                         [61,3,90,3] 60)
    1.45 +translations
    1.46 + " \<Turnstile>n:.{P} c {Q}" \<rightleftharpoons> " \<Turnstile>n:  (P,c,Q)"
    1.47 + "A |\<Turnstile>.{P} c {Q}" \<rightleftharpoons> "A |\<Turnstile> {(P,c,Q)}"
    1.48 +
    1.49 +lemma nvalid1_def2: "\<Turnstile>n:.{P} c {Q} \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
    1.50 +by (simp add: nvalid_def Let_def)
    1.51 +
    1.52 +lemma cnvalid1_def2: 
    1.53 +  "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.54 +by(simp add: nvalid1_def2 nvalids_def cnvalids_def)
    1.55 +
    1.56 +lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n:.{P} c {Q})"
    1.57 +apply (simp add: valid_def nvalid1_def2)
    1.58 +apply blast
    1.59 +done
    1.60 +
    1.61 +
    1.62 +subsection "Soundness"
    1.63 +
    1.64 +declare exec_elim_cases [elim!]
    1.65 +
    1.66 +lemma Impl_nvalid_0: "\<Turnstile>0:.{P} Impl C m {Q}"
    1.67 +by (clarsimp simp add: nvalid1_def2)
    1.68 +
    1.69 +lemma Impl_nvalid_Suc: "\<Turnstile>n:.{P} body C m {Q} \<Longrightarrow> \<Turnstile>Suc n:.{P} Impl C m {Q}"
    1.70 +by (clarsimp simp add: nvalid1_def2)
    1.71 +
    1.72 +lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
    1.73 +by (force simp add: split_paired_all nvalid1_def2 intro: exec_mono)
    1.74 +
    1.75 +lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow>  Ball A (nvalid n)"
    1.76 +by (fast intro: nvalid_SucD)
    1.77 +
    1.78 +lemma Loop_sound_lemma [rule_format (no_asm)]: 
    1.79 +"\<lbrakk>\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<e> \<noteq> Null \<longrightarrow> P t; s -c0-n0\<rightarrow> t\<rbrakk> \<Longrightarrow> 
    1.80 +  P s \<longrightarrow> c0 = While (e) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<e> = Null"
    1.81 +apply (erule exec.induct)
    1.82 +apply clarsimp+
    1.83 +done
    1.84 +
    1.85 +lemma Impl_sound_lemma: 
    1.86 +"\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
    1.87 +          (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
    1.88 +by blast
    1.89 +
    1.90 +lemma hoare_sound_main: "A |\<turnstile> C \<Longrightarrow> A |\<Turnstile> C"
    1.91 +apply (erule hoare.induct)
    1.92 +apply (simp_all only: cnvalid1_def2)
    1.93 +apply clarsimp
    1.94 +apply clarsimp
    1.95 +apply (clarsimp split add: split_if_asm)
    1.96 +apply (clarsimp,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
    1.97 +apply clarsimp
    1.98 +apply clarsimp
    1.99 +apply clarsimp
   1.100 +apply clarsimp
   1.101 +apply (clarsimp del: Meth_elim_cases) (* Call *)
   1.102 +apply (clarsimp del: Impl_elim_cases) (* Meth *)
   1.103 +defer
   1.104 +apply blast (* Conseq *)
   1.105 +apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
   1.106 +apply blast
   1.107 +apply blast
   1.108 +apply blast
   1.109 +(* Impl *)
   1.110 +apply (erule thin_rl)
   1.111 +apply (rule allI)
   1.112 +apply (induct_tac "n")
   1.113 +apply  (clarify intro!: Impl_nvalid_0)
   1.114 +apply (clarify  intro!: Impl_nvalid_Suc)
   1.115 +apply (drule nvalids_SucD)
   1.116 +apply (erule (1) impE)
   1.117 +apply (drule (4) Impl_sound_lemma)
   1.118 +done
   1.119 +
   1.120 +theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
   1.121 +apply (simp only: valid_def2)
   1.122 +apply (drule hoare_sound_main)
   1.123 +apply (unfold cnvalids_def nvalids_def)
   1.124 +apply fast
   1.125 +done
   1.126 +
   1.127 +
   1.128 +subsection "(Relative) Completeness"
   1.129 +
   1.130 +constdefs MGT    :: "stmt => state => triple"
   1.131 +         "MGT c z \<equiv> (\<lambda> s. z = s, c, %t. \<exists>n. z -c-n-> t)"
   1.132 +
   1.133 +lemma MGF_implies_complete:
   1.134 + "\<forall>z. {} |\<turnstile> {MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
   1.135 +apply (simp only: valid_def2)
   1.136 +apply (unfold MGT_def)
   1.137 +apply (erule hoare.Conseq)
   1.138 +apply (clarsimp simp add: nvalid1_def2)
   1.139 +done
   1.140 +
   1.141 +
   1.142 +declare exec.intros[intro!]
   1.143 +
   1.144 +lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> 
   1.145 +  A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
   1.146 +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.147 +       in hoare.Conseq)
   1.148 +apply  (rule allI)
   1.149 +apply  (rule hoare.Loop)
   1.150 +apply  (erule hoare.Conseq)
   1.151 +apply  clarsimp
   1.152 +apply  (blast intro:rtrancl_into_rtrancl)
   1.153 +apply (erule thin_rl)
   1.154 +apply clarsimp
   1.155 +apply (erule_tac x = z in allE)
   1.156 +apply clarsimp
   1.157 +apply (erule converse_rtrancl_induct)
   1.158 +apply  blast
   1.159 +apply clarsimp
   1.160 +apply (drule (1) exec_max2)
   1.161 +apply (blast del: exec_elim_cases)
   1.162 +done
   1.163 +
   1.164 +lemma MGF_lemma[rule_format]:
   1.165 + "(\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z}) \<longrightarrow> (\<forall>z. A |\<turnstile> {MGT c z})"
   1.166 +apply (simp add: MGT_def)
   1.167 +apply (induct_tac c)
   1.168 +apply (tactic "ALLGOALS Clarify_tac")
   1.169 +
   1.170 +apply (rule Conseq1 [OF hoare.Skip])
   1.171 +apply blast
   1.172 +
   1.173 +apply (rule hoare.Comp)
   1.174 +apply  (erule spec)
   1.175 +apply (erule hoare.Conseq)
   1.176 +apply (erule thin_rl, erule thin_rl)
   1.177 +apply clarsimp
   1.178 +apply (drule (1) exec_max2)
   1.179 +apply blast
   1.180 +
   1.181 +apply (rule hoare.Cond)
   1.182 +apply  (erule hoare.Conseq)
   1.183 +apply  (erule thin_rl, erule thin_rl)
   1.184 +apply  force
   1.185 +apply (erule hoare.Conseq)
   1.186 +apply (erule thin_rl, erule thin_rl)
   1.187 +apply force
   1.188 +
   1.189 +apply (erule MGF_Loop)
   1.190 +
   1.191 +apply (rule Conseq1 [OF hoare.NewC])
   1.192 +apply blast
   1.193 +
   1.194 +apply (rule Conseq1 [OF hoare.Cast])
   1.195 +apply blast
   1.196 +
   1.197 +apply (rule Conseq1 [OF hoare.FAcc])
   1.198 +apply blast
   1.199 +
   1.200 +apply (rule Conseq1 [OF hoare.FAss])
   1.201 +apply blast
   1.202 +
   1.203 +apply (rule hoare.Call)
   1.204 +apply (rule allI)
   1.205 +apply (rule hoare.Meth)
   1.206 +apply (rule allI)
   1.207 +apply (drule spec, drule spec, erule hoare.Conseq)
   1.208 +apply blast
   1.209 +
   1.210 +apply (rule hoare.Meth)
   1.211 +apply (rule allI)
   1.212 +apply (drule spec, drule spec, erule hoare.Conseq)
   1.213 +apply blast
   1.214 +
   1.215 +apply blast
   1.216 +done
   1.217 +
   1.218 +lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
   1.219 +apply (unfold MGT_def)
   1.220 +apply (rule Impl1)
   1.221 +apply  (rule_tac [2] UNIV_I)
   1.222 +apply clarsimp
   1.223 +apply (rule hoare.ConjI)
   1.224 +apply clarsimp
   1.225 +apply (rule ssubst [OF Impl_body_eq])
   1.226 +apply (fold MGT_def)
   1.227 +apply (rule MGF_lemma)
   1.228 +apply (rule hoare.Asm)
   1.229 +apply force
   1.230 +done
   1.231 +
   1.232 +theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
   1.233 +apply (rule MGF_implies_complete)
   1.234 +apply  (erule_tac [2] asm_rl)
   1.235 +apply (rule allI)
   1.236 +apply (rule MGF_lemma)
   1.237 +apply (rule MGF_Impl)
   1.238 +done
   1.239 +
   1.240 +end