src/HOL/Bali/AxExample.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
     1 (*  Title:      isabelle/Bali/AxExample.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   2000 Technische Universitaet Muenchen
     5 *)
     6 header {* Example of a proof based on the Bali axiomatic semantics *}
     7 
     8 theory AxExample = AxSem + Example:
     9 
    10 constdefs
    11   arr_inv :: "st \<Rightarrow> bool"
    12  "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
    13                               values obj (Inl (arr, Base)) = Some (Addr a) \<and>
    14                               heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"
    15 
    16 lemma arr_inv_new_obj: 
    17 "\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"
    18 apply (unfold arr_inv_def)
    19 apply (force dest!: new_AddrD2)
    20 done
    21 
    22 lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s"
    23 apply (unfold arr_inv_def)
    24 apply (simp (no_asm))
    25 done
    26 
    27 lemma arr_inv_gupd_Stat [simp]: 
    28   "Base \<noteq> C \<Longrightarrow> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s"
    29 apply (unfold arr_inv_def)
    30 apply (simp (no_asm_simp))
    31 done
    32 
    33 lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s"
    34 apply (unfold arr_inv_def)
    35 apply (simp (no_asm))
    36 done
    37 
    38 
    39 declare split_if_asm [split del]
    40 declare lvar_def [simp]
    41 
    42 ML {*
    43 fun inst1_tac s t = instantiate_tac [(s,t)];
    44 val ax_tac = REPEAT o rtac allI THEN'
    45              resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
    46                          thm "ax_Alloc"::thm "ax_Alloc_Arr"::
    47                          thm "ax_SXAlloc_Normal"::
    48                          funpow 7 tl (thms "ax_derivs.intros"))
    49 *}
    50 
    51 
    52 theorem ax_test: "tprg,({}::'a triple set)\<turnstile> 
    53   {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)} 
    54   .test [Class Base]. {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
    55 apply (unfold test_def arr_viewed_from_def)
    56 apply (tactic "ax_tac 1" (*;;*))
    57 defer
    58 apply  (tactic "ax_tac 1" (* Try *))
    59 defer
    60 apply    (tactic {* inst1_tac "Q1" 
    61                  "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
    62 prefer 2
    63 apply    simp
    64 apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
    65 prefer 2
    66 apply    clarsimp
    67 apply   (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2)
    68 prefer 2
    69 apply    simp
    70 apply   (tactic "ax_tac 1" (* While *))
    71 prefer 2
    72 apply    (rule ax_impossible [THEN conseq1], clarsimp)
    73 apply   (rule_tac P' = "Normal ?P" in conseq1)
    74 prefer 2
    75 apply    clarsimp
    76 apply   (tactic "ax_tac 1")
    77 apply   (tactic "ax_tac 1" (* AVar *))
    78 prefer 2
    79 apply    (rule ax_subst_Val_allI)
    80 apply    (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
    81 apply    (simp del: avar_def2 peek_and_def2)
    82 apply    (tactic "ax_tac 1")
    83 apply   (tactic "ax_tac 1")
    84       (* just for clarification: *)
    85 apply   (rule_tac Q' = "Normal (\<lambda>Var:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2)
    86 prefer 2
    87 apply    (clarsimp simp add: split_beta)
    88 apply   (tactic "ax_tac 1" (* FVar *))
    89 apply    (tactic "ax_tac 2" (* StatRef *))
    90 apply   (rule ax_derivs.Done [THEN conseq1])
    91 apply   (clarsimp simp add: arr_inv_def inited_def in_bounds_def)
    92 defer
    93 apply  (rule ax_SXAlloc_catch_SXcpt)
    94 apply  (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2)
    95 prefer 2
    96 apply   (simp add: arr_inv_new_obj)
    97 apply  (tactic "ax_tac 1") 
    98 apply  (rule_tac C = "Ext" in ax_Call_known_DynT)
    99 apply     (unfold DynT_prop_def)
   100 apply     (simp (no_asm))
   101 apply    (intro strip)
   102 apply    (rule_tac P' = "Normal ?P" in conseq1)
   103 apply     (tactic "ax_tac 1" (* Methd *))
   104 apply     (rule ax_thin [OF _ empty_subsetI])
   105 apply     (simp (no_asm) add: body_def2)
   106 apply     (tactic "ax_tac 1" (* Body *))
   107 (* apply       (rule_tac [2] ax_derivs.Abrupt) *)
   108 defer
   109 apply      (simp (no_asm))
   110 apply      (tactic "ax_tac 1")
   111 apply      (tactic "ax_tac 1") (* Ass *)
   112 prefer 2
   113 apply       (rule ax_subst_Var_allI)
   114 apply       (tactic {* inst1_tac "P'27" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
   115 apply       (rule allI)
   116 apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
   117 apply       (rule ax_derivs.Abrupt)
   118 apply      (simp (no_asm))
   119 apply      (tactic "ax_tac 1" (* FVar *))
   120 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
   121 apply      (tactic "ax_tac 1")
   122 apply     clarsimp
   123 apply     (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> hd vs = Null) \<and>. heap_free two)" *})
   124 prefer 5
   125 apply     (rule ax_derivs.Done [THEN conseq1], force)
   126 apply    force
   127 apply   (rule ax_subst_Val_allI)
   128 apply   (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
   129 apply   (simp (no_asm) del: peek_and_def2)
   130 apply   (tactic "ax_tac 1")
   131 prefer 2
   132 apply   (rule ax_subst_Val_allI)
   133 apply    (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
   134 apply    (simp del: peek_and_def2)
   135 apply    (tactic "ax_tac 1")
   136 apply   (tactic "ax_tac 1")
   137 apply  (tactic "ax_tac 1")
   138 apply  (tactic "ax_tac 1")
   139 (* end method call *)
   140 apply (simp (no_asm))
   141     (* just for clarification: *)
   142 apply (rule_tac Q' = "Normal ((\<lambda>Y (x, s) Z. arr_inv s \<and> (\<exists>a. the (locals s (VName e)) = Addr a \<and> obj_class (the (globs s (Inl a))) = Ext \<and> 
   143  invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base)  
   144      \<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)"
   145   in conseq2)
   146 prefer 2
   147 apply  clarsimp
   148 apply (tactic "ax_tac 1")
   149 apply (tactic "ax_tac 1")
   150 defer
   151 apply  (rule ax_subst_Var_allI)
   152 apply  (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
   153 apply  (simp (no_asm) del: split_paired_All peek_and_def2)
   154 apply  (tactic "ax_tac 1" (* NewC *))
   155 apply  (tactic "ax_tac 1" (* ax_Alloc *))
   156      (* just for clarification: *)
   157 apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2)
   158 prefer 2
   159 apply   (simp add: invocation_declclass_def dynmethd_def)
   160 apply   (unfold dynlookup_def)
   161 apply   (simp add: dynmethd_Ext_foo)
   162 apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
   163      (* begin init *)
   164 apply  (rule ax_InitS)
   165 apply     force
   166 apply    (simp (no_asm))
   167 apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   168 apply   (rule ax_Init_Skip_lemma)
   169 apply  (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   170 apply  (rule ax_InitS [THEN conseq1] (* init Base *))
   171 apply      force
   172 apply     (simp (no_asm))
   173 apply    (unfold arr_viewed_from_def)
   174 apply    (rule allI)
   175 apply    (rule_tac P' = "Normal ?P" in conseq1)
   176 apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   177 apply     (tactic "ax_tac 1")
   178 apply     (tactic "ax_tac 1")
   179 apply     (rule_tac [2] ax_subst_Var_allI)
   180 apply      (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
   181 apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
   182 apply      (tactic "ax_tac 2" (* NewA *))
   183 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
   184 apply       (tactic "ax_tac 3")
   185 apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
   186 apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
   187 apply      (tactic "ax_tac 2")
   188 apply     (tactic "ax_tac 1" (* FVar *))
   189 apply      (tactic "ax_tac 2" (* StatRef *))
   190 apply     (rule ax_derivs.Done [THEN conseq1])
   191 apply     (tactic {* inst1_tac "Q22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
   192 apply     (clarsimp split del: split_if)
   193 apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
   194 apply     (drule initedD)
   195 apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
   196 apply    force
   197 apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   198 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
   199 apply     (rule wf_tprg)
   200 apply    clarsimp
   201 apply   (tactic {* inst1_tac "P22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
   202 apply   clarsimp
   203 apply  (tactic {* inst1_tac "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
   204 apply  clarsimp
   205      (* end init *)
   206 apply (rule conseq1)
   207 apply (tactic "ax_tac 1")
   208 apply clarsimp
   209 done
   210 
   211 (*
   212 while (true) {
   213   if (i) {throw xcpt;}
   214   else i=j
   215 }
   216 *)
   217 lemma Loop_Xcpt_benchmark: 
   218  "Q = (\<lambda>Y (x,s) Z. x \<noteq> None \<longrightarrow> the_Bool (the (locals s i))) \<Longrightarrow>  
   219   G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)}  
   220   .lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else
   221         (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}"
   222 apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12)
   223 apply  safe
   224 apply  (tactic "ax_tac 1" (* Loop *))
   225 apply   (rule ax_Normal_cases)
   226 prefer 2
   227 apply    (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
   228 apply   (rule conseq1)
   229 apply    (tactic "ax_tac 1")
   230 apply   clarsimp
   231 prefer 2
   232 apply  clarsimp
   233 apply (tactic "ax_tac 1" (* If *))
   234 apply  (tactic 
   235   {* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
   236 apply  (tactic "ax_tac 1")
   237 apply  (rule conseq1)
   238 apply   (tactic "ax_tac 1")
   239 apply  clarsimp
   240 apply (rule allI)
   241 apply (rule ax_escape)
   242 apply auto
   243 apply  (rule conseq1)
   244 apply   (tactic "ax_tac 1" (* Throw *))
   245 apply   (tactic "ax_tac 1")
   246 apply   (tactic "ax_tac 1")
   247 apply  clarsimp
   248 apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2)
   249 prefer 2
   250 apply  clarsimp
   251 apply (rule conseq1)
   252 apply  (tactic "ax_tac 1")
   253 apply  (tactic "ax_tac 1")
   254 prefer 2
   255 apply   (rule ax_subst_Var_allI)
   256 apply   (tactic {* inst1_tac "P'29" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
   257 apply   (rule allI)
   258 apply   (rule_tac P' = "Normal ?P" in conseq1)
   259 prefer 2
   260 apply    clarsimp
   261 apply   (tactic "ax_tac 1")
   262 apply   (rule conseq1)
   263 apply    (tactic "ax_tac 1")
   264 apply   clarsimp
   265 apply  (tactic "ax_tac 1")
   266 apply clarsimp
   267 done
   268 
   269 end
   270