src/HOL/Bali/AxExample.thy
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 16121 a80aa66d2271
child 17374 63e0ab9f2ea9
permissions -rw-r--r--
migrated theory headers to new format
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 {*
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
    43
fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
    44
  SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
val ax_tac = REPEAT o rtac allI THEN'
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
             resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
                         thm "ax_Alloc"::thm "ax_Alloc_Arr"::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
                         thm "ax_SXAlloc_Normal"::
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
                         funpow 7 tl (thms "ax_derivs.intros"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
*}
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
theorem ax_test: "tprg,({}::'a triple set)\<turnstile> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
  {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
    55
  .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
    56
  {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
apply (unfold test_def arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
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
    59
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
    60
         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
    61
         precondition. *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
apply  (tactic "ax_tac 1" (* Try *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
defer
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
    64
apply    (tactic {* inst1_tac "Q" 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
                 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
apply    simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
apply    clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
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
    72
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
apply    simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
apply   (tactic "ax_tac 1" (* While *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
apply    (rule ax_impossible [THEN conseq1], clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
apply   (rule_tac P' = "Normal ?P" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
apply    clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
apply   (tactic "ax_tac 1" (* AVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
apply    (rule ax_subst_Val_allI)
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
    84
apply    (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
apply    (simp del: avar_def2 peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
apply    (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
      (* just for clarification: *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
apply   (rule_tac Q' = "Normal (\<lambda>Var:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
apply    (clarsimp simp add: split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
apply   (tactic "ax_tac 1" (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
apply    (tactic "ax_tac 2" (* StatRef *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
apply   (rule ax_derivs.Done [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
apply   (clarsimp simp add: arr_inv_def inited_def in_bounds_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
apply  (rule ax_SXAlloc_catch_SXcpt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
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
    99
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
apply   (simp add: arr_inv_new_obj)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
apply  (tactic "ax_tac 1") 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
apply  (rule_tac C = "Ext" in ax_Call_known_DynT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
apply     (unfold DynT_prop_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
apply     (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
apply    (intro strip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
apply    (rule_tac P' = "Normal ?P" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
apply     (tactic "ax_tac 1" (* Methd *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
apply     (rule ax_thin [OF _ empty_subsetI])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
apply     (simp (no_asm) add: body_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
apply     (tactic "ax_tac 1" (* Body *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
(* apply       (rule_tac [2] ax_derivs.Abrupt) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
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
   114
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
   115
            (* 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
   116
                 ((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
   117
                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
   118
                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
   119
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
   120
             
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 ax_derivs.Expr) (* Expr *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
apply      (tactic "ax_tac 1") (* Ass *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
apply       (rule ax_subst_Var_allI)
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   125
apply       (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
apply       (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply       (rule ax_derivs.Abrupt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
apply      (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
apply      (tactic "ax_tac 1" (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
apply      (tactic "ax_tac 1")
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   133
apply     (tactic {* inst1_tac "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
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
   134
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
   135
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
   136
apply    (rule ax_derivs.Done [THEN conseq1],force)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
apply   (rule ax_subst_Val_allI)
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   138
apply   (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
apply   (simp (no_asm) del: peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
apply   (rule ax_subst_Val_allI)
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   143
apply    (tactic {* inst1_tac "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
apply    (simp del: peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
apply    (tactic "ax_tac 1")
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
(* end method call *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
    (* just for clarification: *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
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
   153
 invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
     \<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
  in conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
apply (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
apply (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
apply  (rule ax_subst_Var_allI)
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   162
apply  (tactic {* inst1_tac "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply  (simp (no_asm) del: split_paired_All peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
apply  (tactic "ax_tac 1" (* NewC *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
apply  (tactic "ax_tac 1" (* ax_Alloc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
     (* just for clarification: *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free tree \<and>. initd Ext)" in conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
apply   (simp add: invocation_declclass_def dynmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
apply   (unfold dynlookup_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply   (simp add: dynmethd_Ext_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
     (* begin init *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
apply  (rule ax_InitS)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
apply     force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
apply    (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
apply   (rule ax_Init_Skip_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
apply  (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
apply  (rule ax_InitS [THEN conseq1] (* init Base *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
apply      force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
apply     (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
apply    (unfold arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
apply    (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
apply    (rule_tac P' = "Normal ?P" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
apply     (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
apply     (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
apply     (rule_tac [2] ax_subst_Var_allI)
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   190
apply      (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
apply      (tactic "ax_tac 2" (* NewA *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
apply       (tactic "ax_tac 3")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
apply      (tactic "ax_tac 2")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
apply     (tactic "ax_tac 1" (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
apply      (tactic "ax_tac 2" (* StatRef *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
apply     (rule ax_derivs.Done [THEN conseq1])
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   201
apply     (tactic {* inst1_tac "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
apply     (clarsimp split del: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
apply     (drule initedD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
apply    force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
apply     (rule wf_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
apply    clarsimp
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   211
apply   (tactic {* inst1_tac "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
apply   clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
apply  (tactic {* inst1_tac "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
     (* end init *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
apply (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
apply (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
while (true) {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
  if (i) {throw xcpt;}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
  else i=j
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
lemma Loop_Xcpt_benchmark: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
 "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
   229
  G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
  .lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
        (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
apply  (tactic "ax_tac 1" (* Loop *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
apply   (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply    (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
apply   (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
apply    (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
apply   clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
apply (tactic "ax_tac 1" (* If *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
apply  (tactic 
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   245
  {* inst1_tac "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply  (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
apply  (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
apply   (tactic "ax_tac 1" (* Throw *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
apply (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
apply   (rule ax_subst_Var_allI)
15793
acfdd493f5c4 Made inst1_tac more robust against changes of variable indices.
berghofe
parents: 14981
diff changeset
   266
apply   (tactic {* inst1_tac "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
apply   (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
apply   (rule_tac P' = "Normal ?P" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
apply    clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
apply   (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
apply    (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
apply   clarsimp
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
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
end
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280