src/HOL/Bali/AxSem.thy
author wenzelm
Sat Jul 21 23:25:00 2007 +0200 (2007-07-21)
changeset 23894 1a4167d761ac
parent 23747 b07cff284683
child 24019 67bde7cfcf10
permissions -rw-r--r--
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm@12857
     1
(*  Title:      HOL/Bali/AxSem.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
schirmer@12854
     4
*)
schirmer@12854
     5
schirmer@12854
     6
header {* Axiomatic semantics of Java expressions and statements 
schirmer@12854
     7
          (see also Eval.thy)
schirmer@12854
     8
        *}
schirmer@12854
     9
haftmann@16417
    10
theory AxSem imports Evaln TypeSafe begin
schirmer@12854
    11
schirmer@12854
    12
text {*
schirmer@12854
    13
design issues:
schirmer@12854
    14
\begin{itemize}
schirmer@12854
    15
\item a strong version of validity for triples with premises, namely one that 
schirmer@12854
    16
      takes the recursive depth needed to complete execution, enables 
schirmer@12854
    17
      correctness proof
schirmer@12854
    18
\item auxiliary variables are handled first-class (-> Thomas Kleymann)
schirmer@12854
    19
\item expressions not flattened to elementary assignments (as usual for 
schirmer@12854
    20
      axiomatic semantics) but treated first-class => explicit result value 
schirmer@12854
    21
      handling
schirmer@12854
    22
\item intermediate values not on triple, but on assertion level 
schirmer@12854
    23
      (with result entry)
schirmer@12854
    24
\item multiple results with semantical substitution mechnism not requiring a 
schirmer@12854
    25
      stack 
schirmer@12854
    26
\item because of dynamic method binding, terms need to be dependent on state.
schirmer@12854
    27
  this is also useful for conditional expressions and statements
schirmer@12854
    28
\item result values in triples exactly as in eval relation (also for xcpt 
schirmer@12854
    29
      states)
schirmer@12854
    30
\item validity: additional assumption of state conformance and well-typedness,
schirmer@12854
    31
  which is required for soundness and thus rule hazard required of completeness
schirmer@12854
    32
\end{itemize}
schirmer@12854
    33
schirmer@12854
    34
restrictions:
schirmer@12854
    35
\begin{itemize}
schirmer@12854
    36
\item all triples in a derivation are of the same type (due to weak 
schirmer@12854
    37
      polymorphism)
schirmer@12854
    38
\end{itemize}
schirmer@12854
    39
*}
schirmer@12854
    40
schirmer@13688
    41
types  res = vals --{* result entry *}
schirmer@12854
    42
syntax
schirmer@12854
    43
  Val  :: "val      \<Rightarrow> res"
schirmer@12854
    44
  Var  :: "var      \<Rightarrow> res"
schirmer@12854
    45
  Vals :: "val list \<Rightarrow> res"
schirmer@12854
    46
translations
schirmer@12854
    47
  "Val  x"     => "(In1 x)"
schirmer@12854
    48
  "Var  x"     => "(In2 x)"
schirmer@12854
    49
  "Vals x"     => "(In3 x)"
schirmer@12854
    50
schirmer@12854
    51
syntax
schirmer@12854
    52
  "Val_"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
schirmer@12854
    53
  "Var_"    :: "[pttrn] => pttrn"     ("Var:_"  [951] 950)
schirmer@12854
    54
  "Vals_"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
schirmer@12854
    55
schirmer@12854
    56
translations
schirmer@12854
    57
  "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> the_In1"
schirmer@12854
    58
  "\<lambda>Var:v . b"  == "(\<lambda>v. b) \<circ> the_In2"
schirmer@12854
    59
  "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> the_In3"
schirmer@12854
    60
schirmer@13688
    61
  --{* relation on result values, state and auxiliary variables *}
schirmer@12854
    62
types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
schirmer@12854
    63
translations
schirmer@12854
    64
      "res"    <= (type) "AxSem.res"
schirmer@12854
    65
      "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
schirmer@12854
    66
schirmer@12854
    67
constdefs
schirmer@12854
    68
  assn_imp   :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool"             (infixr "\<Rightarrow>" 25)
schirmer@12854
    69
 "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
schirmer@12854
    70
  
schirmer@12854
    71
lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
schirmer@12854
    72
apply (unfold assn_imp_def)
schirmer@12854
    73
apply (rule HOL.refl)
schirmer@12854
    74
done
schirmer@12854
    75
schirmer@12854
    76
schirmer@12854
    77
section "assertion transformers"
schirmer@12854
    78
schirmer@12854
    79
subsection "peek-and"
schirmer@12854
    80
schirmer@12854
    81
constdefs
schirmer@12854
    82
  peek_and   :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
schirmer@12854
    83
 "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
schirmer@12854
    84
schirmer@12854
    85
lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
schirmer@12854
    86
apply (unfold peek_and_def)
schirmer@12854
    87
apply (simp (no_asm))
schirmer@12854
    88
done
schirmer@12854
    89
schirmer@12854
    90
lemma peek_and_Not [simp]: "(P \<and>. (\<lambda>s. \<not> f s)) = (P \<and>. Not \<circ> f)"
schirmer@12854
    91
apply (rule ext)
schirmer@12854
    92
apply (rule ext)
schirmer@12854
    93
apply (simp (no_asm))
schirmer@12854
    94
done
schirmer@12854
    95
schirmer@12854
    96
lemma peek_and_and [simp]: "peek_and (peek_and P p) p = peek_and P p"
schirmer@12854
    97
apply (unfold peek_and_def)
schirmer@12854
    98
apply (simp (no_asm))
schirmer@12854
    99
done
schirmer@12854
   100
schirmer@12854
   101
lemma peek_and_commut: "(P \<and>. p \<and>. q) = (P \<and>. q \<and>. p)"
schirmer@12854
   102
apply (rule ext)
schirmer@12854
   103
apply (rule ext)
schirmer@12854
   104
apply (rule ext)
schirmer@12854
   105
apply auto
schirmer@12854
   106
done
schirmer@12854
   107
schirmer@12854
   108
syntax
schirmer@12854
   109
  Normal     :: "'a assn \<Rightarrow> 'a assn"
schirmer@12854
   110
translations
schirmer@12854
   111
  "Normal P" == "P \<and>. normal"
schirmer@12854
   112
schirmer@12854
   113
lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)"
schirmer@12854
   114
apply (rule ext)
schirmer@12854
   115
apply (rule ext)
schirmer@12854
   116
apply (rule ext)
schirmer@12854
   117
apply auto
schirmer@12854
   118
done
schirmer@12854
   119
schirmer@12854
   120
subsection "assn-supd"
schirmer@12854
   121
schirmer@12854
   122
constdefs
schirmer@12854
   123
  assn_supd  :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
schirmer@12854
   124
 "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
schirmer@12854
   125
schirmer@12854
   126
lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
schirmer@12854
   127
apply (unfold assn_supd_def)
schirmer@12854
   128
apply (simp (no_asm))
schirmer@12854
   129
done
schirmer@12854
   130
schirmer@12854
   131
subsection "supd-assn"
schirmer@12854
   132
schirmer@12854
   133
constdefs
schirmer@12854
   134
  supd_assn  :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
schirmer@12854
   135
 "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
schirmer@12854
   136
schirmer@12854
   137
schirmer@12854
   138
lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
schirmer@12854
   139
apply (unfold supd_assn_def)
schirmer@12854
   140
apply (simp (no_asm))
schirmer@12854
   141
done
schirmer@12854
   142
schirmer@12854
   143
lemma supd_assn_supdD [elim]: "((f .; Q) ;. f) Y s Z \<Longrightarrow> Q Y s Z"
schirmer@12854
   144
apply auto
schirmer@12854
   145
done
schirmer@12854
   146
schirmer@12854
   147
lemma supd_assn_supdI [elim]: "Q Y s Z \<Longrightarrow> (f .; (Q ;. f)) Y s Z"
schirmer@12854
   148
apply (auto simp del: split_paired_Ex)
schirmer@12854
   149
done
schirmer@12854
   150
schirmer@12854
   151
subsection "subst-res"
schirmer@12854
   152
schirmer@12854
   153
constdefs
schirmer@12854
   154
  subst_res   :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn"              ("_\<leftarrow>_"  [60,61] 60)
schirmer@12854
   155
 "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
schirmer@12854
   156
schirmer@12854
   157
lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
schirmer@12854
   158
apply (unfold subst_res_def)
schirmer@12854
   159
apply (simp (no_asm))
schirmer@12854
   160
done
schirmer@12854
   161
schirmer@12854
   162
lemma subst_subst_res [simp]: "P\<leftarrow>w\<leftarrow>v = P\<leftarrow>w"
schirmer@12854
   163
apply (rule ext)
schirmer@12854
   164
apply (simp (no_asm))
schirmer@12854
   165
done
schirmer@12854
   166
schirmer@12854
   167
lemma peek_and_subst_res [simp]: "(P \<and>. p)\<leftarrow>w = (P\<leftarrow>w \<and>. p)"
schirmer@12854
   168
apply (rule ext)
schirmer@12854
   169
apply (rule ext)
schirmer@12854
   170
apply (simp (no_asm))
schirmer@12854
   171
done
schirmer@12854
   172
schirmer@12854
   173
(*###Do not work for some strange (unification?) reason
schirmer@12854
   174
lemma subst_res_Val_beta [simp]: "(\<lambda>Y. P (the_In1 Y))\<leftarrow>Val v = (\<lambda>Y. P v)"
schirmer@12854
   175
apply (rule ext)
schirmer@12854
   176
by simp
schirmer@12854
   177
schirmer@12854
   178
lemma subst_res_Var_beta [simp]: "(\<lambda>Y. P (the_In2 Y))\<leftarrow>Var vf = (\<lambda>Y. P vf)";
schirmer@12854
   179
apply (rule ext)
schirmer@12854
   180
by simp
schirmer@12854
   181
schirmer@12854
   182
lemma subst_res_Vals_beta [simp]: "(\<lambda>Y. P (the_In3 Y))\<leftarrow>Vals vs = (\<lambda>Y. P vs)";
schirmer@12854
   183
apply (rule ext)
schirmer@12854
   184
by simp
schirmer@12854
   185
*)
schirmer@12854
   186
schirmer@12854
   187
subsection "subst-Bool"
schirmer@12854
   188
schirmer@12854
   189
constdefs
schirmer@12854
   190
  subst_Bool  :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn"             ("_\<leftarrow>=_" [60,61] 60)
schirmer@12854
   191
 "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
schirmer@12854
   192
schirmer@12854
   193
lemma subst_Bool_def2 [simp]: 
schirmer@12854
   194
"(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
schirmer@12854
   195
apply (unfold subst_Bool_def)
schirmer@12854
   196
apply (simp (no_asm))
schirmer@12854
   197
done
schirmer@12854
   198
schirmer@12854
   199
lemma subst_Bool_the_BoolI: "P (Val b) s Z \<Longrightarrow> (P\<leftarrow>=the_Bool b) Y s Z"
schirmer@12854
   200
apply auto
schirmer@12854
   201
done
schirmer@12854
   202
schirmer@12854
   203
subsection "peek-res"
schirmer@12854
   204
schirmer@12854
   205
constdefs
schirmer@12854
   206
  peek_res    :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
schirmer@12854
   207
 "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
schirmer@12854
   208
schirmer@12854
   209
syntax
schirmer@12854
   210
"@peek_res"  :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
schirmer@12854
   211
translations
schirmer@12854
   212
  "\<lambda>w:. P"   == "peek_res (\<lambda>w. P)"
schirmer@12854
   213
schirmer@12854
   214
lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y"
schirmer@12854
   215
apply (unfold peek_res_def)
schirmer@12854
   216
apply (simp (no_asm))
schirmer@12854
   217
done
schirmer@12854
   218
schirmer@12854
   219
lemma peek_res_subst_res [simp]: "peek_res P\<leftarrow>w = P w\<leftarrow>w"
schirmer@12854
   220
apply (rule ext)
schirmer@12854
   221
apply (simp (no_asm))
schirmer@12854
   222
done
schirmer@12854
   223
schirmer@12854
   224
(* unused *)
schirmer@12854
   225
lemma peek_subst_res_allI: 
schirmer@12854
   226
 "(\<And>a. T a (P (f a)\<leftarrow>f a)) \<Longrightarrow> \<forall>a. T a (peek_res P\<leftarrow>f a)"
schirmer@12854
   227
apply (rule allI)
schirmer@12854
   228
apply (simp (no_asm))
schirmer@12854
   229
apply fast
schirmer@12854
   230
done
schirmer@12854
   231
schirmer@12854
   232
subsection "ign-res"
schirmer@12854
   233
schirmer@12854
   234
constdefs
schirmer@12854
   235
  ign_res    ::  "        'a assn \<Rightarrow> 'a assn"            ("_\<down>" [1000] 1000)
schirmer@12854
   236
  "P\<down>        \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
schirmer@12854
   237
schirmer@12854
   238
lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
schirmer@12854
   239
apply (unfold ign_res_def)
schirmer@12854
   240
apply (simp (no_asm))
schirmer@12854
   241
done
schirmer@12854
   242
schirmer@12854
   243
lemma ign_ign_res [simp]: "P\<down>\<down> = P\<down>"
schirmer@12854
   244
apply (rule ext)
schirmer@12854
   245
apply (rule ext)
schirmer@12854
   246
apply (rule ext)
schirmer@12854
   247
apply (simp (no_asm))
schirmer@12854
   248
done
schirmer@12854
   249
schirmer@12854
   250
lemma ign_subst_res [simp]: "P\<down>\<leftarrow>w = P\<down>"
schirmer@12854
   251
apply (rule ext)
schirmer@12854
   252
apply (rule ext)
schirmer@12854
   253
apply (rule ext)
schirmer@12854
   254
apply (simp (no_asm))
schirmer@12854
   255
done
schirmer@12854
   256
schirmer@12854
   257
lemma peek_and_ign_res [simp]: "(P \<and>. p)\<down> = (P\<down> \<and>. p)"
schirmer@12854
   258
apply (rule ext)
schirmer@12854
   259
apply (rule ext)
schirmer@12854
   260
apply (rule ext)
schirmer@12854
   261
apply (simp (no_asm))
schirmer@12854
   262
done
schirmer@12854
   263
schirmer@12854
   264
subsection "peek-st"
schirmer@12854
   265
schirmer@12854
   266
constdefs
schirmer@12854
   267
  peek_st    :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
schirmer@12854
   268
 "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
schirmer@12854
   269
schirmer@12854
   270
syntax
schirmer@12854
   271
"@peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
schirmer@12854
   272
translations
schirmer@12854
   273
  "\<lambda>s.. P"   == "peek_st (\<lambda>s. P)"
schirmer@12854
   274
schirmer@12854
   275
lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s"
schirmer@12854
   276
apply (unfold peek_st_def)
schirmer@12854
   277
apply (simp (no_asm))
schirmer@12854
   278
done
schirmer@12854
   279
schirmer@12854
   280
lemma peek_st_triv [simp]: "(\<lambda>s.. P) = P"
schirmer@12854
   281
apply (rule ext)
schirmer@12854
   282
apply (rule ext)
schirmer@12854
   283
apply (simp (no_asm))
schirmer@12854
   284
done
schirmer@12854
   285
schirmer@12854
   286
lemma peek_st_st [simp]: "(\<lambda>s.. \<lambda>s'.. P s s') = (\<lambda>s.. P s s)"
schirmer@12854
   287
apply (rule ext)
schirmer@12854
   288
apply (rule ext)
schirmer@12854
   289
apply (simp (no_asm))
schirmer@12854
   290
done
schirmer@12854
   291
schirmer@12854
   292
lemma peek_st_split [simp]: "(\<lambda>s.. \<lambda>Y s'. P s Y s') = (\<lambda>Y s. P (store s) Y s)"
schirmer@12854
   293
apply (rule ext)
schirmer@12854
   294
apply (rule ext)
schirmer@12854
   295
apply (simp (no_asm))
schirmer@12854
   296
done
schirmer@12854
   297
schirmer@12854
   298
lemma peek_st_subst_res [simp]: "(\<lambda>s.. P s)\<leftarrow>w = (\<lambda>s.. P s\<leftarrow>w)"
schirmer@12854
   299
apply (rule ext)
schirmer@12854
   300
apply (simp (no_asm))
schirmer@12854
   301
done
schirmer@12854
   302
schirmer@12854
   303
lemma peek_st_Normal [simp]: "(\<lambda>s..(Normal (P s))) = Normal (\<lambda>s.. P s)"
schirmer@12854
   304
apply (rule ext)
schirmer@12854
   305
apply (rule ext)
schirmer@12854
   306
apply (simp (no_asm))
schirmer@12854
   307
done
schirmer@12854
   308
schirmer@12854
   309
subsection "ign-res-eq"
schirmer@12854
   310
schirmer@12854
   311
constdefs
schirmer@12854
   312
  ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn"               ("_\<down>=_"  [60,61] 60)
schirmer@12854
   313
 "P\<down>=w       \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
schirmer@12854
   314
schirmer@12854
   315
lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
schirmer@12854
   316
apply (unfold ign_res_eq_def)
schirmer@12854
   317
apply auto
schirmer@12854
   318
done
schirmer@12854
   319
schirmer@12854
   320
lemma ign_ign_res_eq [simp]: "(P\<down>=w)\<down> = P\<down>"
schirmer@12854
   321
apply (rule ext)
schirmer@12854
   322
apply (rule ext)
schirmer@12854
   323
apply (rule ext)
schirmer@12854
   324
apply (simp (no_asm))
schirmer@12854
   325
done
schirmer@12854
   326
schirmer@12854
   327
(* unused *)
schirmer@12854
   328
lemma ign_res_eq_subst_res: "P\<down>=w\<leftarrow>w = P\<down>"
schirmer@12854
   329
apply (rule ext)
schirmer@12854
   330
apply (rule ext)
schirmer@12854
   331
apply (rule ext)
schirmer@12854
   332
apply (simp (no_asm))
schirmer@12854
   333
done
schirmer@12854
   334
schirmer@12854
   335
(* unused *)
schirmer@12854
   336
lemma subst_Bool_ign_res_eq: "((P\<leftarrow>=b)\<down>=x) Y s Z = ((P\<leftarrow>=b) Y s Z  \<and> Y=x)"
schirmer@12854
   337
apply (simp (no_asm))
schirmer@12854
   338
done
schirmer@12854
   339
schirmer@12854
   340
subsection "RefVar"
schirmer@12854
   341
schirmer@12854
   342
constdefs
schirmer@12854
   343
  RefVar    :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn"(infixr "..;" 13)
schirmer@12854
   344
 "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
schirmer@12854
   345
 
schirmer@12854
   346
lemma RefVar_def2 [simp]: "(vf ..; P) Y s =  
schirmer@12854
   347
  P (Var (fst (vf s))) (snd (vf s))"
schirmer@12854
   348
apply (unfold RefVar_def Let_def)
schirmer@12854
   349
apply (simp (no_asm) add: split_beta)
schirmer@12854
   350
done
schirmer@12854
   351
schirmer@12854
   352
subsection "allocation"
schirmer@12854
   353
schirmer@12854
   354
constdefs
schirmer@12854
   355
  Alloc      :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
schirmer@12854
   356
 "Alloc G otag P \<equiv> \<lambda>Y s Z.
schirmer@12854
   357
                   \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
schirmer@12854
   358
schirmer@12854
   359
  SXAlloc     :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
schirmer@12854
   360
 "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
schirmer@12854
   361
schirmer@12854
   362
schirmer@12854
   363
lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =  
schirmer@12854
   364
       (\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"
schirmer@12854
   365
apply (unfold Alloc_def)
schirmer@12854
   366
apply (simp (no_asm))
schirmer@12854
   367
done
schirmer@12854
   368
schirmer@12854
   369
lemma SXAlloc_def2 [simp]: 
schirmer@12854
   370
  "SXAlloc G P Y s Z = (\<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
schirmer@12854
   371
apply (unfold SXAlloc_def)
schirmer@12854
   372
apply (simp (no_asm))
schirmer@12854
   373
done
schirmer@12854
   374
schirmer@12854
   375
section "validity"
schirmer@12854
   376
schirmer@12854
   377
constdefs
schirmer@12854
   378
  type_ok  :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool"
schirmer@13688
   379
 "type_ok G t s \<equiv> 
schirmer@13688
   380
    \<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
schirmer@13688
   381
                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
schirmer@13688
   382
              \<and> s\<Colon>\<preceq>(G,L)"
schirmer@12854
   383
schirmer@12854
   384
datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
schirmer@12854
   385
something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
schirmer@12854
   386
                                        ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
schirmer@12854
   387
types    'a triples = "'a triple set"
schirmer@12854
   388
schirmer@12854
   389
syntax
schirmer@12854
   390
schirmer@12854
   391
  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   392
                                         ("{(1_)}/ _=>/ {(1_)}"    [3,80,3] 75)
schirmer@12854
   393
  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   394
                                         ("{(1_)}/ _->/ {(1_)}"    [3,80,3] 75)
schirmer@12854
   395
  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   396
                                         ("{(1_)}/ _#>/ {(1_)}"    [3,65,3] 75)
schirmer@12854
   397
  stmt_triple  :: "['a assn, stmt,        'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   398
                                         ("{(1_)}/ ._./ {(1_)}"     [3,65,3] 75)
schirmer@12854
   399
schirmer@12854
   400
syntax (xsymbols)
schirmer@12854
   401
schirmer@12854
   402
  triple       :: "['a assn, term        ,'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   403
                                         ("{(1_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75)
schirmer@12854
   404
  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   405
                                         ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75)
schirmer@12854
   406
  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   407
                                         ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75)
schirmer@12854
   408
  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
schirmer@12854
   409
                                         ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
schirmer@12854
   410
schirmer@12854
   411
translations
schirmer@12854
   412
  "{P} e-\<succ> {Q}" == "{P} In1l e\<succ> {Q}"
schirmer@12854
   413
  "{P} e=\<succ> {Q}" == "{P} In2  e\<succ> {Q}"
schirmer@12854
   414
  "{P} e\<doteq>\<succ> {Q}" == "{P} In3  e\<succ> {Q}"
schirmer@12854
   415
  "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
schirmer@12854
   416
schirmer@12854
   417
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
paulson@13585
   418
apply (rule inj_onI)
schirmer@12854
   419
apply auto
schirmer@12854
   420
done
schirmer@12854
   421
schirmer@12854
   422
lemma triple_inj_eq: "({P} t\<succ> {Q} = {P'} t'\<succ> {Q'} ) = (P=P' \<and> t=t' \<and> Q=Q')"
schirmer@12854
   423
apply auto
schirmer@12854
   424
done
schirmer@12854
   425
schirmer@12854
   426
constdefs
schirmer@12854
   427
  mtriples  :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
schirmer@12854
   428
                ('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times>  'sig) set \<Rightarrow> 'a triples"
schirmer@12854
   429
                                     ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75)
schirmer@12854
   430
 "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
schirmer@12854
   431
  
schirmer@12854
   432
consts
schirmer@12854
   433
schirmer@12854
   434
 triple_valid :: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
schirmer@12854
   435
                                                (   "_\<Turnstile>_:_" [61,0, 58] 57)
schirmer@12854
   436
    ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
schirmer@12854
   437
                                                ("_,_|\<Turnstile>_"   [61,58,58] 57)
schirmer@12854
   438
schirmer@12854
   439
syntax
schirmer@12854
   440
schirmer@12854
   441
 triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
schirmer@12854
   442
                                                (  "_||=_:_" [61,0, 58] 57)
schirmer@12854
   443
     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
schirmer@12854
   444
                                                ( "_,_|=_"   [61,58,58] 57)
schirmer@12854
   445
schirmer@12854
   446
syntax (xsymbols)
schirmer@12854
   447
schirmer@12854
   448
 triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
schirmer@12854
   449
                                                (  "_|\<Turnstile>_:_" [61,0, 58] 57)
schirmer@12854
   450
     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
schirmer@12854
   451
                                                ( "_,_\<Turnstile>_"   [61,58,58] 57)
schirmer@12854
   452
schirmer@12854
   453
defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
schirmer@12854
   454
                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
schirmer@12854
   455
                          (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
schirmer@12854
   456
translations         "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
schirmer@12854
   457
defs   ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
schirmer@12854
   458
translations         "G,A \<Turnstile>t"  == "G,A|\<Turnstile>{t}"
schirmer@12854
   459
schirmer@12854
   460
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
schirmer@12854
   461
 (\<forall>Y s Z. P Y s Z 
schirmer@13688
   462
  \<longrightarrow> (\<exists>L. (normal s \<longrightarrow> (\<exists> C T A. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
schirmer@13688
   463
                   \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<and> 
schirmer@13688
   464
           s\<Colon>\<preceq>(G,L))
schirmer@13688
   465
  \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> Q Y' s' Z))"
schirmer@12854
   466
apply (unfold triple_valid_def type_ok_def)
schirmer@12854
   467
apply (simp (no_asm))
schirmer@12854
   468
done
schirmer@12854
   469
schirmer@12854
   470
schirmer@12854
   471
declare split_paired_All [simp del] split_paired_Ex [simp del] 
schirmer@12854
   472
declare split_if     [split del] split_if_asm     [split del] 
schirmer@12854
   473
        option.split [split del] option.split_asm [split del]
schirmer@12854
   474
ML_setup {*
wenzelm@17876
   475
change_simpset (fn ss => ss delloop "split_all_tac");
wenzelm@17876
   476
change_claset (fn cs => cs delSWrapper "split_all_tac");
schirmer@12854
   477
*}
schirmer@12854
   478
berghofe@23747
   479
inductive
berghofe@21765
   480
  ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
berghofe@21765
   481
  and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple  \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57)
berghofe@21765
   482
  for G :: prog
berghofe@21765
   483
where
schirmer@12854
   484
berghofe@21765
   485
  "G,A \<turnstile>t \<equiv> G,A|\<turnstile>{t}"
berghofe@21765
   486
berghofe@21765
   487
| empty: " G,A|\<turnstile>{}"
berghofe@21765
   488
| insert:"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
schirmer@12854
   489
          G,A|\<turnstile>insert t ts"
schirmer@12854
   490
berghofe@21765
   491
| asm:   "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
schirmer@12854
   492
schirmer@12854
   493
(* could be added for convenience and efficiency, but is not necessary
schirmer@12854
   494
  cut:   "\<lbrakk>G,A'|\<turnstile>ts; G,A|\<turnstile>A'\<rbrakk> \<Longrightarrow>
schirmer@12854
   495
           G,A |\<turnstile>ts"
schirmer@12854
   496
*)
berghofe@21765
   497
| weaken:"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
schirmer@12854
   498
berghofe@21765
   499
| conseq:"\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
schirmer@12854
   500
         (\<forall>Y   Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
schirmer@12854
   501
                                 Q  Y' s' Z ))
schirmer@12854
   502
                                         \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
schirmer@12854
   503
berghofe@21765
   504
| hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
schirmer@12854
   505
berghofe@21765
   506
| Abrupt:  "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
schirmer@12854
   507
schirmer@13688
   508
  --{* variables *}
berghofe@21765
   509
| LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
schirmer@12854
   510
berghofe@21765
   511
| FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
schirmer@12854
   512
          G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>
schirmer@12925
   513
                                 G,A\<turnstile>{Normal P} {accC,C,stat}e..fn=\<succ> {R}"
schirmer@12854
   514
berghofe@21765
   515
| AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
schirmer@12854
   516
          \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>
schirmer@12854
   517
                                 G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
schirmer@13688
   518
  --{* expressions *}
schirmer@12854
   519
berghofe@21765
   520
| NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
schirmer@12854
   521
                                 G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
schirmer@12854
   522
berghofe@21765
   523
| NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
schirmer@12854
   524
	  {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
schirmer@12854
   525
                                 G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
schirmer@12854
   526
berghofe@21765
   527
| Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
schirmer@12854
   528
          abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) .; Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
schirmer@12854
   529
                                 G,A\<turnstile>{Normal P} Cast T e-\<succ> {Q}"
schirmer@12854
   530
berghofe@21765
   531
| Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
schirmer@12854
   532
                  Q\<leftarrow>Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow>
schirmer@12854
   533
                                 G,A\<turnstile>{Normal P} e InstOf T-\<succ> {Q}"
schirmer@12854
   534
berghofe@21765
   535
| Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
schirmer@12854
   536
berghofe@21765
   537
| UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
schirmer@13337
   538
          \<Longrightarrow>
schirmer@13337
   539
          G,A\<turnstile>{Normal P} UnOp unop e-\<succ> {Q}"
schirmer@13337
   540
berghofe@21765
   541
| BinOp:
schirmer@13337
   542
   "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
schirmer@13384
   543
     \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} 
schirmer@13384
   544
               (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ>
schirmer@13384
   545
               {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
schirmer@13337
   546
    \<Longrightarrow>
schirmer@13337
   547
    G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}" 
schirmer@13337
   548
berghofe@21765
   549
| Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
schirmer@12854
   550
berghofe@21765
   551
| Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
schirmer@12854
   552
                                 G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
schirmer@12854
   553
berghofe@21765
   554
| Ass:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
schirmer@12854
   555
     \<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<rbrakk> \<Longrightarrow>
schirmer@12854
   556
                                 G,A\<turnstile>{Normal P} va:=e-\<succ> {R}"
schirmer@12854
   557
berghofe@21765
   558
| Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
schirmer@12854
   559
          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q}\<rbrakk> \<Longrightarrow>
schirmer@12854
   560
                                 G,A\<turnstile>{Normal P} e0 ? e1 : e2-\<succ> {Q}"
schirmer@12854
   561
berghofe@21765
   562
| Call: 
schirmer@12854
   563
"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a};
schirmer@12854
   564
  \<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.
schirmer@12854
   565
 (\<lambda>s. declC=invocation_declclass G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and>
schirmer@12854
   566
      invC = invocation_class mode (store s) a statT \<and>
schirmer@12854
   567
         l = locals (store s)) ;.
schirmer@12854
   568
      init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.
schirmer@12854
   569
      (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
schirmer@12854
   570
 Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow>
schirmer@12925
   571
         G,A\<turnstile>{Normal P} {accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
schirmer@12854
   572
berghofe@21765
   573
| Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
schirmer@12854
   574
                                 G,A|\<turnstile>{{P} Methd-\<succ>  {Q} | ms}"
schirmer@12854
   575
berghofe@21765
   576
| Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
schirmer@12854
   577
  G,A\<turnstile>{Q} .c. {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>(In1 (the (locals s Result)))}\<rbrakk> 
schirmer@12854
   578
    \<Longrightarrow>
schirmer@12854
   579
                                 G,A\<turnstile>{Normal P} Body D c-\<succ> {R}"
schirmer@12854
   580
  
schirmer@13688
   581
  --{* expression lists *}
schirmer@12854
   582
berghofe@21765
   583
| Nil:                          "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
schirmer@12854
   584
berghofe@21765
   585
| Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
schirmer@12854
   586
          \<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>
schirmer@12854
   587
                                 G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
schirmer@12854
   588
schirmer@13688
   589
  --{* statements *}
schirmer@12854
   590
berghofe@21765
   591
| Skip:                         "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
schirmer@12854
   592
berghofe@21765
   593
| Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
schirmer@12854
   594
                                 G,A\<turnstile>{Normal P} .Expr e. {Q}"
schirmer@12854
   595
berghofe@21765
   596
| Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
schirmer@12854
   597
                           G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
schirmer@12854
   598
berghofe@21765
   599
| Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
schirmer@12854
   600
          G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>
schirmer@12854
   601
                                 G,A\<turnstile>{Normal P} .c1;;c2. {R}"
schirmer@12854
   602
berghofe@21765
   603
| If:   "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
schirmer@12854
   604
          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow>
schirmer@12854
   605
                                 G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"
schirmer@12854
   606
(* unfolding variant of Loop, not needed here
schirmer@12854
   607
  LoopU:"\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
schirmer@12854
   608
          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk>
schirmer@12854
   609
         \<Longrightarrow>              G,A\<turnstile>{Normal P} .While(e) c. {Q}"
schirmer@12854
   610
*)
berghofe@21765
   611
| Loop: "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
schirmer@12854
   612
          G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>
schirmer@12854
   613
                            G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"
schirmer@12854
   614
  
berghofe@21765
   615
| Jmp: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P}"
schirmer@12854
   616
berghofe@21765
   617
| Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
schirmer@12854
   618
                                 G,A\<turnstile>{Normal P} .Throw e. {Q}"
schirmer@12854
   619
berghofe@21765
   620
| Try:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
schirmer@12854
   621
          G,A\<turnstile>{Q \<and>. (\<lambda>s.  G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R};
schirmer@12854
   622
              (Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>
schirmer@12854
   623
                                 G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"
schirmer@12854
   624
berghofe@21765
   625
| Fin:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
schirmer@12854
   626
      \<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)}
schirmer@12854
   627
              .c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow>
schirmer@12854
   628
                                 G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"
schirmer@12854
   629
berghofe@21765
   630
| Done:                       "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"
schirmer@12854
   631
berghofe@21765
   632
| Init: "\<lbrakk>the (class G C) = c;
schirmer@12854
   633
          G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
schirmer@12854
   634
              .(if C = Object then Skip else Init (super c)). {Q};
schirmer@12854
   635
      \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
schirmer@12854
   636
              .init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
schirmer@12854
   637
                               G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
schirmer@12854
   638
schirmer@13337
   639
-- {* Some dummy rules for the intermediate terms @{text Callee},
schirmer@13337
   640
@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep 
schirmer@13337
   641
semantics.
schirmer@13337
   642
*}
berghofe@21765
   643
| InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
berghofe@21765
   644
| InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
berghofe@21765
   645
| Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
berghofe@21765
   646
| FinA:      " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
schirmer@13688
   647
(*
schirmer@13688
   648
axioms 
schirmer@13688
   649
*)
schirmer@12854
   650
schirmer@12854
   651
constdefs
schirmer@12854
   652
 adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
schirmer@12854
   653
"adapt_pre P Q Q'\<equiv>\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z)"
schirmer@12854
   654
schirmer@12854
   655
schirmer@12854
   656
section "rules derived by induction"
schirmer@12854
   657
schirmer@12854
   658
lemma cut_valid: "\<lbrakk>G,A'|\<Turnstile>ts; G,A|\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A|\<Turnstile>ts"
schirmer@12854
   659
apply (unfold ax_valids_def)
schirmer@12854
   660
apply fast
schirmer@12854
   661
done
schirmer@12854
   662
schirmer@12854
   663
(*if cut is available
schirmer@12854
   664
Goal "\<lbrakk>G,A'|\<turnstile>ts; A' \<subseteq> A; \<forall>P Q t. {P} t\<succ> {Q} \<in> A' \<longrightarrow> (\<exists>T. (G,L)\<turnstile>t\<Colon>T) \<rbrakk> \<Longrightarrow>  
schirmer@12854
   665
       G,A|\<turnstile>ts"
schirmer@12854
   666
b y etac ax_derivs.cut 1;
schirmer@12854
   667
b y eatac ax_derivs.asm 1 1;
schirmer@12854
   668
qed "ax_thin";
schirmer@12854
   669
*)
schirmer@12854
   670
lemma ax_thin [rule_format (no_asm)]: 
schirmer@12854
   671
  "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
schirmer@12854
   672
apply (erule ax_derivs.induct)
wenzelm@23894
   673
apply                (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
schirmer@12854
   674
apply                (rule ax_derivs.empty)
schirmer@12854
   675
apply               (erule (1) ax_derivs.insert)
schirmer@12854
   676
apply              (fast intro: ax_derivs.asm)
schirmer@12854
   677
(*apply           (fast intro: ax_derivs.cut) *)
schirmer@12854
   678
apply            (fast intro: ax_derivs.weaken)
schirmer@13337
   679
apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) 
schirmer@13337
   680
(* 37 subgoals *)
schirmer@13337
   681
prefer 18 (* Methd *)
paulson@23563
   682
apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
paulson@23563
   683
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *})
paulson@23563
   684
apply auto
schirmer@12854
   685
done
schirmer@12854
   686
schirmer@12854
   687
lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"
schirmer@12854
   688
apply (erule ax_thin)
schirmer@12854
   689
apply fast
schirmer@12854
   690
done
schirmer@12854
   691
schirmer@12854
   692
lemma subset_mtriples_iff: 
schirmer@12854
   693
  "ts \<subseteq> {{P} mb-\<succ> {Q} | ms} = (\<exists>ms'. ms'\<subseteq>ms \<and>  ts = {{P} mb-\<succ> {Q} | ms'})"
schirmer@12854
   694
apply (unfold mtriples_def)
schirmer@12854
   695
apply (rule subset_image_iff)
schirmer@12854
   696
done
schirmer@12854
   697
schirmer@12854
   698
lemma weaken: 
schirmer@12854
   699
 "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
schirmer@12854
   700
apply (erule ax_derivs.induct)
schirmer@13337
   701
(*42 subgoals*)
schirmer@12854
   702
apply       (tactic "ALLGOALS strip_tac")
schirmer@12854
   703
apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
schirmer@12854
   704
         etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
schirmer@12854
   705
apply       (tactic "TRYALL hyp_subst_tac")
schirmer@12854
   706
apply       (simp, rule ax_derivs.empty)
schirmer@12854
   707
apply      (drule subset_insertD)
schirmer@12854
   708
apply      (blast intro: ax_derivs.insert)
schirmer@12854
   709
apply     (fast intro: ax_derivs.asm)
schirmer@12854
   710
(*apply  (blast intro: ax_derivs.cut) *)
schirmer@12854
   711
apply   (fast intro: ax_derivs.weaken)
schirmer@12854
   712
apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
schirmer@13337
   713
(*37 subgoals*)
schirmer@12854
   714
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
wenzelm@23894
   715
                   THEN_ALL_NEW fast_tac @{claset}) *})
schirmer@12854
   716
(*1 subgoal*)
schirmer@12854
   717
apply (clarsimp simp add: subset_mtriples_iff)
schirmer@12854
   718
apply (rule ax_derivs.Methd)
schirmer@12854
   719
apply (drule spec)
schirmer@12854
   720
apply (erule impE)
schirmer@12854
   721
apply  (rule exI)
schirmer@12854
   722
apply  (erule conjI)
schirmer@12854
   723
apply  (rule HOL.refl)
schirmer@12854
   724
oops (* dead end, Methd is to blame *)
schirmer@12854
   725
schirmer@12854
   726
schirmer@12854
   727
section "rules derived from conseq"
schirmer@12854
   728
schirmer@13688
   729
text {* In the following rules we often have to give some type annotations like:
schirmer@13688
   730
 @{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}.
schirmer@13688
   731
Given only the term above without annotations, Isabelle would infer a more 
schirmer@13688
   732
general type were we could have 
schirmer@13688
   733
different types of auxiliary variables in the assumption set (@{term A}) and 
schirmer@13688
   734
in the triple itself (@{term P} and @{term Q}). But 
schirmer@13688
   735
@{text "ax_derivs.Methd"} enforces the same type in the inductive definition of
schirmer@13688
   736
the derivation. So we have to restrict the types to be able to apply the
schirmer@13688
   737
rules. 
schirmer@13688
   738
*}
schirmer@13688
   739
lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
schirmer@12854
   740
 \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>  
schirmer@12854
   741
  Q Y' s' Z)\<rbrakk>  
schirmer@12854
   742
  \<Longrightarrow>  G,A\<turnstile>{P ::'a assn} t\<succ> {Q }"
schirmer@13688
   743
apply (rule ax_derivs.conseq)
schirmer@12854
   744
apply clarsimp
schirmer@12854
   745
apply blast
schirmer@12854
   746
done
schirmer@12854
   747
schirmer@13688
   748
-- {* Nice variant, since it is so symmetric we might be able to memorise it. *}
schirmer@13688
   749
lemma conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; \<forall>s Y' s'.  
schirmer@12854
   750
       (\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>  
schirmer@12854
   751
       (\<forall>Y Z. P  Y s Z \<longrightarrow> Q  Y' s' Z)\<rbrakk>  
schirmer@13688
   752
  \<Longrightarrow>  G,A\<turnstile>{P::'a assn } t\<succ> {Q }"
schirmer@12854
   753
apply (erule conseq12)
schirmer@12854
   754
apply fast
schirmer@12854
   755
done
schirmer@12854
   756
schirmer@13688
   757
lemma conseq12_from_conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
schirmer@12854
   758
 \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>  
schirmer@12854
   759
  Q Y' s' Z)\<rbrakk>  
schirmer@13688
   760
  \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q }"
schirmer@12854
   761
apply (erule conseq12')
schirmer@12854
   762
apply blast
schirmer@12854
   763
done
schirmer@12854
   764
schirmer@13688
   765
lemma conseq1: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> 
schirmer@13688
   766
 \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
schirmer@12854
   767
apply (erule conseq12)
schirmer@12854
   768
apply blast
schirmer@12854
   769
done
schirmer@12854
   770
schirmer@13688
   771
lemma conseq2: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> 
schirmer@13688
   772
\<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
schirmer@12854
   773
apply (erule conseq12)
schirmer@12854
   774
apply blast
schirmer@12854
   775
done
schirmer@12854
   776
schirmer@13688
   777
lemma ax_escape: 
schirmer@13688
   778
 "\<lbrakk>\<forall>Y s Z. P Y s Z 
schirmer@13688
   779
   \<longrightarrow> G,(A::'a triple set)\<turnstile>{\<lambda>Y' s' (Z'::'a). (Y',s') = (Y,s)} 
schirmer@13688
   780
                             t\<succ> 
schirmer@13688
   781
                            {\<lambda>Y s Z'. Q Y s Z}
schirmer@13688
   782
\<rbrakk> \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q::'a assn}"
schirmer@13688
   783
apply (rule ax_derivs.conseq)
schirmer@12854
   784
apply force
schirmer@12854
   785
done
schirmer@12854
   786
schirmer@12854
   787
(* unused *)
schirmer@13688
   788
lemma ax_constant: "\<lbrakk> C \<Longrightarrow> G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}\<rbrakk> 
schirmer@13688
   789
\<Longrightarrow> G,A\<turnstile>{\<lambda>Y s Z. C \<and> P Y s Z} t\<succ> {Q}"
schirmer@12854
   790
apply (rule ax_escape (* unused *))
schirmer@12854
   791
apply clarify
schirmer@12854
   792
apply (rule conseq12)
schirmer@12854
   793
apply  fast
schirmer@12854
   794
apply auto
schirmer@12854
   795
done
schirmer@12854
   796
(*alternative (more direct) proof:
schirmer@12854
   797
apply (rule ax_derivs.conseq) *)(* unused *)(*
schirmer@12854
   798
apply (fast)
schirmer@12854
   799
*)
schirmer@12854
   800
schirmer@12854
   801
schirmer@13688
   802
lemma ax_impossible [intro]: 
schirmer@13688
   803
  "G,(A::'a triple set)\<turnstile>{\<lambda>Y s Z. False} t\<succ> {Q::'a assn}"
schirmer@12854
   804
apply (rule ax_escape)
schirmer@12854
   805
apply clarify
schirmer@12854
   806
done
schirmer@12854
   807
schirmer@12854
   808
(* unused *)
schirmer@12854
   809
lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s"
schirmer@12854
   810
apply auto
schirmer@12854
   811
done
schirmer@13688
   812
schirmer@13688
   813
lemma ax_nochange:
schirmer@13688
   814
 "G,(A::(res \<times> state) triple set)\<turnstile>{\<lambda>Y s Z. (Y,s)=Z} t\<succ> {\<lambda>Y s Z. (Y,s)=Z} 
schirmer@13688
   815
  \<Longrightarrow> G,A\<turnstile>{P::(res \<times> state) assn} t\<succ> {P}"
schirmer@12854
   816
apply (erule conseq12)
schirmer@12854
   817
apply auto
schirmer@12854
   818
apply (erule (1) ax_nochange_lemma)
schirmer@12854
   819
done
schirmer@12854
   820
schirmer@12854
   821
(* unused *)
schirmer@13688
   822
lemma ax_trivial: "G,(A::'a triple set)\<turnstile>{P::'a assn}  t\<succ> {\<lambda>Y s Z. True}"
schirmer@13688
   823
apply (rule ax_derivs.conseq(* unused *))
schirmer@12854
   824
apply auto
schirmer@12854
   825
done
schirmer@12854
   826
schirmer@12854
   827
(* unused *)
schirmer@13688
   828
lemma ax_disj: 
schirmer@13688
   829
 "\<lbrakk>G,(A::'a triple set)\<turnstile>{P1::'a assn} t\<succ> {Q1}; G,A\<turnstile>{P2::'a assn} t\<succ> {Q2}\<rbrakk> 
schirmer@13688
   830
  \<Longrightarrow>  G,A\<turnstile>{\<lambda>Y s Z. P1 Y s Z \<or> P2 Y s Z} t\<succ> {\<lambda>Y s Z. Q1 Y s Z \<or> Q2 Y s Z}"
schirmer@12854
   831
apply (rule ax_escape (* unused *))
schirmer@12854
   832
apply safe
schirmer@12854
   833
apply  (erule conseq12, fast)+
schirmer@12854
   834
done
schirmer@12854
   835
schirmer@12854
   836
(* unused *)
schirmer@13688
   837
lemma ax_supd_shuffle: 
schirmer@13688
   838
 "(\<exists>Q. G,(A::'a triple set)\<turnstile>{P::'a assn} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) =  
schirmer@12854
   839
       (\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})"
schirmer@12854
   840
apply (best elim!: conseq1 conseq2)
schirmer@12854
   841
done
schirmer@12854
   842
schirmer@13688
   843
lemma ax_cases: "
schirmer@13688
   844
 \<lbrakk>G,(A::'a triple set)\<turnstile>{P \<and>.       C} t\<succ> {Q::'a assn};  
schirmer@13688
   845
                   G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
schirmer@12854
   846
apply (unfold peek_and_def)
schirmer@12854
   847
apply (rule ax_escape)
schirmer@12854
   848
apply clarify
schirmer@12854
   849
apply (case_tac "C s")
schirmer@12854
   850
apply  (erule conseq12, force)+
schirmer@12854
   851
done
schirmer@12854
   852
(*alternative (more direct) proof:
schirmer@12854
   853
apply (rule rtac ax_derivs.conseq) *)(* unused *)(*
schirmer@12854
   854
apply clarify
schirmer@12854
   855
apply (case_tac "C s")
schirmer@12854
   856
apply  force+
schirmer@12854
   857
*)
schirmer@12854
   858
schirmer@13688
   859
lemma ax_adapt: "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
schirmer@13688
   860
  \<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
schirmer@12854
   861
apply (unfold adapt_pre_def)
schirmer@12854
   862
apply (erule conseq12)
schirmer@12854
   863
apply fast
schirmer@12854
   864
done
schirmer@12854
   865
schirmer@13688
   866
lemma adapt_pre_adapts: "G,(A::'a triple set)\<Turnstile>{P::'a assn} t\<succ> {Q} 
schirmer@13688
   867
\<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
schirmer@12854
   868
apply (unfold adapt_pre_def)
schirmer@12854
   869
apply (simp add: ax_valids_def triple_valid_def2)
schirmer@12854
   870
apply fast
schirmer@12854
   871
done
schirmer@12854
   872
schirmer@12854
   873
schirmer@12854
   874
lemma adapt_pre_weakest: 
schirmer@12854
   875
"\<forall>G (A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>  
schirmer@12854
   876
  P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)"
schirmer@12854
   877
apply (unfold adapt_pre_def)
schirmer@12854
   878
apply (drule spec)
schirmer@12854
   879
apply (drule_tac x = "{}" in spec)
schirmer@12854
   880
apply (drule_tac x = "In1r Skip" in spec)
schirmer@12854
   881
apply (simp add: ax_valids_def triple_valid_def2)
schirmer@12854
   882
oops
schirmer@12854
   883
schirmer@12854
   884
lemma peek_and_forget1_Normal: 
schirmer@13688
   885
 "G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} 
schirmer@13688
   886
 \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}"
schirmer@12854
   887
apply (erule conseq1)
schirmer@12854
   888
apply (simp (no_asm))
schirmer@12854
   889
done
schirmer@12854
   890
schirmer@13688
   891
lemma peek_and_forget1: 
schirmer@13688
   892
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
schirmer@13688
   893
 \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}"
schirmer@12854
   894
apply (erule conseq1)
schirmer@12854
   895
apply (simp (no_asm))
schirmer@12854
   896
done
schirmer@12854
   897
schirmer@12854
   898
lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal] 
schirmer@12854
   899
schirmer@13688
   900
lemma peek_and_forget2: 
schirmer@13688
   901
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q \<and>. p} 
schirmer@13688
   902
\<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
schirmer@12854
   903
apply (erule conseq2)
schirmer@12854
   904
apply (simp (no_asm))
schirmer@12854
   905
done
schirmer@12854
   906
schirmer@13688
   907
lemma ax_subst_Val_allI: 
schirmer@13688
   908
"\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Val v} t\<succ> {(Q v)::'a assn}
schirmer@13688
   909
 \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}"
schirmer@12854
   910
apply (force elim!: conseq1)
schirmer@12854
   911
done
schirmer@12854
   912
schirmer@13688
   913
lemma ax_subst_Var_allI: 
schirmer@13688
   914
"\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Var v} t\<succ> {(Q v)::'a assn}
schirmer@13688
   915
 \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}"
schirmer@12854
   916
apply (force elim!: conseq1)
schirmer@12854
   917
done
schirmer@12854
   918
schirmer@13688
   919
lemma ax_subst_Vals_allI: 
schirmer@13688
   920
"(\<forall>v. G,(A::'a triple set)\<turnstile>{(     P'          v )\<leftarrow>Vals v} t\<succ> {(Q v)::'a assn})
schirmer@13688
   921
 \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}"
schirmer@12854
   922
apply (force elim!: conseq1)
schirmer@12854
   923
done
schirmer@12854
   924
schirmer@12854
   925
schirmer@12854
   926
section "alternative axioms"
schirmer@12854
   927
schirmer@12854
   928
lemma ax_Lit2: 
schirmer@12854
   929
  "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}"
schirmer@12854
   930
apply (rule ax_derivs.Lit [THEN conseq1])
schirmer@12854
   931
apply force
schirmer@12854
   932
done
schirmer@12854
   933
lemma ax_Lit2_test_complete: 
schirmer@12854
   934
  "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v-\<succ> {P}"
schirmer@12854
   935
apply (rule ax_Lit2 [THEN conseq2])
schirmer@12854
   936
apply force
schirmer@12854
   937
done
schirmer@12854
   938
schirmer@12854
   939
lemma ax_LVar2: "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} LVar vn=\<succ> {Normal (\<lambda>s.. P\<down>=Var (lvar vn s))}"
schirmer@12854
   940
apply (rule ax_derivs.LVar [THEN conseq1])
schirmer@12854
   941
apply force
schirmer@12854
   942
done
schirmer@12854
   943
schirmer@12854
   944
lemma ax_Super2: "G,(A::'a triple set)\<turnstile>
schirmer@12854
   945
  {Normal P::'a assn} Super-\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}"
schirmer@12854
   946
apply (rule ax_derivs.Super [THEN conseq1])
schirmer@12854
   947
apply force
schirmer@12854
   948
done
schirmer@12854
   949
schirmer@12854
   950
lemma ax_Nil2: 
schirmer@12854
   951
  "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}"
schirmer@12854
   952
apply (rule ax_derivs.Nil [THEN conseq1])
schirmer@12854
   953
apply force
schirmer@12854
   954
done
schirmer@12854
   955
schirmer@12854
   956
schirmer@12854
   957
section "misc derived structural rules"
schirmer@12854
   958
schirmer@12854
   959
(* unused *)
schirmer@12854
   960
lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 
schirmer@12854
   961
    G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 
schirmer@12854
   962
       G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
schirmer@12854
   963
apply (frule (1) finite_subset)
schirmer@12854
   964
apply (erule make_imp)
schirmer@12854
   965
apply (erule thin_rl)
schirmer@12854
   966
apply (erule finite_induct)
schirmer@12854
   967
apply  (unfold mtriples_def)
schirmer@12854
   968
apply  (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+
schirmer@12854
   969
apply force
schirmer@12854
   970
done
schirmer@12854
   971
lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl]
schirmer@12854
   972
schirmer@12854
   973
lemma ax_derivs_insertD: 
schirmer@12854
   974
 "G,(A::'a triple set)|\<turnstile>insert (t::'a triple) ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A|\<turnstile>ts"
schirmer@12854
   975
apply (fast intro: ax_derivs.weaken)
schirmer@12854
   976
done
schirmer@12854
   977
schirmer@12854
   978
lemma ax_methods_spec: 
schirmer@12854
   979
"\<lbrakk>G,(A::'a triple set)|\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
schirmer@12854
   980
apply (erule ax_derivs.weaken)
schirmer@12854
   981
apply (force del: image_eqI intro: rev_image_eqI)
schirmer@12854
   982
done
schirmer@12854
   983
schirmer@12854
   984
(* this version is used to avoid using the cut rule *)
schirmer@12854
   985
lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
schirmer@12854
   986
  ((\<forall>(C,sig)\<in>F. G,(A::'a triple set)\<turnstile>(f C sig::'a triple)) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>(g C sig::'a triple))) \<longrightarrow>  
schirmer@12854
   987
      G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
schirmer@12854
   988
apply (frule (1) finite_subset)
schirmer@12854
   989
apply (erule make_imp)
schirmer@12854
   990
apply (erule thin_rl)
schirmer@12854
   991
apply (erule finite_induct)
schirmer@12854
   992
apply  clarsimp+
schirmer@12854
   993
apply (drule ax_derivs_insertD)
schirmer@12854
   994
apply (rule ax_derivs.insert)
schirmer@12854
   995
apply  (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
   996
apply  (auto elim: ax_methods_spec)
schirmer@12854
   997
done
schirmer@12854
   998
lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl]
schirmer@12854
   999
 
schirmer@12854
  1000
lemma ax_no_hazard: 
schirmer@12854
  1001
  "G,(A::'a triple set)\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q::'a assn} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
schirmer@12854
  1002
apply (erule ax_cases)
schirmer@12854
  1003
apply (rule ax_derivs.hazard [THEN conseq1])
schirmer@12854
  1004
apply force
schirmer@12854
  1005
done
schirmer@12854
  1006
schirmer@12854
  1007
lemma ax_free_wt: 
schirmer@12854
  1008
 "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
schirmer@12854
  1009
  \<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> 
schirmer@12854
  1010
  G,A\<turnstile>{Normal P} t\<succ> {Q}"
schirmer@12854
  1011
apply (rule ax_no_hazard)
schirmer@12854
  1012
apply (rule ax_escape)
schirmer@12854
  1013
apply clarify
schirmer@12854
  1014
apply (erule mp [THEN conseq12])
schirmer@12854
  1015
apply  (auto simp add: type_ok_def)
schirmer@12854
  1016
done
schirmer@12854
  1017
schirmer@12854
  1018
ML {*
schirmer@12854
  1019
bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
schirmer@12854
  1020
*}
schirmer@12854
  1021
declare ax_Abrupts [intro!]
schirmer@12854
  1022
berghofe@21765
  1023
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
schirmer@12854
  1024
schirmer@12854
  1025
lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}"
schirmer@12854
  1026
apply (rule ax_Normal_cases)
schirmer@12854
  1027
apply  (rule ax_derivs.Skip)
schirmer@12854
  1028
apply fast
schirmer@12854
  1029
done
schirmer@12854
  1030
lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
schirmer@12854
  1031
schirmer@12854
  1032
schirmer@12854
  1033
section "derived rules for methd call"
schirmer@12854
  1034
schirmer@12854
  1035
lemma ax_Call_known_DynT: 
schirmer@12854
  1036
"\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 
schirmer@12854
  1037
  \<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.
schirmer@12854
  1038
  init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)} 
schirmer@12854
  1039
    Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
schirmer@12854
  1040
  \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>  
schirmer@12854
  1041
       {R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>
schirmer@12854
  1042
                     C = invocation_declclass 
schirmer@12854
  1043
                            G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};  
schirmer@12854
  1044
       G,(A::'a triple set)\<turnstile>{Normal P} e-\<succ> {Q::'a assn}\<rbrakk>  
schirmer@12925
  1045
   \<Longrightarrow> G,A\<turnstile>{Normal P} {accC,statT,IntVir}e\<cdot>mn({pTs}args)-\<succ> {S}"
schirmer@12854
  1046
apply (erule ax_derivs.Call)
schirmer@12854
  1047
apply  safe
schirmer@12854
  1048
apply  (erule spec)
schirmer@12854
  1049
apply (rule ax_escape, clarsimp)
schirmer@12854
  1050
apply (drule spec, drule spec, drule spec,erule conseq12)
schirmer@12854
  1051
apply force
schirmer@12854
  1052
done
schirmer@12854
  1053
schirmer@12854
  1054
schirmer@12854
  1055
lemma ax_Call_Static: 
schirmer@12854
  1056
 "\<lbrakk>\<forall>a vs l. G,A\<turnstile>{R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.  
schirmer@12854
  1057
               init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs}  
schirmer@12854
  1058
              Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
schirmer@12854
  1059
  G,A\<turnstile>{Normal P} e-\<succ> {Q};
schirmer@12854
  1060
  \<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn)  a 
schirmer@12854
  1061
  \<and>. (\<lambda> s. C=invocation_declclass 
schirmer@12854
  1062
                G Static (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr>)}
schirmer@12925
  1063
\<rbrakk>  \<Longrightarrow>  G,A\<turnstile>{Normal P} {accC,statT,Static}e\<cdot>mn({pTs}args)-\<succ> {S}"
schirmer@12854
  1064
apply (erule ax_derivs.Call)
schirmer@12854
  1065
apply  safe
schirmer@12854
  1066
apply  (erule spec)
schirmer@12854
  1067
apply (rule ax_escape, clarsimp)
schirmer@12854
  1068
apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
schirmer@12854
  1069
apply (drule spec,drule spec,drule spec, erule conseq12)
schirmer@20014
  1070
apply (force simp add: init_lvars_def Let_def)
schirmer@12854
  1071
done
schirmer@12854
  1072
schirmer@12854
  1073
lemma ax_Methd1: 
schirmer@12854
  1074
 "\<lbrakk>G,A\<union>{{P} Methd-\<succ> {Q} | ms}|\<turnstile> {{P} body G-\<succ> {Q} | ms}; (C,sig)\<in> ms\<rbrakk> \<Longrightarrow> 
schirmer@12854
  1075
       G,A\<turnstile>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
schirmer@12854
  1076
apply (drule ax_derivs.Methd)
schirmer@12854
  1077
apply (unfold mtriples_def)
schirmer@12854
  1078
apply (erule (1) ax_methods_spec)
schirmer@12854
  1079
done
schirmer@12854
  1080
schirmer@12854
  1081
lemma ax_MethdN: 
schirmer@12854
  1082
"G,insert({Normal P} Methd  C sig-\<succ> {Q}) A\<turnstile> 
schirmer@12854
  1083
          {Normal P} body G C sig-\<succ> {Q} \<Longrightarrow>  
schirmer@12854
  1084
      G,A\<turnstile>{Normal P} Methd   C sig-\<succ> {Q}"
schirmer@12854
  1085
apply (rule ax_Methd1)
schirmer@12854
  1086
apply  (rule_tac [2] singletonI)
schirmer@12854
  1087
apply (unfold mtriples_def)
schirmer@12854
  1088
apply clarsimp
schirmer@12854
  1089
done
schirmer@12854
  1090
schirmer@12854
  1091
lemma ax_StatRef: 
schirmer@12854
  1092
  "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt-\<succ> {P::'a assn}"
schirmer@12854
  1093
apply (rule ax_derivs.Cast)
schirmer@12854
  1094
apply (rule ax_Lit2 [THEN conseq2])
schirmer@12854
  1095
apply clarsimp
schirmer@12854
  1096
done
schirmer@12854
  1097
schirmer@12854
  1098
section "rules derived from Init and Done"
schirmer@12854
  1099
schirmer@12854
  1100
  lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;  
schirmer@12854
  1101
     \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
schirmer@12854
  1102
            .init c. {set_lvars l .; R};   
schirmer@12854
  1103
         G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}  
schirmer@12854
  1104
  .Init (super c). {Q}\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1105
  G,(A::'a triple set)\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R::'a assn}"
schirmer@12854
  1106
apply (erule ax_derivs.Init)
schirmer@12854
  1107
apply  (simp (no_asm_simp))
schirmer@12854
  1108
apply assumption
schirmer@12854
  1109
done
schirmer@12854
  1110
schirmer@12854
  1111
lemma ax_Init_Skip_lemma: 
schirmer@12854
  1112
"\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit> \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars l'}
schirmer@12854
  1113
  .Skip. {(set_lvars l .; P)::'a assn}"
schirmer@12854
  1114
apply (rule allI)
schirmer@12854
  1115
apply (rule ax_SkipI)
schirmer@12854
  1116
apply clarsimp
schirmer@12854
  1117
done
schirmer@12854
  1118
schirmer@12854
  1119
lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object; 
schirmer@12854
  1120
       P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P);  
schirmer@12854
  1121
       G,A\<turnstile>{Normal (P \<and>. initd C)} .Init (super c). {(P \<and>. initd C)\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1122
       G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init C. {(P \<and>. initd C)::'a assn}"
schirmer@12854
  1123
apply (rule_tac C = "initd C" in ax_cases)
schirmer@12854
  1124
apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
schirmer@12854
  1125
apply (simp (no_asm))
schirmer@12854
  1126
apply (erule (1) ax_InitS)
schirmer@12854
  1127
apply  simp
schirmer@12854
  1128
apply  (rule ax_Init_Skip_lemma)
schirmer@12854
  1129
apply (erule conseq1)
schirmer@12854
  1130
apply force
schirmer@12854
  1131
done
schirmer@12854
  1132
schirmer@12854
  1133
lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>
schirmer@12854
  1134
  {Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)} 
schirmer@12854
  1135
       .Init Object. {(P \<and>. initd Object)::'a assn}"
schirmer@12854
  1136
apply (rule ax_derivs.Init)
schirmer@12854
  1137
apply   (drule class_Object, force)
schirmer@12854
  1138
apply (simp_all (no_asm))
schirmer@12854
  1139
apply (rule_tac [2] ax_Init_Skip_lemma)
schirmer@12854
  1140
apply (rule ax_SkipI, force)
schirmer@12854
  1141
done
schirmer@12854
  1142
schirmer@12854
  1143
lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G;  
schirmer@12854
  1144
       (P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1145
  G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}"
schirmer@12854
  1146
apply (rule_tac C = "initd Object" in ax_cases)
schirmer@12854
  1147
apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
schirmer@12854
  1148
apply (erule ax_Init_Object [THEN conseq1])
schirmer@12854
  1149
apply force
schirmer@12854
  1150
done
schirmer@12854
  1151
schirmer@12854
  1152
schirmer@12854
  1153
section "introduction rules for Alloc and SXAlloc"
schirmer@12854
  1154
schirmer@13688
  1155
lemma ax_SXAlloc_Normal: 
schirmer@13688
  1156
 "G,(A::'a triple set)\<turnstile>{P::'a assn} .c. {Normal Q} 
schirmer@13688
  1157
 \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}"
schirmer@12854
  1158
apply (erule conseq2)
schirmer@12854
  1159
apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all)
schirmer@12854
  1160
done
schirmer@12854
  1161
schirmer@12854
  1162
lemma ax_Alloc: 
schirmer@13688
  1163
  "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
schirmer@13688
  1164
     {Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
schirmer@13688
  1165
      Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>. 
schirmer@13688
  1166
      heap_free (Suc (Suc 0))}
schirmer@12854
  1167
   \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}"
schirmer@12854
  1168
apply (erule conseq2)
schirmer@12854
  1169
apply (auto elim!: halloc_elim_cases)
schirmer@12854
  1170
done
schirmer@12854
  1171
schirmer@12854
  1172
lemma ax_Alloc_Arr: 
schirmer@13688
  1173
 "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
schirmer@13688
  1174
   {\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. \<not>the_Intg i<0 \<and>  
schirmer@13688
  1175
    (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
schirmer@13688
  1176
    Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>.
schirmer@13688
  1177
    heap_free (Suc (Suc 0))} 
schirmer@13688
  1178
 \<Longrightarrow>  
schirmer@12854
  1179
 G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}"
schirmer@12854
  1180
apply (erule conseq2)
schirmer@12854
  1181
apply (auto elim!: halloc_elim_cases)
schirmer@12854
  1182
done
schirmer@12854
  1183
schirmer@12854
  1184
lemma ax_SXAlloc_catch_SXcpt: 
schirmer@13688
  1185
 "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
schirmer@13688
  1186
     {(\<lambda>Y (x,s) Z. x=Some (Xcpt (Std xn)) \<and>  
schirmer@13688
  1187
      (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
schirmer@13688
  1188
      Q Y (Some (Xcpt (Loc a)),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z))  
schirmer@13688
  1189
      \<and>. heap_free (Suc (Suc 0))}\<rbrakk> 
schirmer@13688
  1190
 \<Longrightarrow>  
schirmer@13688
  1191
 G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}"
schirmer@12854
  1192
apply (erule conseq2)
schirmer@12854
  1193
apply (auto elim!: sxalloc_elim_cases halloc_elim_cases)
schirmer@12854
  1194
done
schirmer@12854
  1195
schirmer@12854
  1196
end