src/HOL/NanoJava/AxSem.thy
author oheimb
Sat Jun 16 20:06:42 2001 +0200 (2001-06-16)
changeset 11376 bf98ad1c22c6
child 11449 d25be0ad1a6c
permissions -rw-r--r--
added NanoJava
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@11376
    12
      triple = "assn \<times> stmt \<times> assn"
oheimb@11376
    13
translations
oheimb@11376
    14
  "assn"   \<leftharpoondown> (type)"state => bool"
oheimb@11376
    15
  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
oheimb@11376
    16
oheimb@11376
    17
consts   hoare   :: "(triple set \<times> triple set) set"
oheimb@11376
    18
syntax (xsymbols)
oheimb@11376
    19
 "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
oheimb@11376
    20
 "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
oheimb@11376
    21
                                   ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
oheimb@11376
    22
syntax
oheimb@11376
    23
 "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
oheimb@11376
    24
 "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
oheimb@11376
    25
                                  ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
oheimb@11376
    26
oheimb@11376
    27
translations "A |\<turnstile> C"       \<rightleftharpoons> "(A,C) \<in> hoare"
oheimb@11376
    28
             "A  \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
oheimb@11376
    29
oheimb@11376
    30
inductive hoare
oheimb@11376
    31
intros
oheimb@11376
    32
oheimb@11376
    33
  Skip:  "A |- {P} Skip {P}"
oheimb@11376
    34
oheimb@11376
    35
  Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
oheimb@11376
    36
oheimb@11376
    37
  Cond: "[| A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c1 {Q}; 
oheimb@11376
    38
            A |- {\<lambda>s. P s \<and> s<e> = Null} c2 {Q}  |] ==>
oheimb@11376
    39
            A |- {P} If(e) c1 Else c2 {Q}"
oheimb@11376
    40
oheimb@11376
    41
  Loop: "A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c {P} ==>
oheimb@11376
    42
         A |- {P} While(e) c {\<lambda>s. P s \<and> s<e> = Null}"
oheimb@11376
    43
oheimb@11376
    44
  NewC: "A |- {\<lambda>s.\<forall>a. new_Addr s=Addr a--> P (lupd(x|->Addr a)(new_obj a C s))}
oheimb@11376
    45
              x:=new C {P}"
oheimb@11376
    46
oheimb@11376
    47
  Cast: "A |- {\<lambda>s.(case s<y> of Null=> True | Addr a=> obj_class s a <=C C) -->
oheimb@11376
    48
              P (lupd(x|->s<y>) s)} x:=(C)y {P}"
oheimb@11376
    49
oheimb@11376
    50
  FAcc: "A |- {\<lambda>s.\<forall>a. s<y>=Addr a-->P(lupd(x|->get_field s a f) s)} x:=y..f{P}"
oheimb@11376
    51
oheimb@11376
    52
  FAss: "A |- {\<lambda>s. \<forall>a. s<y>=Addr a --> P (upd_obj a f (s<x>) s)} y..f:=x {P}"
oheimb@11376
    53
oheimb@11376
    54
  Call: "\<forall>l. A |- {\<lambda>s'. \<exists>s. P s \<and> l = s \<and> 
oheimb@11376
    55
                    s' = lupd(This|->s<y>)(lupd(Param|->s<p>)(init_locs C m s))}
oheimb@11376
    56
                  Meth C m {\<lambda>s. Q (lupd(x|->s<Res>)(set_locs l s))} ==>
oheimb@11376
    57
             A |- {P} x:={C}y..m(p) {Q}"
oheimb@11376
    58
oheimb@11376
    59
  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
    60
                  Impl D m {Q} ==>
oheimb@11376
    61
             A |- {P} Meth C m {Q}"
oheimb@11376
    62
oheimb@11376
    63
  (*\<Union>z instead of \<forall>z in the conclusion and
oheimb@11376
    64
      z restricted to type state due to limitations of the inductive paackage *)
oheimb@11376
    65
  Impl: "A\<union>   (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||- 
oheimb@11376
    66
               (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
oheimb@11376
    67
         A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
oheimb@11376
    68
oheimb@11376
    69
(* structural rules *)
oheimb@11376
    70
oheimb@11376
    71
  (* z restricted to type state due to limitations of the inductive paackage *)
oheimb@11376
    72
  Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
oheimb@11376
    73
             \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
oheimb@11376
    74
            A |- {P} c {Q }"
oheimb@11376
    75
oheimb@11376
    76
  Asm:  "   a \<in> A ==> A ||- {a}"
oheimb@11376
    77
oheimb@11376
    78
  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
oheimb@11376
    79
oheimb@11376
    80
  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}";
oheimb@11376
    81
oheimb@11376
    82
oheimb@11376
    83
subsection "Derived Rules"
oheimb@11376
    84
oheimb@11376
    85
lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
oheimb@11376
    86
apply (rule hoare.Conseq)
oheimb@11376
    87
apply  (rule allI, assumption)
oheimb@11376
    88
apply fast
oheimb@11376
    89
done
oheimb@11376
    90
oheimb@11376
    91
lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
oheimb@11376
    92
apply (rule hoare.ConjI)
oheimb@11376
    93
apply clarify
oheimb@11376
    94
apply (drule hoare.ConjE)
oheimb@11376
    95
apply  fast
oheimb@11376
    96
apply assumption
oheimb@11376
    97
done
oheimb@11376
    98
oheimb@11376
    99
lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
oheimb@11376
   100
by (auto intro: hoare.ConjI hoare.ConjE)
oheimb@11376
   101
oheimb@11376
   102
lemma Impl': 
oheimb@11376
   103
 "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||- 
oheimb@11376
   104
                (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
oheimb@11376
   105
      A     ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
oheimb@11376
   106
apply (drule Union[THEN iffD2])
oheimb@11376
   107
apply (drule hoare.Impl)
oheimb@11376
   108
apply (drule Union[THEN iffD1])
oheimb@11376
   109
apply (erule spec)
oheimb@11376
   110
done
oheimb@11376
   111
oheimb@11376
   112
lemma Impl1: 
oheimb@11376
   113
 "\<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
   114
                 (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms; 
oheimb@11376
   115
  (C,m)\<in> ms\<rbrakk> \<Longrightarrow> 
oheimb@11376
   116
       A    \<turnstile> {P z C m} Impl C m {Q (z::state) C m}"
oheimb@11376
   117
apply (drule Impl')
oheimb@11376
   118
apply (erule Weaken)
oheimb@11376
   119
apply (auto del: image_eqI intro: rev_image_eqI)
oheimb@11376
   120
done
oheimb@11376
   121
oheimb@11376
   122
end