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