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