src/HOL/NanoJava/Equivalence.thy
author oheimb
Wed Aug 08 12:36:48 2001 +0200 (2001-08-08)
changeset 11476 06c1998340a8
parent 11376 bf98ad1c22c6
child 11486 8f32860eac3a
permissions -rw-r--r--
changed to full expressions with side effects
     1 (*  Title:      HOL/NanoJava/Equivalence.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   2001 Technische Universitaet Muenchen
     5 *)
     6 
     7 header "Equivalence of Operational and Axiomatic Semantics"
     8 
     9 theory Equivalence = OpSem + AxSem:
    10 
    11 subsection "Validity"
    12 
    13 constdefs
    14   valid   :: "[assn,stmt, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    15  "|=  {P} c {Q} \<equiv> \<forall>s   t. P s --> (\<exists>n. s -c  -n-> t) --> Q   t"
    16 
    17  evalid   :: "[assn,expr,vassn] => bool" ("|=e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    18  "|=e {P} e {Q} \<equiv> \<forall>s v t. P s --> (\<exists>n. s -e>v-n-> t) --> Q v t"
    19 
    20 
    21  nvalid   :: "[nat, triple    ] => bool" ("|=_: _"  [61,61] 60)
    22  "|=n:  t \<equiv> let (P,c,Q) = t in \<forall>s   t. s -c  -n-> t --> P s --> Q   t"
    23 
    24 envalid   :: "[nat,etriple    ] => bool" ("|=_:e _" [61,61] 60)
    25  "|=n:e t \<equiv> let (P,e,Q) = t in \<forall>s v t. s -e>v-n-> t --> P s --> Q v t"
    26 
    27   nvalids :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
    28  "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
    29 
    30  cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"  [61,61] 60)
    31  "A ||=  C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
    32 
    33 cenvalid  :: "[triple set,etriple   ] => bool" ("_ ||=e/ _" [61,61] 60)
    34  "A ||=e t \<equiv> \<forall>n. ||=n: A --> |=n:e t"
    35 
    36 syntax (xsymbols)
    37    valid  :: "[assn,stmt, assn] => bool" ( "\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    38   evalid  :: "[assn,expr,vassn] => bool" ("\<Turnstile>e {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
    39   nvalid  :: "[nat, triple          ] => bool" ("\<Turnstile>_: _"  [61,61] 60)
    40  envalid  :: "[nat,etriple          ] => bool" ("\<Turnstile>_:e _" [61,61] 60)
    41   nvalids :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
    42  cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
    43 cenvalid  :: "[triple set,etriple   ] => bool" ("_ |\<Turnstile>e/ _"[61,61] 60)
    44 
    45 
    46 lemma nvalid_def2: "\<Turnstile>n: (P,c,Q) \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
    47 by (simp add: nvalid_def Let_def)
    48 
    49 lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n: (P,c,Q))"
    50 apply (simp add: valid_def nvalid_def2)
    51 apply blast
    52 done
    53 
    54 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"
    55 by (simp add: envalid_def Let_def)
    56 
    57 lemma evalid_def2: "\<Turnstile>e {P} e {Q} = (\<forall>n. \<Turnstile>n:e (P,e,Q))"
    58 apply (simp add: evalid_def envalid_def2)
    59 apply blast
    60 done
    61 
    62 lemma cenvalid_def2: 
    63   "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))"
    64 by(simp add: cenvalid_def envalid_def2) 
    65 
    66 
    67 subsection "Soundness"
    68 
    69 declare exec_elim_cases [elim!] eval_elim_cases [elim!]
    70 
    71 lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl C m,Q)"
    72 by (clarsimp simp add: nvalid_def2)
    73 
    74 lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body C m,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl C m,Q)"
    75 by (clarsimp simp add: nvalid_def2)
    76 
    77 lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
    78 by (force simp add: split_paired_all nvalid_def2 intro: exec_mono)
    79 
    80 lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow>  Ball A (nvalid n)"
    81 by (fast intro: nvalid_SucD)
    82 
    83 lemma Loop_sound_lemma [rule_format (no_asm)]: 
    84 "\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<x> \<noteq> Null \<longrightarrow> P t \<Longrightarrow> 
    85   (s -c0-n0\<rightarrow> t \<longrightarrow> P s \<longrightarrow> c0 = While (x) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<x> = Null)"
    86 apply (rule_tac "P2.1"="%s e v n t. True" in exec_eval.induct [THEN conjunct1])
    87 apply clarsimp+
    88 done
    89 
    90 lemma Impl_sound_lemma: 
    91 "\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
    92           (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
    93 by blast
    94 
    95 lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
    96 by fast
    97 
    98 lemma all3_conjunct2: 
    99   "\<forall>a p l. (P' a p l \<and> P a p l) \<Longrightarrow> \<forall>a p l. P a p l"
   100 by fast
   101 
   102 lemma cnvalid1_eq: 
   103   "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)"
   104 by(simp add: cnvalids_def nvalids_def nvalid_def2)
   105 
   106 lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>e t \<longrightarrow> A |\<Turnstile>e t)"
   107 apply (tactic "split_all_tac 1", rename_tac P e Q)
   108 apply (rule hoare_ehoare.induct)
   109 apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [thm "all_conjunct2", thm "all3_conjunct2"]) *})
   110 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x :  hoare") *})
   111 apply (tactic {* ALLGOALS (REPEAT o thin_tac "?x : ehoare") *})
   112 apply (simp_all only: cnvalid1_eq cenvalid_def2)
   113 apply fast
   114 apply fast
   115 apply fast
   116 apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
   117 apply fast
   118 apply fast
   119 apply fast
   120 apply fast
   121 apply fast
   122 apply fast
   123 apply (clarsimp del: Meth_elim_cases) (* Call *)
   124 apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
   125 apply (tactic "smp_tac 2 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
   126 apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast)
   127 apply (clarsimp del: Impl_elim_cases) (* Meth *)
   128 defer
   129 prefer 4 apply blast (*  Conseq *)
   130 prefer 4 apply blast (* eConseq *)
   131 apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
   132 apply blast
   133 apply blast
   134 apply blast
   135 (* Impl *)
   136 apply (rule allI)
   137 apply (induct_tac "n")
   138 apply  (clarify intro!: Impl_nvalid_0)
   139 apply (clarify  intro!: Impl_nvalid_Suc)
   140 apply (drule nvalids_SucD)
   141 apply (erule (1) impE)
   142 apply (drule (4) Impl_sound_lemma)
   143 done
   144 
   145 theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
   146 apply (simp only: valid_def2)
   147 apply (drule hoare_sound_main [THEN conjunct1, rule_format])
   148 apply (unfold cnvalids_def nvalids_def)
   149 apply fast
   150 done
   151 
   152 theorem ehoare_sound: "{} \<turnstile>e {P} e {Q} \<Longrightarrow> \<Turnstile>e {P} e {Q}"
   153 apply (simp only: evalid_def2)
   154 apply (drule hoare_sound_main [THEN conjunct2, rule_format])
   155 apply (unfold cenvalid_def nvalids_def)
   156 apply fast
   157 done
   158 
   159 
   160 subsection "(Relative) Completeness"
   161 
   162 constdefs MGT    :: "stmt => state =>  triple"
   163          "MGT c z \<equiv> (\<lambda>s. z = s, c, \<lambda>  t. \<exists>n. z -c-  n-> t)"
   164          eMGT    :: "expr => state => etriple"
   165         "eMGT e z \<equiv> (\<lambda>s. z = s, e, \<lambda>v t. \<exists>n. z -e>v-n-> t)"
   166 
   167 lemma MGF_implies_complete:
   168  "\<forall>z. {} |\<turnstile> { MGT c z} \<Longrightarrow> \<Turnstile>  {P} c {Q} \<Longrightarrow> {} \<turnstile>  {P} c {Q}"
   169 apply (simp only: valid_def2)
   170 apply (unfold MGT_def)
   171 apply (erule hoare_ehoare.Conseq)
   172 apply (clarsimp simp add: nvalid_def2)
   173 done
   174 
   175 lemma eMGF_implies_complete:
   176  "\<forall>z. {} |\<turnstile>e eMGT e z \<Longrightarrow> \<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
   177 apply (simp only: evalid_def2)
   178 apply (unfold eMGT_def)
   179 apply (erule hoare_ehoare.eConseq)
   180 apply (clarsimp simp add: envalid_def2)
   181 done
   182 
   183 declare exec_eval.intros[intro!]
   184 
   185 lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> 
   186   A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
   187 apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
   188        in hoare_ehoare.Conseq)
   189 apply  (rule allI)
   190 apply  (rule hoare_ehoare.Loop)
   191 apply  (erule hoare_ehoare.Conseq)
   192 apply  clarsimp
   193 apply  (blast intro:rtrancl_into_rtrancl)
   194 apply (erule thin_rl)
   195 apply clarsimp
   196 apply (erule_tac x = z in allE)
   197 apply clarsimp
   198 apply (erule converse_rtrancl_induct)
   199 apply  blast
   200 apply clarsimp
   201 apply (drule (1) exec_exec_max)
   202 apply (blast del: exec_elim_cases)
   203 done
   204 
   205 lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow> 
   206  (\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>e eMGT e z)"
   207 apply (simp add: MGT_def eMGT_def)
   208 apply (rule stmt_expr.induct)
   209 apply (rule_tac [!] allI)
   210 
   211 apply (rule Conseq1 [OF hoare_ehoare.Skip])
   212 apply blast
   213 
   214 apply (rule hoare_ehoare.Comp)
   215 apply  (erule spec)
   216 apply (erule hoare_ehoare.Conseq)
   217 apply clarsimp
   218 apply (drule (1) exec_exec_max)
   219 apply blast
   220 
   221 apply (erule thin_rl)
   222 apply (rule hoare_ehoare.Cond)
   223 apply  (erule spec)
   224 apply (rule allI)
   225 apply (simp)
   226 apply (rule conjI)
   227 apply  (rule impI, erule hoare_ehoare.Conseq, clarsimp, drule (1) eval_exec_max,
   228         erule thin_rl, erule thin_rl, force)+
   229 
   230 apply (erule MGF_Loop)
   231 
   232 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.LAss])
   233 apply fast
   234 
   235 apply (erule thin_rl)
   236 apply (rule_tac Q = "\<lambda>a s. \<exists>n. z -expr1\<succ>Addr a-n\<rightarrow> s" in hoare_ehoare.FAss)
   237 apply  (drule spec)
   238 apply  (erule eConseq2)
   239 apply  fast
   240 apply (rule allI)
   241 apply (erule hoare_ehoare.eConseq)
   242 apply clarsimp
   243 apply (drule (1) eval_eval_max)
   244 apply blast
   245 
   246 apply (rule hoare_ehoare.Meth)
   247 apply (rule allI)
   248 apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
   249 apply blast
   250 
   251 apply blast
   252 
   253 apply (rule eConseq1 [OF hoare_ehoare.NewC])
   254 apply blast
   255 
   256 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.Cast])
   257 apply fast
   258 
   259 apply (rule eConseq1 [OF hoare_ehoare.LAcc])
   260 apply blast
   261 
   262 apply (erule hoare_ehoare.eConseq [THEN hoare_ehoare.FAcc])
   263 apply fast
   264 
   265 apply (rule_tac R = "\<lambda>a v s. \<exists>n1 n2 t. z -expr1\<succ>a-n1\<rightarrow> t \<and> t -expr2\<succ>v-n2\<rightarrow> s" in
   266                 hoare_ehoare.Call)
   267 apply   (erule spec)
   268 apply  (rule allI)
   269 apply  (erule hoare_ehoare.eConseq)
   270 apply  clarsimp
   271 apply  blast
   272 apply (rule allI)+
   273 apply (rule hoare_ehoare.Meth)
   274 apply (rule allI)
   275 apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
   276 apply (erule thin_rl, erule thin_rl)
   277 apply (clarsimp del: Impl_elim_cases)
   278 apply (drule (2) eval_eval_exec_max)
   279 apply (fast del: Impl_elim_cases)
   280 done
   281 
   282 lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
   283 apply (unfold MGT_def)
   284 apply (rule Impl1)
   285 apply  (rule_tac [2] UNIV_I)
   286 apply clarsimp
   287 apply (rule hoare_ehoare.ConjI)
   288 apply clarsimp
   289 apply (rule ssubst [OF Impl_body_eq])
   290 apply (fold MGT_def)
   291 apply (rule MGF_lemma [THEN conjunct1, rule_format])
   292 apply (rule hoare_ehoare.Asm)
   293 apply force
   294 done
   295 
   296 theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
   297 apply (rule MGF_implies_complete)
   298 apply  (erule_tac [2] asm_rl)
   299 apply (rule allI)
   300 apply (rule MGF_lemma [THEN conjunct1, rule_format])
   301 apply (rule MGF_Impl)
   302 done
   303 
   304 theorem ehoare_relative_complete: "\<Turnstile>e {P} e {Q} \<Longrightarrow> {} \<turnstile>e {P} e {Q}"
   305 apply (rule eMGF_implies_complete)
   306 apply  (erule_tac [2] asm_rl)
   307 apply (rule allI)
   308 apply (rule MGF_lemma [THEN conjunct2, rule_format])
   309 apply (rule MGF_Impl)
   310 done
   311 
   312 end