src/HOL/Bali/AxExample.thy
changeset 15793 acfdd493f5c4
parent 14981 e73f8140af78
child 16121 a80aa66d2271
equal deleted inserted replaced
15792:e9b7e210ad2a 15793:acfdd493f5c4
    37 
    37 
    38 
    38 
    39 declare split_if_asm [split del]
    39 declare split_if_asm [split del]
    40 declare lvar_def [simp]
    40 declare lvar_def [simp]
    41 
    41 
    42 ML {*
    42 ML_setup {*
    43 fun inst1_tac s t = instantiate_tac [(s,t)];
    43 fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
       
    44   SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
    44 val ax_tac = REPEAT o rtac allI THEN'
    45 val ax_tac = REPEAT o rtac allI THEN'
    45              resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
    46              resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
    46                          thm "ax_Alloc"::thm "ax_Alloc_Arr"::
    47                          thm "ax_Alloc"::thm "ax_Alloc_Arr"::
    47                          thm "ax_SXAlloc_Normal"::
    48                          thm "ax_SXAlloc_Normal"::
    48                          funpow 7 tl (thms "ax_derivs.intros"))
    49                          funpow 7 tl (thms "ax_derivs.intros"))
    58 defer (* We begin with the last assertion, to synthesise the intermediate
    59 defer (* We begin with the last assertion, to synthesise the intermediate
    59          assertions, like in the fashion of the weakest
    60          assertions, like in the fashion of the weakest
    60          precondition. *)
    61          precondition. *)
    61 apply  (tactic "ax_tac 1" (* Try *))
    62 apply  (tactic "ax_tac 1" (* Try *))
    62 defer
    63 defer
    63 apply    (tactic {* inst1_tac "Q1" 
    64 apply    (tactic {* inst1_tac "Q" 
    64                  "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
    65                  "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
    65 prefer 2
    66 prefer 2
    66 apply    simp
    67 apply    simp
    67 apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
    68 apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
    68 prefer 2
    69 prefer 2
    78 apply    clarsimp
    79 apply    clarsimp
    79 apply   (tactic "ax_tac 1")
    80 apply   (tactic "ax_tac 1")
    80 apply   (tactic "ax_tac 1" (* AVar *))
    81 apply   (tactic "ax_tac 1" (* AVar *))
    81 prefer 2
    82 prefer 2
    82 apply    (rule ax_subst_Val_allI)
    83 apply    (rule ax_subst_Val_allI)
    83 apply    (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
    84 apply    (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
    84 apply    (simp del: avar_def2 peek_and_def2)
    85 apply    (simp del: avar_def2 peek_and_def2)
    85 apply    (tactic "ax_tac 1")
    86 apply    (tactic "ax_tac 1")
    86 apply   (tactic "ax_tac 1")
    87 apply   (tactic "ax_tac 1")
    87       (* just for clarification: *)
    88       (* just for clarification: *)
    88 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)
    89 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)
   119              
   120              
   120 apply      (rule ax_derivs.Expr) (* Expr *)
   121 apply      (rule ax_derivs.Expr) (* Expr *)
   121 apply      (tactic "ax_tac 1") (* Ass *)
   122 apply      (tactic "ax_tac 1") (* Ass *)
   122 prefer 2
   123 prefer 2
   123 apply       (rule ax_subst_Var_allI)
   124 apply       (rule ax_subst_Var_allI)
   124 apply       (tactic {* inst1_tac "P'29" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
   125 apply       (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
   125 apply       (rule allI)
   126 apply       (rule allI)
   126 apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
   127 apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
   127 apply       (rule ax_derivs.Abrupt)
   128 apply       (rule ax_derivs.Abrupt)
   128 apply      (simp (no_asm))
   129 apply      (simp (no_asm))
   129 apply      (tactic "ax_tac 1" (* FVar *))
   130 apply      (tactic "ax_tac 1" (* FVar *))
   130 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
   131 apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
   131 apply      (tactic "ax_tac 1")
   132 apply      (tactic "ax_tac 1")
   132 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> vs = [Null]) \<and>. heap_free two)" *})
   133 apply     (tactic {* inst1_tac "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)" *})
   133 apply     fastsimp
   134 apply     fastsimp
   134 prefer 4
   135 prefer 4
   135 apply    (rule ax_derivs.Done [THEN conseq1],force)
   136 apply    (rule ax_derivs.Done [THEN conseq1],force)
   136 apply   (rule ax_subst_Val_allI)
   137 apply   (rule ax_subst_Val_allI)
   137 apply   (tactic {* inst1_tac "P'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
   138 apply   (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
   138 apply   (simp (no_asm) del: peek_and_def2)
   139 apply   (simp (no_asm) del: peek_and_def2)
   139 apply   (tactic "ax_tac 1")
   140 apply   (tactic "ax_tac 1")
   140 prefer 2
   141 prefer 2
   141 apply   (rule ax_subst_Val_allI)
   142 apply   (rule ax_subst_Val_allI)
   142 apply    (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
   143 apply    (tactic {* inst1_tac "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
   143 apply    (simp del: peek_and_def2)
   144 apply    (simp del: peek_and_def2)
   144 apply    (tactic "ax_tac 1")
   145 apply    (tactic "ax_tac 1")
   145 apply   (tactic "ax_tac 1")
   146 apply   (tactic "ax_tac 1")
   146 apply  (tactic "ax_tac 1")
   147 apply  (tactic "ax_tac 1")
   147 apply  (tactic "ax_tac 1")
   148 apply  (tactic "ax_tac 1")
   156 apply  clarsimp
   157 apply  clarsimp
   157 apply (tactic "ax_tac 1")
   158 apply (tactic "ax_tac 1")
   158 apply (tactic "ax_tac 1")
   159 apply (tactic "ax_tac 1")
   159 defer
   160 defer
   160 apply  (rule ax_subst_Var_allI)
   161 apply  (rule ax_subst_Var_allI)
   161 apply  (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
   162 apply  (tactic {* inst1_tac "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
   162 apply  (simp (no_asm) del: split_paired_All peek_and_def2)
   163 apply  (simp (no_asm) del: split_paired_All peek_and_def2)
   163 apply  (tactic "ax_tac 1" (* NewC *))
   164 apply  (tactic "ax_tac 1" (* NewC *))
   164 apply  (tactic "ax_tac 1" (* ax_Alloc *))
   165 apply  (tactic "ax_tac 1" (* ax_Alloc *))
   165      (* just for clarification: *)
   166      (* just for clarification: *)
   166 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)
   167 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)
   184 apply    (rule_tac P' = "Normal ?P" in conseq1)
   185 apply    (rule_tac P' = "Normal ?P" in conseq1)
   185 apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   186 apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   186 apply     (tactic "ax_tac 1")
   187 apply     (tactic "ax_tac 1")
   187 apply     (tactic "ax_tac 1")
   188 apply     (tactic "ax_tac 1")
   188 apply     (rule_tac [2] ax_subst_Var_allI)
   189 apply     (rule_tac [2] ax_subst_Var_allI)
   189 apply      (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
   190 apply      (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
   190 apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
   191 apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
   191 apply      (tactic "ax_tac 2" (* NewA *))
   192 apply      (tactic "ax_tac 2" (* NewA *))
   192 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
   193 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
   193 apply       (tactic "ax_tac 3")
   194 apply       (tactic "ax_tac 3")
   194 apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
   195 apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
   195 apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
   196 apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
   196 apply      (tactic "ax_tac 2")
   197 apply      (tactic "ax_tac 2")
   197 apply     (tactic "ax_tac 1" (* FVar *))
   198 apply     (tactic "ax_tac 1" (* FVar *))
   198 apply      (tactic "ax_tac 2" (* StatRef *))
   199 apply      (tactic "ax_tac 2" (* StatRef *))
   199 apply     (rule ax_derivs.Done [THEN conseq1])
   200 apply     (rule ax_derivs.Done [THEN conseq1])
   200 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)" *})
   201 apply     (tactic {* inst1_tac "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
   201 apply     (clarsimp split del: split_if)
   202 apply     (clarsimp split del: split_if)
   202 apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
   203 apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
   203 apply     (drule initedD)
   204 apply     (drule initedD)
   204 apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
   205 apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
   205 apply    force
   206 apply    force
   206 apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   207 apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
   207 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
   208 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
   208 apply     (rule wf_tprg)
   209 apply     (rule wf_tprg)
   209 apply    clarsimp
   210 apply    clarsimp
   210 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)" *})
   211 apply   (tactic {* inst1_tac "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
   211 apply   clarsimp
   212 apply   clarsimp
   212 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)" *})
   213 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)" *})
   213 apply  clarsimp
   214 apply  clarsimp
   214      (* end init *)
   215      (* end init *)
   215 apply (rule conseq1)
   216 apply (rule conseq1)
   239 apply   clarsimp
   240 apply   clarsimp
   240 prefer 2
   241 prefer 2
   241 apply  clarsimp
   242 apply  clarsimp
   242 apply (tactic "ax_tac 1" (* If *))
   243 apply (tactic "ax_tac 1" (* If *))
   243 apply  (tactic 
   244 apply  (tactic 
   244   {* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
   245   {* inst1_tac "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
   245 apply  (tactic "ax_tac 1")
   246 apply  (tactic "ax_tac 1")
   246 apply  (rule conseq1)
   247 apply  (rule conseq1)
   247 apply   (tactic "ax_tac 1")
   248 apply   (tactic "ax_tac 1")
   248 apply  clarsimp
   249 apply  clarsimp
   249 apply (rule allI)
   250 apply (rule allI)
   260 apply (rule conseq1)
   261 apply (rule conseq1)
   261 apply  (tactic "ax_tac 1")
   262 apply  (tactic "ax_tac 1")
   262 apply  (tactic "ax_tac 1")
   263 apply  (tactic "ax_tac 1")
   263 prefer 2
   264 prefer 2
   264 apply   (rule ax_subst_Var_allI)
   265 apply   (rule ax_subst_Var_allI)
   265 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)" *})
   266 apply   (tactic {* inst1_tac "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
   266 apply   (rule allI)
   267 apply   (rule allI)
   267 apply   (rule_tac P' = "Normal ?P" in conseq1)
   268 apply   (rule_tac P' = "Normal ?P" in conseq1)
   268 prefer 2
   269 prefer 2
   269 apply    clarsimp
   270 apply    clarsimp
   270 apply   (tactic "ax_tac 1")
   271 apply   (tactic "ax_tac 1")