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