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