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