src/HOL/Bali/AxExample.thy
author wenzelm
Mon, 25 Feb 2002 20:48:14 +0100
changeset 12937 0c4fd7529467
parent 12925 99131847fb93
child 13688 a0b16d42d489
permissions -rw-r--r--
clarified syntax of ``long'' statements: fixes/assumes/shows;
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
12859
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
     6
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
header {* Example of a proof based on the Bali axiomatic semantics *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
theory AxExample = AxSem + Example:
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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
fun inst1_tac s t = instantiate_tac [(s,t)];
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)} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
  .test [Class Base]. {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
apply (unfold test_def arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
apply (tactic "ax_tac 1" (*;;*))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
apply  (tactic "ax_tac 1" (* Try *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
apply    (tactic {* inst1_tac "Q1" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
                 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
apply    simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
apply    clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
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
    69
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
apply    simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
apply   (tactic "ax_tac 1" (* While *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
apply    (rule ax_impossible [THEN conseq1], clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
apply   (rule_tac P' = "Normal ?P" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
apply    clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
apply   (tactic "ax_tac 1" (* AVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
apply    (rule ax_subst_Val_allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
apply    (tactic {* inst1_tac "P'21" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
apply    (simp del: avar_def2 peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
apply    (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
      (* just for clarification: *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
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
    87
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
apply    (clarsimp simp add: split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
apply   (tactic "ax_tac 1" (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
apply    (tactic "ax_tac 2" (* StatRef *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
apply   (rule ax_derivs.Done [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
apply   (clarsimp simp add: arr_inv_def inited_def in_bounds_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
apply  (rule ax_SXAlloc_catch_SXcpt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
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
    96
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
apply   (simp add: arr_inv_new_obj)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
apply  (tactic "ax_tac 1") 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
apply  (rule_tac C = "Ext" in ax_Call_known_DynT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
apply     (unfold DynT_prop_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
apply     (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
apply    (intro strip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
apply    (rule_tac P' = "Normal ?P" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
apply     (tactic "ax_tac 1" (* Methd *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
apply     (rule ax_thin [OF _ empty_subsetI])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
apply     (simp (no_asm) add: body_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
apply     (tactic "ax_tac 1" (* Body *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
(* apply       (rule_tac [2] ax_derivs.Abrupt) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
apply      (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
apply      (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
apply      (tactic "ax_tac 1") (* Ass *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
apply       (rule ax_subst_Var_allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
apply       (tactic {* inst1_tac "P'27" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
apply       (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
apply       (rule ax_derivs.Abrupt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
apply      (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
apply      (tactic "ax_tac 1" (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
apply      (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
apply     clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
apply     (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> hd vs = Null) \<and>. heap_free two)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
prefer 5
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
apply     (rule ax_derivs.Done [THEN conseq1], force)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
apply    force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply   (rule ax_subst_Val_allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
apply   (tactic {* inst1_tac "P'33" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
apply   (simp (no_asm) del: peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
apply   (rule ax_subst_Val_allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
apply    (tactic {* inst1_tac "P'4" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
apply    (simp del: peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
apply    (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
(* end method call *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
    (* just for clarification: *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
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
   144
 invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
     \<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
  in conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
apply  clarsimp
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
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
apply  (rule ax_subst_Var_allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
apply  (tactic {* inst1_tac "P'14" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
apply  (simp (no_asm) del: split_paired_All peek_and_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
apply  (tactic "ax_tac 1" (* NewC *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
apply  (tactic "ax_tac 1" (* ax_Alloc *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
     (* just for clarification: *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
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
   159
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
apply   (simp add: invocation_declclass_def dynmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
apply   (unfold dynlookup_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
apply   (simp add: dynmethd_Ext_foo)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
     (* begin init *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
apply  (rule ax_InitS)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
apply     force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
apply    (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
apply   (rule ax_Init_Skip_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
apply  (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply  (rule ax_InitS [THEN conseq1] (* init Base *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
apply      force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
apply     (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
apply    (unfold arr_viewed_from_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
apply    (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
apply    (rule_tac P' = "Normal ?P" in conseq1)
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     (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
apply     (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
apply     (rule_tac [2] ax_subst_Var_allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
apply      (tactic {* inst1_tac "P'29" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
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
   183
apply      (tactic "ax_tac 2" (* NewA *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
apply       (tactic "ax_tac 3")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
apply      (tactic "ax_tac 2")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
apply     (tactic "ax_tac 1" (* FVar *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
apply      (tactic "ax_tac 2" (* StatRef *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
apply     (rule ax_derivs.Done [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
apply     (tactic {* inst1_tac "Q22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
apply     (clarsimp split del: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
apply     (drule initedD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
apply    force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
apply     (rule wf_tprg)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
apply    clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
apply   (tactic {* inst1_tac "P22" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
apply   clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
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
   205
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
     (* end init *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
apply (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
apply (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
while (true) {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
  if (i) {throw xcpt;}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
  else i=j
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
lemma Loop_Xcpt_benchmark: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
 "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
   220
  G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
  .lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
        (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
apply  (tactic "ax_tac 1" (* Loop *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
apply   (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
apply    (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
apply   (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
apply    (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
apply   clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
apply (tactic "ax_tac 1" (* If *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
apply  (tactic 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
  {* inst1_tac "P'21" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply  (tactic "ax_tac 1")
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
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
apply  (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
apply   (tactic "ax_tac 1" (* Throw *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply   (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
apply (rule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
apply   (rule ax_subst_Var_allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
apply   (tactic {* inst1_tac "P'29" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
apply   (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
apply   (rule_tac P' = "Normal ?P" in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
apply    clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
apply   (tactic "ax_tac 1")
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   clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
apply  (tactic "ax_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
end
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271