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