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