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