src/HOL/NanoJava/AxSem.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 23894 1a4167d761ac
child 35431 8758fe1fc9f8
permissions -rw-r--r--
avoid rebinding of existing facts;
oheimb@11376
     1
(*  Title:      HOL/NanoJava/AxSem.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@11560
     7
header "Axiomatic Semantics"
oheimb@11376
     8
haftmann@16417
     9
theory AxSem imports State begin
oheimb@11376
    10
oheimb@11376
    11
types assn   = "state => bool"
oheimb@11486
    12
     vassn   = "val => assn"
oheimb@11476
    13
      triple = "assn \<times> stmt \<times>  assn"
oheimb@11476
    14
     etriple = "assn \<times> expr \<times> vassn"
oheimb@11376
    15
translations
oheimb@11376
    16
  "assn"   \<leftharpoondown> (type)"state => bool"
oheimb@11476
    17
 "vassn"   \<leftharpoondown> (type)"val => assn"
oheimb@11476
    18
  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times>  assn"
oheimb@11476
    19
 "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
oheimb@11376
    20
oheimb@11476
    21
oheimb@11560
    22
subsection "Hoare Logic Rules"
oheimb@11560
    23
berghofe@23755
    24
inductive
berghofe@23755
    25
 hoare :: "[triple set, triple set] => bool"  ("_ |\<turnstile>/ _" [61, 61] 60)
berghofe@23755
    26
 and ehoare :: "[triple set, etriple] => bool"  ("_ |\<turnstile>\<^sub>e/ _" [61, 61] 60)
berghofe@23755
    27
 and hoare1 :: "[triple set, assn,stmt,assn] => bool" 
berghofe@23755
    28
   ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
berghofe@23755
    29
 and ehoare1 :: "[triple set, assn,expr,vassn]=> bool"
berghofe@23755
    30
   ("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
berghofe@23755
    31
where
oheimb@11376
    32
berghofe@23755
    33
  "A  \<turnstile> {P}c{Q} \<equiv> A |\<turnstile> {(P,c,Q)}"
berghofe@23755
    34
| "A  \<turnstile>\<^sub>e {P}e{Q} \<equiv> A |\<turnstile>\<^sub>e (P,e,Q)"
oheimb@11476
    35
berghofe@23755
    36
| Skip:  "A \<turnstile> {P} Skip {P}"
berghofe@23755
    37
berghofe@23755
    38
| Comp: "[| A \<turnstile> {P} c1 {Q}; A \<turnstile> {Q} c2 {R} |] ==> A \<turnstile> {P} c1;;c2 {R}"
oheimb@11376
    39
berghofe@23755
    40
| Cond: "[| A \<turnstile>\<^sub>e {P} e {Q}; 
berghofe@23755
    41
            \<forall>v. A \<turnstile> {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
berghofe@23755
    42
            A \<turnstile> {P} If(e) c1 Else c2 {R}"
oheimb@11376
    43
berghofe@23755
    44
| Loop: "A \<turnstile> {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
berghofe@23755
    45
         A \<turnstile> {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
berghofe@23755
    46
berghofe@23755
    47
| LAcc: "A \<turnstile>\<^sub>e {\<lambda>s. P (s<x>) s} LAcc x {P}"
oheimb@11476
    48
berghofe@23755
    49
| LAss: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s.  Q (lupd(x\<mapsto>v) s)} ==>
berghofe@23755
    50
         A \<turnstile>  {P} x:==e {Q}"
berghofe@23755
    51
berghofe@23755
    52
| FAcc: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
berghofe@23755
    53
         A \<turnstile>\<^sub>e {P} e..f {Q}"
oheimb@11376
    54
berghofe@23755
    55
| FAss: "[| A \<turnstile>\<^sub>e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
berghofe@23755
    56
        \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
berghofe@23755
    57
            A \<turnstile>  {P} e1..f:==e2 {R}"
oheimb@11376
    58
berghofe@23755
    59
| NewC: "A \<turnstile>\<^sub>e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
oheimb@11476
    60
                new C {P}"
oheimb@11376
    61
berghofe@23755
    62
| Cast: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. (case v of Null => True 
oheimb@11476
    63
                                 | Addr a => obj_class s a <=C C) --> Q v s} ==>
berghofe@23755
    64
         A \<turnstile>\<^sub>e {P} Cast C e {Q}"
oheimb@11376
    65
berghofe@23755
    66
| Call: "[| A \<turnstile>\<^sub>e {P} e1 {Q}; \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {R a};
berghofe@23755
    67
    \<forall>a p ls. A \<turnstile> {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> 
oheimb@11772
    68
                    s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))}
oheimb@11565
    69
                  Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
berghofe@23755
    70
             A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}"
oheimb@11376
    71
berghofe@23755
    72
| Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> 
oheimb@11497
    73
                        P s \<and> s' = init_locs D m s}
oheimb@11497
    74
                  Impl (D,m) {Q} ==>
berghofe@23755
    75
             A \<turnstile> {P} Meth (C,m) {Q}"
oheimb@11376
    76
oheimb@11565
    77
  --{* @{text "\<Union>Z"} instead of @{text "\<forall>Z"} in the conclusion and\\
oheimb@11565
    78
       Z restricted to type state due to limitations of the inductive package *}
berghofe@23755
    79
| Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
oheimb@11565
    80
                            (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
berghofe@23755
    81
                      A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
oheimb@11376
    82
oheimb@11558
    83
--{* structural rules *}
oheimb@11376
    84
berghofe@23755
    85
| Asm:  "   a \<in> A ==> A |\<turnstile> {a}"
oheimb@11476
    86
berghofe@23755
    87
| ConjI: " \<forall>c \<in> C. A |\<turnstile> {c} ==> A |\<turnstile> C"
oheimb@11476
    88
berghofe@23755
    89
| ConjE: "[|A |\<turnstile> C; c \<in> C |] ==> A |\<turnstile> {c}"
oheimb@11476
    90
oheimb@11565
    91
  --{* Z restricted to type state due to limitations of the inductive package *}
berghofe@23755
    92
| Conseq:"[| \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z};
oheimb@11565
    93
             \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
berghofe@23755
    94
            A \<turnstile> {P} c {Q }"
oheimb@11376
    95
oheimb@11565
    96
  --{* Z restricted to type state due to limitations of the inductive package *}
berghofe@23755
    97
| eConseq:"[| \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
oheimb@11565
    98
             \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
berghofe@23755
    99
            A \<turnstile>\<^sub>e {P} e {Q }"
oheimb@11565
   100
oheimb@11565
   101
oheimb@12934
   102
subsection "Fully polymorphic variants, required for Example only"
oheimb@11376
   103
oheimb@11565
   104
axioms
oheimb@12934
   105
berghofe@23755
   106
  Conseq:"[| \<forall>Z. A \<turnstile> {P' Z} c {Q' Z};
oheimb@11565
   107
             \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
berghofe@23755
   108
                 A \<turnstile> {P} c {Q }"
oheimb@11565
   109
berghofe@23755
   110
 eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
oheimb@11565
   111
             \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
berghofe@23755
   112
                 A \<turnstile>\<^sub>e {P} e {Q }"
oheimb@11565
   113
berghofe@23755
   114
 Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
oheimb@11565
   115
                          (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
berghofe@23755
   116
                    A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
oheimb@11376
   117
oheimb@11376
   118
subsection "Derived Rules"
oheimb@11376
   119
oheimb@11376
   120
lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
oheimb@11476
   121
apply (rule hoare_ehoare.Conseq)
oheimb@11476
   122
apply  (rule allI, assumption)
oheimb@11476
   123
apply fast
oheimb@11476
   124
done
oheimb@11476
   125
oheimb@11476
   126
lemma Conseq2: "\<lbrakk>A \<turnstile> {P} c {Q'}; \<forall>t. Q' t \<longrightarrow> Q t\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
oheimb@11476
   127
apply (rule hoare_ehoare.Conseq)
oheimb@11476
   128
apply  (rule allI, assumption)
oheimb@11476
   129
apply fast
oheimb@11476
   130
done
oheimb@11476
   131
oheimb@11486
   132
lemma eConseq1: "\<lbrakk>A \<turnstile>\<^sub>e {P'} e {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
oheimb@11476
   133
apply (rule hoare_ehoare.eConseq)
oheimb@11476
   134
apply  (rule allI, assumption)
oheimb@11476
   135
apply fast
oheimb@11476
   136
done
oheimb@11476
   137
oheimb@11486
   138
lemma eConseq2: "\<lbrakk>A \<turnstile>\<^sub>e {P} e {Q'}; \<forall>v t. Q' v t \<longrightarrow> Q v t\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
oheimb@11476
   139
apply (rule hoare_ehoare.eConseq)
oheimb@11376
   140
apply  (rule allI, assumption)
oheimb@11376
   141
apply fast
oheimb@11376
   142
done
oheimb@11376
   143
oheimb@11376
   144
lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
oheimb@11476
   145
apply (rule hoare_ehoare.ConjI)
oheimb@11376
   146
apply clarify
oheimb@11476
   147
apply (drule hoare_ehoare.ConjE)
oheimb@11376
   148
apply  fast
oheimb@11376
   149
apply assumption
oheimb@11376
   150
done
oheimb@11376
   151
oheimb@11565
   152
lemma Thin_lemma: 
oheimb@11565
   153
  "(A' |\<turnstile>  C         \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile>  C       )) \<and> 
oheimb@11565
   154
   (A'  \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A  \<turnstile>\<^sub>e {P} e {Q}))"
oheimb@11565
   155
apply (rule hoare_ehoare.induct)
wenzelm@23894
   156
apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
oheimb@11565
   157
apply (blast intro: hoare_ehoare.Skip)
oheimb@11565
   158
apply (blast intro: hoare_ehoare.Comp)
oheimb@11565
   159
apply (blast intro: hoare_ehoare.Cond)
oheimb@11565
   160
apply (blast intro: hoare_ehoare.Loop)
oheimb@11565
   161
apply (blast intro: hoare_ehoare.LAcc)
oheimb@11565
   162
apply (blast intro: hoare_ehoare.LAss)
oheimb@11565
   163
apply (blast intro: hoare_ehoare.FAcc)
oheimb@11565
   164
apply (blast intro: hoare_ehoare.FAss)
oheimb@11565
   165
apply (blast intro: hoare_ehoare.NewC)
oheimb@11565
   166
apply (blast intro: hoare_ehoare.Cast)
oheimb@11565
   167
apply (erule hoare_ehoare.Call)
oheimb@11565
   168
apply   (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption)
oheimb@11565
   169
apply  blast
oheimb@11565
   170
apply (blast intro!: hoare_ehoare.Meth)
oheimb@11565
   171
apply (blast intro!: hoare_ehoare.Impl)
oheimb@11565
   172
apply (blast intro!: hoare_ehoare.Asm)
oheimb@11565
   173
apply (blast intro: hoare_ehoare.ConjI)
oheimb@11565
   174
apply (blast intro: hoare_ehoare.ConjE)
oheimb@11565
   175
apply (rule hoare_ehoare.Conseq)
oheimb@11565
   176
apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
oheimb@11565
   177
apply (rule hoare_ehoare.eConseq)
oheimb@11565
   178
apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
oheimb@11565
   179
done
oheimb@11565
   180
oheimb@11565
   181
lemma cThin: "\<lbrakk>A' |\<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
oheimb@11565
   182
by (erule (1) conjunct1 [OF Thin_lemma, rule_format])
oheimb@11565
   183
oheimb@11565
   184
lemma eThin: "\<lbrakk>A' \<turnstile>\<^sub>e {P} e {Q}; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
oheimb@11565
   185
by (erule (1) conjunct2 [OF Thin_lemma, rule_format])
oheimb@11565
   186
oheimb@11565
   187
oheimb@11565
   188
lemma Union: "A |\<turnstile> (\<Union>Z. C Z) = (\<forall>Z. A |\<turnstile> C Z)"
oheimb@11476
   189
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
oheimb@11376
   190
oheimb@11565
   191
lemma Impl1': 
oheimb@12934
   192
   "\<lbrakk>\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
oheimb@11565
   193
                 (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms; 
oheimb@11508
   194
    Cm \<in> Ms\<rbrakk> \<Longrightarrow> 
oheimb@11565
   195
                A   \<turnstile>  {P Z Cm} Impl Cm {Q Z Cm}"
oheimb@12934
   196
apply (drule AxSem.Impl)
oheimb@11376
   197
apply (erule Weaken)
oheimb@11376
   198
apply (auto del: image_eqI intro: rev_image_eqI)
oheimb@11376
   199
done
oheimb@11376
   200
oheimb@11565
   201
lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard]
oheimb@11565
   202
oheimb@11376
   203
end