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