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