src/HOL/NanoJava/AxSem.thy
author oheimb
Wed Aug 08 12:36:48 2001 +0200 (2001-08-08)
changeset 11476 06c1998340a8
parent 11449 d25be0ad1a6c
child 11486 8f32860eac3a
permissions -rw-r--r--
changed to full expressions with side effects
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@11376
     7
header "Axiomatic Semantics (Hoare Logic)"
oheimb@11376
     8
oheimb@11376
     9
theory AxSem = State:
oheimb@11376
    10
oheimb@11376
    11
types assn   = "state => bool"
oheimb@11476
    12
     vassn   = "val \<Rightarrow> 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
consts   hoare   :: "(triple set \<times>  triple set) set"
oheimb@11476
    22
consts  ehoare   :: "(triple set \<times> etriple    ) set"
oheimb@11376
    23
syntax (xsymbols)
oheimb@11376
    24
 "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
oheimb@11376
    25
 "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
oheimb@11376
    26
                                   ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
oheimb@11476
    27
"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ |\<turnstile>e/ _"[61,61]60)
oheimb@11476
    28
"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
oheimb@11476
    29
                                  ("_ \<turnstile>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
oheimb@11376
    30
syntax
oheimb@11376
    31
 "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
oheimb@11376
    32
 "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
oheimb@11376
    33
                                  ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
oheimb@11476
    34
"@ehoare"  :: "[triple set,  etriple       ] => bool" ("_ ||-e/ _"[61,61] 60)
oheimb@11476
    35
"@ehoare1" :: "[triple set,  assn,expr,vassn]=> bool"
oheimb@11476
    36
                                 ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
oheimb@11376
    37
oheimb@11476
    38
translations "A |\<turnstile> C"        \<rightleftharpoons> "(A,C) \<in> hoare"
oheimb@11476
    39
             "A  \<turnstile> {P}c{Q}"  \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
oheimb@11476
    40
             "A |\<turnstile>e t"       \<rightleftharpoons> "(A,t) \<in> ehoare"
oheimb@11476
    41
             "A |\<turnstile>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (** shouldn't be necess.**)
oheimb@11476
    42
             "A  \<turnstile>e{P}e{Q}"  \<rightleftharpoons> "A |\<turnstile>e (P,e,Q)"
oheimb@11376
    43
oheimb@11476
    44
oheimb@11476
    45
inductive hoare ehoare
oheimb@11376
    46
intros
oheimb@11376
    47
oheimb@11376
    48
  Skip:  "A |- {P} Skip {P}"
oheimb@11376
    49
oheimb@11376
    50
  Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
oheimb@11376
    51
oheimb@11476
    52
  Cond: "[| A |-e {P} e {Q}; 
oheimb@11476
    53
            \<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
oheimb@11476
    54
            A |- {P} If(e) c1 Else c2 {R}"
oheimb@11476
    55
oheimb@11476
    56
  Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
oheimb@11476
    57
         A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
oheimb@11376
    58
oheimb@11476
    59
  LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}"
oheimb@11376
    60
oheimb@11476
    61
  LAss: "A |-e {P} e {\<lambda>v s.  Q (lupd(x\<mapsto>v) s)} ==>
oheimb@11476
    62
         A |-  {P} x:==e {Q}"
oheimb@11476
    63
oheimb@11476
    64
  FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
oheimb@11476
    65
         A |-e {P} e..f {Q}"
oheimb@11376
    66
oheimb@11476
    67
  FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
oheimb@11476
    68
        \<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
oheimb@11476
    69
            A |-  {P} e1..f:==e2 {R}"
oheimb@11376
    70
oheimb@11476
    71
  NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
oheimb@11476
    72
                new C {P}"
oheimb@11376
    73
oheimb@11476
    74
  Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True 
oheimb@11476
    75
                                 | Addr a => obj_class s a <=C C) --> Q v s} ==>
oheimb@11476
    76
         A |-e {P} Cast C e {Q}"
oheimb@11376
    77
oheimb@11476
    78
  Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
oheimb@11476
    79
    \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> 
oheimb@11476
    80
                    s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s))}
oheimb@11476
    81
                  Meth C m {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
oheimb@11476
    82
             A |-e {P} {C}e1..m(e2) {S}"
oheimb@11376
    83
oheimb@11376
    84
  Meth: "\<forall>D. A |- {\<lambda>s. \<exists>a. s<This> = Addr a \<and> D=obj_class s a \<and> D <=C C \<and> P s}
oheimb@11376
    85
                  Impl D m {Q} ==>
oheimb@11376
    86
             A |- {P} Meth C m {Q}"
oheimb@11376
    87
oheimb@11376
    88
  (*\<Union>z instead of \<forall>z in the conclusion and
oheimb@11476
    89
      z restricted to type state due to limitations of the inductive package *)
oheimb@11376
    90
  Impl: "A\<union>   (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||- 
oheimb@11376
    91
               (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
oheimb@11376
    92
         A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
oheimb@11376
    93
oheimb@11376
    94
(* structural rules *)
oheimb@11376
    95
oheimb@11476
    96
  Asm:  "   a \<in> A ==> A ||- {a}"
oheimb@11476
    97
oheimb@11476
    98
  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
oheimb@11476
    99
oheimb@11476
   100
  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
oheimb@11476
   101
oheimb@11476
   102
  (* z restricted to type state due to limitations of the inductive package *)
oheimb@11376
   103
  Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
oheimb@11376
   104
             \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
oheimb@11376
   105
            A |- {P} c {Q }"
oheimb@11376
   106
oheimb@11476
   107
  (* z restricted to type state due to limitations of the inductive package *)
oheimb@11476
   108
 eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
oheimb@11476
   109
             \<forall>s v t. (\<forall>z::state. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
oheimb@11476
   110
            A |-e {P} c {Q }"
oheimb@11376
   111
oheimb@11376
   112
oheimb@11376
   113
subsection "Derived Rules"
oheimb@11376
   114
oheimb@11376
   115
lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
oheimb@11476
   116
apply (rule hoare_ehoare.Conseq)
oheimb@11476
   117
apply  (rule allI, assumption)
oheimb@11476
   118
apply fast
oheimb@11476
   119
done
oheimb@11476
   120
oheimb@11476
   121
lemma Conseq2: "\<lbrakk>A \<turnstile> {P} c {Q'}; \<forall>t. Q' t \<longrightarrow> Q t\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
oheimb@11476
   122
apply (rule hoare_ehoare.Conseq)
oheimb@11476
   123
apply  (rule allI, assumption)
oheimb@11476
   124
apply fast
oheimb@11476
   125
done
oheimb@11476
   126
oheimb@11476
   127
lemma eConseq1: "\<lbrakk>A \<turnstile>e {P'} e {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile>e {P} e {Q}"
oheimb@11476
   128
apply (rule hoare_ehoare.eConseq)
oheimb@11476
   129
apply  (rule allI, assumption)
oheimb@11476
   130
apply fast
oheimb@11476
   131
done
oheimb@11476
   132
oheimb@11476
   133
lemma eConseq2: "\<lbrakk>A \<turnstile>e {P} e {Q'}; \<forall>v t. Q' v t \<longrightarrow> Q v t\<rbrakk> \<Longrightarrow> A \<turnstile>e {P} e {Q}"
oheimb@11476
   134
apply (rule hoare_ehoare.eConseq)
oheimb@11376
   135
apply  (rule allI, assumption)
oheimb@11376
   136
apply fast
oheimb@11376
   137
done
oheimb@11376
   138
oheimb@11376
   139
lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
oheimb@11476
   140
apply (rule hoare_ehoare.ConjI)
oheimb@11376
   141
apply clarify
oheimb@11476
   142
apply (drule hoare_ehoare.ConjE)
oheimb@11376
   143
apply  fast
oheimb@11376
   144
apply assumption
oheimb@11376
   145
done
oheimb@11376
   146
oheimb@11376
   147
lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
oheimb@11476
   148
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
oheimb@11376
   149
oheimb@11376
   150
lemma Impl': 
oheimb@11449
   151
  "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
oheimb@11376
   152
                (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
oheimb@11449
   153
       A    ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
oheimb@11376
   154
apply (drule Union[THEN iffD2])
oheimb@11476
   155
apply (drule hoare_ehoare.Impl)
oheimb@11376
   156
apply (drule Union[THEN iffD1])
oheimb@11376
   157
apply (erule spec)
oheimb@11376
   158
done
oheimb@11376
   159
oheimb@11376
   160
lemma Impl1: 
oheimb@11449
   161
   "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
oheimb@11376
   162
                 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms; 
oheimb@11449
   163
    (C,m)\<in> ms\<rbrakk> \<Longrightarrow> 
oheimb@11449
   164
         A             |- {P z C m} Impl C m {Q (z::state) C m}"
oheimb@11376
   165
apply (drule Impl')
oheimb@11376
   166
apply (erule Weaken)
oheimb@11376
   167
apply (auto del: image_eqI intro: rev_image_eqI)
oheimb@11376
   168
done
oheimb@11376
   169
oheimb@11376
   170
end