src/HOL/Bali/TypeSafe.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46714 a7ca72710dfe
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/TypeSafe.thy
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
     2
    Author:     David von Oheimb and Norbert Schirmer
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
header {* The type soundness proof for Java *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
23019
019d44d46834 hide locale predicate "field" from HOL library
haftmann
parents: 21765
diff changeset
     6
theory TypeSafe
019d44d46834 hide locale predicate "field" from HOL library
haftmann
parents: 21765
diff changeset
     7
imports DefiniteAssignmentCorrect Conform
019d44d46834 hide locale predicate "field" from HOL library
haftmann
parents: 21765
diff changeset
     8
begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    10
section "error free"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    11
 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    12
lemma error_free_halloc:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
    13
  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    14
          error_free_s0: "error_free s0"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
    15
  shows "error_free s1"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    16
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    17
  from halloc error_free_s0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    18
  obtain abrupt0 store0 abrupt1 store1
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    19
    where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    20
          halloc': "G\<turnstile>(abrupt0,store0) \<midarrow>halloc oi\<succ>a\<rightarrow> (abrupt1,store1)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    21
          error_free_s0': "error_free (abrupt0,store0)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    22
    by (cases s0,cases s1) auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    23
  from halloc' error_free_s0'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    24
  have "error_free (abrupt1,store1)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    25
  proof (induct)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    26
    case Abrupt 
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: 13601
diff changeset
    27
    then show ?case .
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    28
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    29
    case New
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    30
    then show ?case
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
    31
      by auto
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    32
  qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    33
  with eqs 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    34
  show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    35
    by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    36
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    37
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    38
lemma error_free_sxalloc:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
    39
  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
    40
  shows "error_free s1"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    41
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    42
  from sxalloc error_free_s0
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    43
  obtain abrupt0 store0 abrupt1 store1
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    44
    where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    45
          sxalloc': "G\<turnstile>(abrupt0,store0) \<midarrow>sxalloc\<rightarrow> (abrupt1,store1)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    46
          error_free_s0': "error_free (abrupt0,store0)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    47
    by (cases s0,cases s1) auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    48
  from sxalloc' error_free_s0'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    49
  have "error_free (abrupt1,store1)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    50
  proof (induct)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    51
  qed (auto)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    52
  with eqs 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    53
  show ?thesis 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    54
    by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    55
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    56
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    57
lemma error_free_check_field_access_eq:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    58
 "error_free (check_field_access G accC statDeclC fn stat a s)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    59
 \<Longrightarrow> (check_field_access G accC statDeclC fn stat a s) = s"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    60
apply (cases s)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    61
apply (auto simp add: check_field_access_def Let_def error_free_def 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    62
                      abrupt_if_def 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    63
            split: split_if_asm)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    64
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    65
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    66
lemma error_free_check_method_access_eq:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    67
"error_free (check_method_access G accC statT mode sig a' s)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    68
 \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    69
apply (cases s)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    70
apply (auto simp add: check_method_access_def Let_def error_free_def 
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
    71
                      abrupt_if_def)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    72
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    73
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    74
lemma error_free_FVar_lemma: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    75
     "error_free s 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    76
       \<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
    77
  by (case_tac s) auto
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    78
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    79
lemma error_free_init_lvars [simp,intro]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    80
"error_free s \<Longrightarrow> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    81
  error_free (init_lvars G C sig mode a pvs s)"
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
    82
by (cases s) (auto simp add: init_lvars_def Let_def)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    83
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    84
lemma error_free_LVar_lemma:   
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    85
"error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    86
by (cases s) simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    87
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    88
lemma error_free_throw [simp,intro]:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    89
  "error_free s \<Longrightarrow> error_free (abupd (throw x) s)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    90
by (cases s) (simp add: throw_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
    91
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
section "result conformance"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
    95
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
    96
  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
    97
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
    98
  "s\<le>|f\<preceq>T\<Colon>\<preceq>E =
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
    99
   ((\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   100
    (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s'))))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
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: 13601
diff changeset
   102
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   103
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   104
  rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   105
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   106
  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T =
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   107
    (case T of
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   108
      Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   109
                then (\<forall> n. (the_In2 t) = LVar n 
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   110
                       \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   111
                           (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   112
                    (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   113
                    (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   114
                else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   115
    | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
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: 13601
diff changeset
   117
text {*
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: 13601
diff changeset
   118
 With @{term rconf} we describe the conformance of the result value of a term.
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: 13601
diff changeset
   119
 This definition gets rather complicated because of the relations between 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: 13601
diff changeset
   120
 injections of the different terms, types and values. The main case distinction
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: 13601
diff changeset
   121
 is between single values and value lists. In case of value lists, every 
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: 13601
diff changeset
   122
 value has to conform to its type. For single values we have to do a further
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: 13601
diff changeset
   123
 case distinction, between values of variables @{term "\<exists>var. t=In2 var" } 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: 13601
diff changeset
   124
 ordinary values. Values of variables are modelled as pairs consisting of 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: 13601
diff changeset
   125
 current value and an update function which will perform an assignment to 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: 13601
diff changeset
   126
 variable. This stems form the decision, that we only have one evaluation rule
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   127
 for each kind of variable. The decision if we read or write to 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: 13601
diff changeset
   128
 variable is made by syntactic enclosing rules. So conformance 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: 13601
diff changeset
   129
 variable-values must ensure that both the current value and an update will 
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: 13601
diff changeset
   130
 conform to the type. With the introduction of definite assignment of local
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: 13601
diff changeset
   131
 variables we have to do another case distinction. For the notion of conformance
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: 13601
diff changeset
   132
 local variables are allowed to be @{term None}, since the definedness is not 
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: 13601
diff changeset
   133
 ensured by conformance but by definite assignment. Field and array variables 
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: 13601
diff changeset
   134
 must contain a value. 
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: 13601
diff changeset
   135
*}
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: 13601
diff changeset
   136
 
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: 13601
diff changeset
   137
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: 13601
diff changeset
   138
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
lemma rconf_In1 [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
 "G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T  =  G,s\<turnstile>v\<Colon>\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
apply (unfold rconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
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: 13601
diff changeset
   145
lemma rconf_In2_no_LVar [simp]: 
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: 13601
diff changeset
   146
 "\<forall> n. va\<noteq>LVar n \<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: 13601
diff changeset
   147
   G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  = (G,s\<turnstile>fst vf\<Colon>\<preceq>T \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
apply (unfold rconf_def)
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: 13601
diff changeset
   149
apply auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
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: 13601
diff changeset
   152
lemma rconf_In2_LVar [simp]: 
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: 13601
diff changeset
   153
 "va=LVar n \<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: 13601
diff changeset
   154
   G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  
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: 13601
diff changeset
   155
    = ((fst vf = the (locals s n)) \<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: 13601
diff changeset
   156
       (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst vf\<Colon>\<preceq>T) \<and> s\<le>|snd vf\<preceq>T\<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: 13601
diff changeset
   157
apply (unfold rconf_def)
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: 13601
diff changeset
   158
by simp
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: 13601
diff changeset
   159
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
lemma rconf_In3 [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
 "G,L,s\<turnstile>In3 es\<succ>In3 vs\<Colon>\<preceq>Inr Ts = list_all2 (\<lambda>v T. G,s\<turnstile>v\<Colon>\<preceq>T) vs Ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
apply (unfold rconf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
section "fits and conf"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
apply (unfold fits_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply clarify
18585
5d379fe2eb74 replaced swap by contrapos_np;
wenzelm
parents: 18576
diff changeset
   172
apply (erule contrapos_np, simp (no_asm_use))
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
apply (drule conf_RefTD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
lemma fits_conf: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
  "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T\<preceq>? T'; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
apply (force dest: conf_RefTD intro: conf_AddrI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
lemma fits_Array: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
 "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T'.[]\<preceq>T.[]; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
apply (force dest: conf_RefTD intro: conf_AddrI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
section "gext"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
apply (erule halloc.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
apply  (auto dest!: new_AddrD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
lemma sxalloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
apply (erule sxalloc.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
apply   (auto dest!: halloc_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
lemma eval_gext_lemma [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> snd s\<le>|snd s' \<and> (case w of  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
    In1 v \<Rightarrow> True  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
  | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
  | In3 vs \<Rightarrow> True)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
apply (erule eval_induct)
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12937
diff changeset
   211
prefer 26 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
  apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   214
 simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   215
            check_field_access_def check_method_access_def Let_def
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
 split del: split_if_asm split add: sum3.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
(* 6 subgoals *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
apply force+
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
lemma evar_gext_f: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
  "G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
apply (drule eval_gext_lemma [THEN conjunct2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
lemmas eval_gext = eval_gext_lemma [THEN conjunct1]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 19796
diff changeset
   229
lemma eval_gext': "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,(x2,s2)) \<Longrightarrow> s1\<le>|s2"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
apply (drule eval_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
apply (erule eval_cases , auto split del: split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
apply (case_tac "inited C (globs s1)")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
apply  (clarsimp split del: split_if_asm)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
apply (drule eval_gext')+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
apply (drule init_class_obj_inited)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
apply (erule inited_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
apply (simp (no_asm_use))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
section "Lemmas"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
lemma obj_ty_obj_class1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
 "\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
apply (case_tac "tag obj")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
apply (auto simp add: obj_ty_def obj_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
lemma oconf_init_obj: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
 "\<lbrakk>wf_prog G;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
 (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
apply (auto intro!: oconf_init_obj_lemma unique_fields)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
  wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
                        | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
  (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
apply (unfold init_obj_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
15217
15fa818ef624 bug-fix with new records
schirmer
parents: 15102
diff changeset
   266
            )
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
lemma conforms_init_class_obj: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
 "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
  (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
apply (rule not_initedD [THEN conforms_newG])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
apply    (auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
lemma fst_init_lvars[simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
 "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   279
  (if is_static m then x else (np a') x)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
apply (simp (no_asm) add: init_lvars_def2)
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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
lemma halloc_conforms: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
  is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
apply (case_tac "aa")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
apply  (auto elim!: halloc_elim_cases dest!: new_AddrD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
       intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   292
lemma halloc_type_sound: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   293
"\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s); wf_prog G; s1\<Colon>\<preceq>(G, L);
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
  T = obj_ty \<lparr>tag=oi,values=fs\<rparr>; is_type G T\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
  (x,s)\<Colon>\<preceq>(G, L) \<and> (x = None \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
apply (auto elim!: halloc_conforms)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
apply (case_tac "aa")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
apply (subst obj_ty_eq)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
apply  (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
lemma sxalloc_type_sound: 
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: 13601
diff changeset
   303
 "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<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: 13601
diff changeset
   304
  case fst s1 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: 13601
diff changeset
   305
    None \<Rightarrow> s2 = s1 
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: 13601
diff changeset
   306
  | Some abr \<Rightarrow> (case abr 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: 13601
diff changeset
   307
                   Xcpt x \<Rightarrow> (\<exists>a. fst s2 = Some(Xcpt (Loc 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: 13601
diff changeset
   308
                                  (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<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: 13601
diff changeset
   309
                 | Jump j \<Rightarrow> s2 = s1
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: 13601
diff changeset
   310
                 | Error e \<Rightarrow> s2 = s1)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
apply (erule sxalloc.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
apply   auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
apply (rule halloc_conforms [THEN conforms_xconf])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
apply     (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
lemma wt_init_comp_ty: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
"is_acc_type G (pid C) T \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
apply (unfold init_comp_ty_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
apply (clarsimp simp add: accessible_in_RefT_simp 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
                          is_acc_type_def is_acc_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
declare fun_upd_same [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
declare fun_upd_apply [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
37956
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   330
definition
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   331
  DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   332
where
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   333
  "G\<turnstile>mode\<rightarrow>D\<preceq>t = (mode = IntVir \<longrightarrow> is_class G D \<and> 
ee939247b2fb modernized/unified some specifications;
wenzelm
parents: 36635
diff changeset
   334
                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
lemma DynT_propI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
 "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
  \<Longrightarrow>  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
proof (unfold DynT_prop_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
  assume state_conform: "(x,s)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
     and      statT_a': "G,s\<turnstile>a'\<Colon>\<preceq>RefT statT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
     and            wf: "wf_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
     and          mode: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
  let ?invCls = "(invocation_class mode s a' statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
  let ?IntVir = "mode = IntVir"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
  let ?Concl  = "\<lambda>invCls. is_class G invCls \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
                          (if \<exists>T. statT = ArrayT T
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
                                  then invCls = Object
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
                                  else G\<turnstile>Class invCls\<preceq>RefT statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
  show "?IntVir \<longrightarrow> ?Concl ?invCls"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
  proof  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
    assume modeIntVir: ?IntVir 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
    with mode have not_Null: "a' \<noteq> Null" ..
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
    from statT_a' not_Null state_conform 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
    obtain a obj 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
      where obj_props:  "a' = Addr a" "globs s (Inl a) = Some obj"   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
                        "G\<turnstile>obj_ty obj\<preceq>RefT statT" "is_type G (obj_ty obj)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
      by (blast dest: conforms_RefTD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
    show "?Concl ?invCls"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
    proof (cases "tag obj")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
      case CInst
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
      with modeIntVir obj_props
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
      show ?thesis 
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
   364
        by (auto dest!: widen_Array2)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
      case Arr
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
   367
      from Arr obtain T where "obj_ty obj = T.[]" by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
      moreover from Arr have "obj_class obj = Object" 
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
   369
        by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
      moreover note modeIntVir obj_props wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
      ultimately show ?thesis by (auto dest!: widen_Array )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
lemma invocation_methd:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
"\<lbrakk>wf_prog G; statT \<noteq> NullT; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
 (\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
 (\<forall>     I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
 (\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
 G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
 dynlookup G statT (invocation_class mode s a' statT) sig = Some m \<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
\<Longrightarrow> methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
  assume         wf: "wf_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
     and  not_NullT: "statT \<noteq> NullT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
     and statC_prop: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
     and statI_prop: "(\<forall> I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
     and statA_prop: "(\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
     and  invC_prop: "G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
     and  dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
                      = Some m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
  proof (cases statT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
    case NullT
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
    with not_NullT show ?thesis by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
    case IfaceT
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
    with statI_prop obtain I 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
      where    statI: "statT = IfaceT I" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
            is_iface: "is_iface G I"     and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
          not_SuperM: "mode \<noteq> SuperM" by blast            
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
    show ?thesis 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
    proof (cases mode)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
      case Static
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
      with wf dynlookup statI is_iface 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   409
        by (auto simp add: invocation_declclass_def dynlookup_def 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
                           dynimethd_def dynmethd_C_C 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   411
                    intro: dynmethd_declclass
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   412
                    dest!: wf_imethdsD
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
   413
                     dest: table_of_map_SomeI)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   414
    next        
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
      case SuperM
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
      with not_SuperM show ?thesis ..
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
      case IntVir
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
      with wf dynlookup IfaceT invC_prop show ?thesis 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   420
        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
                           DynT_prop_def
46714
a7ca72710dfe tuned proofs;
wenzelm
parents: 44890
diff changeset
   422
                    intro: methd_declclass dynmethd_declclass)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
    case ClassT
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
    proof (cases mode)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
      case Static
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
      with wf ClassT dynlookup statC_prop 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
                               intro: dynmethd_declclass)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
      case SuperM
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
      with wf ClassT dynlookup statC_prop 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
                               intro: dynmethd_declclass)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
      case IntVir
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
      with wf ClassT dynlookup statC_prop invC_prop 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   441
        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
                           DynT_prop_def
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   443
                    intro: dynmethd_declclass)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
    case ArrayT
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
    proof (cases mode)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
      case Static
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
      with wf ArrayT dynlookup show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   451
        by (auto simp add: invocation_declclass_def dynlookup_def 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
                           dynimethd_def dynmethd_C_C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
                    intro: dynmethd_declclass
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
                     dest: table_of_map_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
      case SuperM
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
      with ArrayT statA_prop show ?thesis by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
      case IntVir
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
      with wf ArrayT dynlookup invC_prop show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   461
        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
                           DynT_prop_def dynmethd_C_C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
                    intro: dynmethd_declclass
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
                     dest: table_of_map_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
qed
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   468
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
lemma DynT_mheadsD: 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   470
"\<lbrakk>G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT; 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
  wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   472
  (statDeclT,sm) \<in> mheads G C statT sig; 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   473
  invC = invocation_class (invmode sm e) s a' statT;
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   474
  declC =invocation_declclass G (invmode sm e) s a' statT sig
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
 \<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
  \<exists> dm. 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   477
  methd G declC sig = Some dm \<and> dynlookup G statT invC sig = Some dm  \<and> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   478
  G\<turnstile>resTy (mthd dm)\<preceq>resTy sm \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
  wf_mdecl G declC (sig, mthd dm) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
  declC = declclass dm \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
  is_static dm = is_static sm \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
  is_class G invC \<and> is_class G declC  \<and> G\<turnstile>invC\<preceq>\<^sub>C declC \<and>  
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   483
  (if invmode sm e = IntVir
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
      then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
      else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
            \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and> 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   487
            statDeclT = ClassT (declclass dm))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
proof -
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   489
  assume invC_prop: "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
     and        wf: "wf_prog G" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
     and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   492
     and        sm: "(statDeclT,sm) \<in> mheads G C statT sig" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   493
     and      invC: "invC = invocation_class (invmode sm e) s a' statT"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
     and     declC: "declC = 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   495
                    invocation_declclass G (invmode sm e) s a' statT sig"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
  from wt_e wf have type_statT: "is_type G (RefT statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
    by (auto dest: ty_expr_is_type)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
  from sm have not_Null: "statT \<noteq> NullT" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
  from type_statT 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
  have wf_C: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
    by (auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
  from type_statT wt_e 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
  have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   504
                                        invmode sm e \<noteq> SuperM)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
    by (auto dest: invocationTypeExpr_noClassD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
  from wt_e
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   507
  have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode sm e \<noteq> SuperM)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
    by (auto dest: invocationTypeExpr_noClassD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
  show ?thesis
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   510
  proof (cases "invmode sm e = IntVir")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
    case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
    with invC_prop not_Null
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
    have invC_prop': " is_class G invC \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
                      (if (\<exists>T. statT=ArrayT T) then invC=Object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
                                              else G\<turnstile>Class invC\<preceq>RefT statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
      by (auto simp add: DynT_prop_def) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
    from True 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
    have "\<not> is_static sm"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   519
      by (simp add: invmode_IntVir_eq member_is_static_simp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
    with invC_prop' not_Null
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
    have "G,statT \<turnstile> invC valid_lookup_cls_for (is_static sm)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
      by (cases statT) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
    with sm wf type_statT obtain dm where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
           dm: "dynlookup G statT invC sig = Some dm" and
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   525
      resT_dm: "G\<turnstile>resTy (mthd dm)\<preceq>resTy sm"      and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
       static: "is_static dm = is_static sm"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   527
      by  - (drule dynamic_mheadsD,force+)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
    with declC invC not_Null 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
    have declC': "declC = (declclass dm)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
      by (auto simp add: invocation_declclass_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
    with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
    have dm': "methd G declC sig = Some dm"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
      by - (drule invocation_methd,auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
    from wf dm invC_prop' declC' type_statT 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
      by (auto dest: dynlookup_declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
    from wf dm' declC_prop declC' 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
      by (auto dest: methd_wf_mdecl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
    from invC_prop' 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
    have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
      by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
    from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   544
         dm
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
    show ?thesis by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
    case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
    with type_statT wf invC not_Null wf_I wf_A
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
    have invC_prop': "is_class G invC \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
                     ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   551
                      (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
        by (case_tac "statT") (auto simp add: invocation_class_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
                                       split: inv_mode.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
    with not_Null wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
                                            dynimethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
    from sm wf wt_e not_Null False invC_prop' obtain "dm" where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
                    dm: "methd G invC sig = Some dm"          and
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   560
        eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32693
diff changeset
   561
             eq_mheads:"sm=mhead (mthd dm) "
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   562
      by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   563
    then have static: "is_static dm = is_static sm" by - (auto)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
    with declC invC dynlookup_static dm
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
    have declC': "declC = (declclass dm)"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
      by (auto simp add: invocation_declclass_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
    from invC_prop' wf declC' dm 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
    have dm': "methd G declC sig = Some dm"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
      by (auto intro: methd_declclass)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   570
    from dynlookup_static dm 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   571
    have dm'': "dynlookup G statT invC sig = Some dm"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   572
      by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
    from wf dm invC_prop' declC' type_statT 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
      by (auto dest: methd_declC )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
    then have declC_prop1: "invC=Object \<longrightarrow> declC=Object"  by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
    from wf dm' declC_prop declC' 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
      by (auto dest: methd_wf_mdecl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
    from invC_prop' declC_prop declC_prop1
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
    have statC_prop: "(   (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
                       \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object))" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
      by auto
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   584
    from False dm' dm'' wf_dm invC_prop' declC_prop statC_prop declC' 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
         eq_declC_sm_dm eq_mheads static
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
    show ?thesis by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
  qed
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: 13601
diff changeset
   588
qed
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: 13601
diff changeset
   589
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: 13601
diff changeset
   590
corollary DynT_mheadsE [consumes 7]: 
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: 13601
diff changeset
   591
--{* Same as @{text DynT_mheadsD} but better suited for application in 
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: 13601
diff changeset
   592
typesafety proof   *}
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: 13601
diff changeset
   593
 assumes invC_compatible: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT" 
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: 13601
diff changeset
   594
     and wf: "wf_prog G" 
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: 13601
diff changeset
   595
     and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
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: 13601
diff changeset
   596
     and mheads: "(statDeclT,sm) \<in> mheads G C statT sig"
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: 13601
diff changeset
   597
     and mode: "mode=invmode sm e" 
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: 13601
diff changeset
   598
     and invC: "invC = invocation_class mode s a' statT"
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: 13601
diff changeset
   599
     and declC: "declC =invocation_declclass G mode s a' statT sig"
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: 13601
diff changeset
   600
     and dm: "\<And> dm. \<lbrakk>methd G declC sig = Some dm; 
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: 13601
diff changeset
   601
                      dynlookup G statT invC sig = Some dm; 
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: 13601
diff changeset
   602
                      G\<turnstile>resTy (mthd dm)\<preceq>resTy sm; 
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: 13601
diff changeset
   603
                      wf_mdecl G declC (sig, mthd dm);
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: 13601
diff changeset
   604
                      declC = declclass dm;
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: 13601
diff changeset
   605
                      is_static dm = is_static sm;  
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: 13601
diff changeset
   606
                      is_class G invC; is_class G declC; G\<turnstile>invC\<preceq>\<^sub>C declC;  
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: 13601
diff changeset
   607
                      (if invmode sm e = IntVir
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: 13601
diff changeset
   608
                      then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
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: 13601
diff changeset
   609
                      else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
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: 13601
diff changeset
   610
                             \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<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: 13601
diff changeset
   611
                             statDeclT = ClassT (declclass dm))\<rbrakk> \<Longrightarrow> 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: 13601
diff changeset
   612
   shows "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: 13601
diff changeset
   613
proof -
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: 13601
diff changeset
   614
    from invC_compatible mode have "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" by simp 
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: 13601
diff changeset
   615
    moreover note wf wt_e mheads
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: 13601
diff changeset
   616
    moreover from invC mode 
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: 13601
diff changeset
   617
    have "invC = invocation_class (invmode sm e) s a' statT" by simp
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: 13601
diff changeset
   618
    moreover from declC mode 
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: 13601
diff changeset
   619
    have "declC =invocation_declclass G (invmode sm e) s a' statT sig" by simp
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: 13601
diff changeset
   620
    ultimately show ?thesis
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: 13601
diff changeset
   621
      by (rule DynT_mheadsD [THEN exE,rule_format])
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: 13601
diff changeset
   622
         (elim conjE,rule dm)
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: 13601
diff changeset
   623
qed
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: 13601
diff changeset
   624
   
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
lemma DynT_conf: "\<lbrakk>G\<turnstile>invocation_class mode s a' statT \<preceq>\<^sub>C declC; wf_prog G;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
 isrtype G (statT);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
 G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; mode = IntVir \<longrightarrow> a' \<noteq> Null;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
  mode \<noteq> IntVir \<longrightarrow>    (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
                    \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
 \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
apply (case_tac "mode = IntVir")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
apply (drule conf_RefTD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
apply (force intro!: conf_AddrI 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
            simp add: obj_class_def split add: obj_tag.split_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
apply    (erule (1) widen.subcls [THEN conf_widen])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
apply    (erule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
apply    (frule widen_Object) apply (erule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
apply    (erule (1) conf_widen) apply (erule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   645
lemma Ass_lemma:
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   646
"\<lbrakk> G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2;
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   647
   G,s2\<turnstile>v\<Colon>\<preceq>eT;s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)\<rbrakk>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   648
\<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   649
      (normal (assign f v (Norm s2)) \<longrightarrow> G,store (assign f v (Norm s2))\<turnstile>v\<Colon>\<preceq>eT)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
apply (drule eval_gext', clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
apply (erule conf_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
    x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
apply (auto split add: split_abrupt_if simp add: throw_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
apply (erule conforms_xconf)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
apply (frule conf_RefTD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
apply (auto elim: widen.subcls [THEN conf_widen])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
lemma Try_lemma: "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
 (Some (Xcpt (Loc a)), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
 \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
apply (rule conforms_allocL)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
apply  (erule conforms_NormI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
apply (auto intro!: conf_AddrI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
lemma Fin_lemma: 
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: 13601
diff changeset
   674
"\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<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: 13601
diff changeset
   675
  dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
\<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
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: 13601
diff changeset
   677
apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   680
lemma FVar_lemma1: 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   681
"\<lbrakk>table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   682
  x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class statC; wf_prog G; G\<turnstile>statC\<preceq>\<^sub>C statDeclC; 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   683
  statDeclC \<noteq> Object; 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   684
  class G statDeclC = Some y; (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   685
  inited statDeclC (globs s1); 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   686
  (if static f then id else np a) x2 = None\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
 \<Longrightarrow>  
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   688
  \<exists>obj. globs s2 (if static f then Inr statDeclC else Inl (the_Addr a)) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   689
                  = Some obj \<and> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   690
  var_tys G (tag obj)  (if static f then Inr statDeclC else Inl(the_Addr a)) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   691
          (Inl(fn,statDeclC)) = Some (type f)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
apply (drule initedD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
apply (frule subcls_is_class2, simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
apply (case_tac "static f")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
apply  (drule (1) rev_gext_objD, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
apply  (frule fields_declC, erule wf_ws_prog, simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
apply  (rule var_tys_Some_eq [THEN iffD2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
apply  (erule fields_table_SomeI, simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
apply (auto dest!: widen_Array split add: obj_tag.split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
apply (rule fields_table_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
apply (auto elim!: fields_mono subcls_is_class2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   708
lemma FVar_lemma2: "error_free state
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   709
       \<Longrightarrow> error_free
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   710
           (assign
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   711
             (\<lambda>v. supd
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   712
                   (upd_gobj
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   713
                     (if static field then Inr statDeclC
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   714
                      else Inl (the_Addr a))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   715
                     (Inl (fn, statDeclC)) v))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   716
             w state)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   717
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   718
  assume error_free: "error_free state"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   719
  obtain a s where "state=(a,s)"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
   720
    by (cases state)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   721
  with error_free
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   722
  show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   723
    by (cases a) auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   724
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   725
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   726
declare split_paired_All [simp del] split_paired_Ex [simp del] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   727
declare split_if     [split del] split_if_asm     [split del] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   728
        option.split [split del] option.split_asm [split del]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   729
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   730
declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   731
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
lemma FVar_lemma: 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   733
"\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   734
  G\<turnstile>statC\<preceq>\<^sub>C statDeclC;  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   735
  table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   736
  wf_prog G;   
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   737
  x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class statC; 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   738
  statDeclC \<noteq> Object; class G statDeclC = Some y;   
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   739
  (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited statDeclC (globs s1)\<rbrakk> \<Longrightarrow>  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
  G,s2'\<turnstile>v\<Colon>\<preceq>type field \<and> s2'\<le>|f\<preceq>type field\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
apply (unfold assign_conforms_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
apply (drule sym)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
apply (clarsimp simp add: fvar_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
apply (drule (9) FVar_lemma1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
apply (clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
apply clarsimp
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   748
apply (rule conjI)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   749
apply   clarsimp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   750
apply   (drule (1) rev_gext_objD)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   751
apply   (force elim!: conforms_upd_gobj)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   752
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   753
apply   (blast intro: FVar_lemma2)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
done
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   755
declare split_paired_All [simp] split_paired_Ex [simp] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   756
declare split_if     [split] split_if_asm     [split] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   757
        option.split [split] option.split_asm [split]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   758
declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   759
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   761
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
 the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
\<rbrakk> \<Longrightarrow> G,s\<turnstile>the ((values obj) (Inr (the_Intg i')))\<Colon>\<preceq>Tb"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
apply (erule widen_Array_Array [THEN conf_widen])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
apply  (erule_tac [2] wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
defer apply assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
apply (force intro: var_tys_Some_eq [THEN iffD2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
14700
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14030
diff changeset
   772
lemma obj_split: "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
2f885b7e5ba7 reimplementation of HOL records; only one type is created for
schirmer
parents: 14030
diff changeset
   773
  by (cases obj) auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   775
lemma AVar_lemma2: "error_free state 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   776
       \<Longrightarrow> error_free
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   777
           (assign
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   778
             (\<lambda>v (x, s').
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   779
                 ((raise_if (\<not> G,s'\<turnstile>v fits T) ArrStore) x,
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   780
                  upd_gobj (Inl a) (Inr (the_Intg i)) v s'))
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   781
             w state)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   782
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   783
  assume error_free: "error_free state"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   784
  obtain a s where "state=(a,s)"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
   785
    by (cases state)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   786
  with error_free
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   787
  show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   788
    by (cases a) auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   789
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   790
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
lemma AVar_lemma: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
  ((v,f), Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
  (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2\<rbrakk> \<Longrightarrow> G,s2'\<turnstile>v\<Colon>\<preceq>Ta \<and> s2'\<le>|f\<preceq>Ta\<Colon>\<preceq>(G, L)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
apply (unfold assign_conforms_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
apply (drule sym)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
apply (clarsimp simp add: avar_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
apply (drule (1) conf_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
apply (drule conf_RefTD, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
apply (subgoal_tac "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
apply   (rule obj_split)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
apply (frule obj_ty_widenD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
apply (auto dest!: widen_Class)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   805
apply   (force dest: AVar_lemma1)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   806
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   807
apply   (force elim!: fits_Array dest: gext_objD 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   808
         intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
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: 13601
diff changeset
   811
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   812
section "Call"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
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: 13601
diff changeset
   815
  wf_mhead G P sig mh;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
  list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
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: 13601
diff changeset
   817
  G,s\<turnstile>empty (pars mh[\<mapsto>]pvs)
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: 13601
diff changeset
   818
      [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
apply (unfold wf_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   820
apply clarify
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: 13601
diff changeset
   821
apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   822
apply (drule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   823
apply (erule (2) conf_list_widen)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   824
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   825
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   826
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   827
lemma lconf_map_lname [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
  "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
   =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   830
  (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
apply (unfold lconf_def)
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: 13601
diff changeset
   832
apply (auto split add: lname.splits)
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: 13601
diff changeset
   833
done
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: 13601
diff changeset
   834
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: 13601
diff changeset
   835
lemma wlconf_map_lname [simp]: 
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: 13601
diff changeset
   836
  "G,s\<turnstile>(lname_case l1 l2)[\<sim>\<Colon>\<preceq>](lname_case L1 L2)
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: 13601
diff changeset
   837
   =
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: 13601
diff changeset
   838
  (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
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: 13601
diff changeset
   839
apply (unfold wlconf_def)
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: 13601
diff changeset
   840
apply (auto split add: lname.splits)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   841
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   842
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   843
lemma lconf_map_ename [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   844
  "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   845
   =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   846
  (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   847
apply (unfold lconf_def)
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: 13601
diff changeset
   848
apply (auto split add: ename.splits)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   849
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   850
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: 13601
diff changeset
   851
lemma wlconf_map_ename [simp]:
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: 13601
diff changeset
   852
  "G,s\<turnstile>(ename_case l1 l2)[\<sim>\<Colon>\<preceq>](ename_case L1 L2)
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: 13601
diff changeset
   853
   =
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: 13601
diff changeset
   854
  (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
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: 13601
diff changeset
   855
apply (unfold wlconf_def)
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: 13601
diff changeset
   856
apply (auto split add: ename.splits)
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: 13601
diff changeset
   857
done
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: 13601
diff changeset
   858
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: 13601
diff changeset
   859
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
lemma defval_conf1 [rule_format (no_asm), elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
  "is_type G T \<longrightarrow> (\<exists>v\<in>Some (default_val T): G,s\<turnstile>v\<Colon>\<preceq>T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
apply (unfold conf_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
apply (induct "T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
apply (auto intro: prim_ty.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   866
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   867
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: 13601
diff changeset
   868
lemma np_no_jump: "x\<noteq>Some (Jump j) \<Longrightarrow> (np a') x \<noteq> Some (Jump j)"
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: 13601
diff changeset
   869
by (auto simp add: abrupt_if_def)
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: 13601
diff changeset
   870
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   871
declare split_paired_All [simp del] split_paired_Ex [simp del] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   872
declare split_if     [split del] split_if_asm     [split del] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   873
        option.split [split del] option.split_asm [split del]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   874
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   875
declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   876
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
lemma conforms_init_lvars: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
"\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   879
  list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
  (x, s)\<Colon>\<preceq>(G, L); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
  methd G declC sig = Some dm;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   882
  isrtype G statT;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   883
  G\<turnstile>invC\<preceq>\<^sub>C declC; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   884
  G,s\<turnstile>a'\<Colon>\<preceq>RefT statT;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
  invmode (mhd sm) e = IntVir \<longrightarrow> a' \<noteq> Null; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   886
  invmode (mhd sm) e \<noteq> IntVir \<longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
       (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   888
    \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
  invC  = invocation_class (invmode (mhd sm) e) s a' statT;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   890
  declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
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: 13601
diff changeset
   891
  x\<noteq>Some (Jump Ret) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   892
 \<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   893
  init_lvars G declC sig (invmode (mhd sm) e) a'  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   894
  pvs (x,s)\<Colon>\<preceq>(G,\<lambda> k. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   895
                (case k of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   896
                   EName e \<Rightarrow> (case e of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   897
                                 VNam v 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   898
                                  \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   899
                                        (pars (mthd dm)[\<mapsto>]parTs sig)) v
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   900
                               | Res \<Rightarrow> Some (resTy (mthd dm)))
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   901
                 | This \<Rightarrow> if (is_static (mthd sm)) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   902
                              then None else Some (Class declC)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   903
apply (simp add: init_lvars_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   904
apply (rule conforms_set_locals)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   905
apply  (simp (no_asm_simp) split add: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
apply (drule  (4) DynT_conf)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   907
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   908
(* apply intro *)
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: 13601
diff changeset
   909
apply (drule (3) conforms_init_lvars_lemma 
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: 13601
diff changeset
   910
                 [where ?lvars="(lcls (mbody (mthd dm)))"])
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
apply (case_tac "dm",simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   912
apply (rule conjI)
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: 13601
diff changeset
   913
apply (unfold wlconf_def, clarify)
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: 13601
diff changeset
   914
apply   (clarsimp simp add: wf_mhead_def is_acc_type_def)
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: 13601
diff changeset
   915
apply   (case_tac "is_static sm")
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: 13601
diff changeset
   916
apply     simp
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: 13601
diff changeset
   917
apply     simp
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: 13601
diff changeset
   918
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: 13601
diff changeset
   919
apply   simp
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: 13601
diff changeset
   920
apply   (case_tac "is_static sm")
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: 13601
diff changeset
   921
apply     simp
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: 13601
diff changeset
   922
apply     (simp add: np_no_jump)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
done
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   924
declare split_paired_All [simp] split_paired_Ex [simp] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   925
declare split_if     [split] split_if_asm     [split] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   926
        option.split [split] option.split_asm [split]
24019
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   927
declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
67bde7cfcf10 tuned ML/simproc declarations;
wenzelm
parents: 23373
diff changeset
   928
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   931
subsection "accessibility"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   932
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   933
theorem dynamic_field_access_ok:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   934
  assumes wf: "wf_prog G" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   935
    not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   936
   conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   937
   conform_s: "s\<Colon>\<preceq>(G, L)" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   938
    normal_s: "normal s" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   939
        wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   940
           f: "accfield G accC statC fn = Some f" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   941
        dynC: "if stat then dynC=declclass f  
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   942
                       else dynC=obj_class (lookup_obj (store s) a)" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   943
        stat: "if stat then (is_static f) else (\<not> is_static f)"
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: 13601
diff changeset
   944
  shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)\<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: 13601
diff changeset
   945
         G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
proof (cases "stat")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   947
  case True
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   948
  with stat have static: "(is_static f)" by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   949
  from True dynC 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   950
  have dynC': "dynC=declclass f" by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   951
  with f
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   952
  have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   953
    by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   954
  moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   955
  from wt_e wf have "is_class G statC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   956
    by (auto dest!: ty_expr_is_type)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   957
  moreover note wf dynC'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   958
  ultimately have
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   959
     "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   960
    by (auto dest: fields_declC)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   961
  with dynC' f static wf
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   962
  show ?thesis
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   963
    by (auto dest: static_to_dynamic_accessible_from_static
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   964
            dest!: accfield_accessibleD )
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   965
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   966
  case False
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   967
  with wf conform_a not_Null conform_s dynC
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   968
  obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   969
    "is_class G dynC"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   970
    by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   971
              dest: obj_ty_obj_class1
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   972
          simp add: obj_ty_obj_class )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   973
  with wf f
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   974
  have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   975
    by (auto simp add: accfield_def Let_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   976
                 dest: fields_mono
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   977
                dest!: table_of_remap_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   978
  moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   979
  from f subclseq
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   980
  have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
   981
    by (auto intro!: static_to_dynamic_accessible_from wf
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   982
               dest: accfield_accessibleD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   983
  ultimately show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
    by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   987
lemma error_free_field_access:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   988
  assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   989
              wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   990
         eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   991
            eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   992
           conf_s2: "s2\<Colon>\<preceq>(G, L)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   993
            conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   994
              fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   995
                wf: "wf_prog G"   
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   996
  shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   997
proof -
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   998
  from fvar
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
   999
  have store_s2': "store s2'=store s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1000
    by (cases s2) (simp add: fvar_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1001
  with fvar conf_s2 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1002
  have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1003
    by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1004
  from eval_init 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1005
  have initd_statDeclC_s1: "initd statDeclC s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1006
    by (rule init_yields_initd)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1007
  with eval_e store_s2'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1008
  have initd_statDeclC_s2': "initd statDeclC s2'"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1009
    by (auto dest: eval_gext intro: inited_gext)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1010
  show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1011
  proof (cases "normal s2'")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1012
    case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1013
    then show ?thesis 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1014
      by (auto simp add: check_field_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1015
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1016
    case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1017
    with fvar store_s2' 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1018
    have not_Null: "\<not> (is_static f) \<longrightarrow> a\<noteq>Null" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1019
      by (cases s2) (auto simp add: fvar_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1020
    from True fvar store_s2'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1021
    have "normal s2"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1022
      by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1023
    with conf_a store_s2'
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1024
    have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1025
      by simp
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1026
    from conf_a' conf_s2' True initd_statDeclC_s2' 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1027
      dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1028
                                   True wt_e accfield ] 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1029
    show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1030
      by  (cases "is_static f")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1031
          (auto dest!: initedD
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1032
           simp add: check_field_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1033
  qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1034
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1035
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1036
lemma call_access_ok:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1037
  assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1038
      and        wf: "wf_prog G" 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1039
      and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1040
      and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1041
      and      invC: "invC = invocation_class (invmode statM e) s a statT"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1042
  shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1043
  G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1044
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1045
  from wt_e wf have type_statT: "is_type G (RefT statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1046
    by (auto dest: ty_expr_is_type)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1047
  from statM have not_Null: "statT \<noteq> NullT" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1048
  from type_statT wt_e 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1049
  have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1050
                                        invmode statM e \<noteq> SuperM)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1051
    by (auto dest: invocationTypeExpr_noClassD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1052
  from wt_e
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1053
  have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode statM e \<noteq> SuperM)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1054
    by (auto dest: invocationTypeExpr_noClassD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1055
  show ?thesis
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1056
  proof (cases "invmode statM e = IntVir")
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1057
    case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1058
    with invC_prop not_Null
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1059
    have invC_prop': "is_class G invC \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1060
                      (if (\<exists>T. statT=ArrayT T) then invC=Object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1061
                                              else G\<turnstile>Class invC\<preceq>RefT statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1062
      by (auto simp add: DynT_prop_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1063
    with True not_Null
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1064
    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1065
     by (cases statT) (auto simp add: invmode_def) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1066
    with statM type_statT wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1067
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1068
      by - (rule dynlookup_access,auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1069
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1070
    case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1071
    with type_statT wf invC not_Null wf_I wf_A
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1072
    have invC_prop': " is_class G invC \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1073
                      ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1074
                      (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1075
        by (case_tac "statT") (auto simp add: invocation_class_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1076
                                       split: inv_mode.splits)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1077
    with not_Null wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1078
    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1079
      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1080
                                            dynimethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1081
   from statM wf wt_e not_Null False invC_prop' obtain dynM where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1082
                "accmethd G accC invC sig = Some dynM" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1083
     by (auto dest!: static_mheadsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1084
   from invC_prop' False not_Null wf_I
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1085
   have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1086
     by (cases statT) (auto simp add: invmode_def) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1087
   with statM type_statT wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1088
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1089
      by - (rule dynlookup_access,auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1090
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1091
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1092
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1093
lemma error_free_call_access:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1094
  assumes
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1095
   eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1096
        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1097
       statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1098
               = {((statDeclT, statM), pTs')}" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1099
     conf_s2: "s2\<Colon>\<preceq>(G, L)" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1100
      conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1101
     invProp: "normal s3 \<Longrightarrow>
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1102
                G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1103
          s3: "s3=init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1104
                        (invmode statM e) a vs s2" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1105
        invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1106
    invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1107
                             a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1108
          wf: "wf_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1109
  shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1110
   = s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1111
proof (cases "normal s2")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1112
  case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1113
  with s3 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1114
  have "abrupt s3 = abrupt s2"  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1115
    by (auto simp add: init_lvars_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1116
  with False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1117
  show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1118
    by (auto simp add: check_method_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1119
next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1120
  case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1121
  note normal_s2 = True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1122
  with eval_args
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1123
  have normal_s1: "normal s1"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1124
    by (cases "normal s1") auto
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1125
  with conf_a eval_args 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1126
  have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1127
    by (auto dest: eval_gext intro: conf_gext)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1128
  show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1129
  proof (cases "a=Null \<longrightarrow> (is_static statM)")
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1130
    case False
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1131
    then obtain "\<not> is_static statM" "a=Null" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1132
      by blast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1133
    with normal_s2 s3
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1134
    have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1135
      by (auto simp add: init_lvars_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1136
    then show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1137
      by (auto simp add: check_method_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1138
  next
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1139
    case True
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1140
    from statM 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1141
    obtain
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1142
      statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1143
      by (blast dest: max_spec2mheads)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1144
    from True normal_s2 s3
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1145
    have "normal s3"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1146
      by (auto simp add: init_lvars_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1147
    then have "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1148
      by (rule invProp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1149
    with wt_e statM' wf invC
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1150
    obtain dynM where 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1151
      dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1152
      acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1153
                          in invC dyn_accessible_from accC"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1154
      by (force dest!: call_access_ok)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1155
    moreover
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1156
    from s3 invC
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1157
    have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1158
      by (cases s2,cases "invmode statM e") 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1159
         (simp add: init_lvars_def2 del: invmode_Static_eq)+
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1160
    ultimately
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1161
    show ?thesis
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1162
      by (auto simp add: check_method_access_def Let_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1163
  qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1164
qed
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12858
diff changeset
  1165
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: 13601
diff changeset
  1166
lemma map_upds_eq_length_append_simp:
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: 13601
diff changeset
  1167
  "\<And> tab qs. length ps = length qs \<Longrightarrow>  tab(ps[\<mapsto>]qs@zs) = tab(ps[\<mapsto>]qs)"
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: 13601
diff changeset
  1168
proof (induct ps) 
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: 13601
diff changeset
  1169
  case Nil thus ?case by simp
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: 13601
diff changeset
  1170
next
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: 13601
diff changeset
  1171
  case (Cons p ps tab qs)
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
  1172
  from `length (p#ps) = length qs`
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
  1173
  obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
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: 13601
diff changeset
  1174
    by (cases qs) auto
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: 13601
diff changeset
  1175
  from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
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: 13601
diff changeset
  1176
    by (rule Cons.hyps)
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: 13601
diff changeset
  1177
  with qs show ?case 
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: 13601
diff changeset
  1178
    by simp
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: 13601
diff changeset
  1179
qed
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: 13601
diff changeset
  1180
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: 13601
diff changeset
  1181
lemma map_upds_upd_eq_length_simp:
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: 13601
diff changeset
  1182
  "\<And> tab qs x y. length ps = length qs 
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: 13601
diff changeset
  1183
                  \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
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: 13601
diff changeset
  1184
proof (induct "ps")
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: 13601
diff changeset
  1185
  case Nil thus ?case by simp
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: 13601
diff changeset
  1186
next
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: 13601
diff changeset
  1187
  case (Cons p ps tab qs x y)
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
  1188
  from `length (p#ps) = length qs`
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
  1189
  obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
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: 13601
diff changeset
  1190
    by (cases qs) auto
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: 13601
diff changeset
  1191
  from eq_length 
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: 13601
diff changeset
  1192
  have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
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: 13601
diff changeset
  1193
    by (rule Cons.hyps)
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: 13601
diff changeset
  1194
  with qs show ?case
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: 13601
diff changeset
  1195
    by simp
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: 13601
diff changeset
  1196
qed
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: 13601
diff changeset
  1197
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: 13601
diff changeset
  1198
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: 13601
diff changeset
  1199
lemma map_upd_cong: "tab=tab'\<Longrightarrow> tab(x\<mapsto>y) = tab'(x\<mapsto>y)"
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: 13601
diff changeset
  1200
by simp
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: 13601
diff changeset
  1201
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: 13601
diff changeset
  1202
lemma map_upd_cong_ext: "tab z=tab' z\<Longrightarrow> (tab(x\<mapsto>y)) z = (tab'(x\<mapsto>y)) 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: 13601
diff changeset
  1203
by (simp add: fun_upd_def)
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: 13601
diff changeset
  1204
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: 13601
diff changeset
  1205
lemma map_upds_cong: "tab=tab'\<Longrightarrow> tab(xs[\<mapsto>]ys) = tab'(xs[\<mapsto>]ys)"
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: 13601
diff changeset
  1206
by (cases xs) simp+
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: 13601
diff changeset
  1207
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: 13601
diff changeset
  1208
lemma map_upds_cong_ext: 
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: 13601
diff changeset
  1209
 "\<And> tab tab' ys. tab z=tab' z \<Longrightarrow> (tab(xs[\<mapsto>]ys)) z = (tab'(xs[\<mapsto>]ys)) 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: 13601
diff changeset
  1210
proof (induct xs)
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: 13601
diff changeset
  1211
  case Nil thus ?case by simp
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: 13601
diff changeset
  1212
next
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: 13601
diff changeset
  1213
  case (Cons x xs tab tab' ys)
14030
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1214
  note Hyps = this
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1215
  show ?case
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1216
  proof (cases ys)
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1217
    case Nil
23350
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
  1218
    with Hyps
50c5b0912a0c tuned proofs: avoid implicit prems;
wenzelm
parents: 23019
diff changeset
  1219
    show ?thesis by simp
14030
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1220
  next
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1221
    case (Cons y ys')
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1222
    have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
  1223
      by (iprover intro: Hyps map_upd_cong_ext)
14030
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1224
    with Cons show ?thesis
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1225
      by simp
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 13690
diff changeset
  1226
  qed
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: 13601
diff changeset
  1227
qed
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: 13601
diff changeset
  1228
   
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: 13601
diff changeset
  1229
lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
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: 13601
diff changeset
  1230
  by simp
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: 13601
diff changeset
  1231
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: 13601
diff changeset
  1232
lemma map_upds_eq_length_suffix: "\<And> tab qs. 
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: 13601
diff changeset
  1233
        length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
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: 13601
diff changeset
  1234
proof (induct ps)
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: 13601
diff changeset
  1235
  case Nil thus ?case by simp
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: 13601
diff changeset
  1236
next
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: 13601
diff changeset
  1237
  case (Cons p ps tab qs)
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: 13601
diff changeset
  1238
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
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: 13601
diff changeset
  1239
    by (cases qs) auto
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: 13601
diff changeset
  1240
  from eq_length
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: 13601
diff changeset
  1241
  have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
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: 13601
diff changeset
  1242
    by (rule Cons.hyps)
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: 13601
diff changeset
  1243
  with qs show ?case 
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: 13601
diff changeset
  1244
    by simp
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: 13601
diff changeset
  1245
qed
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: 13601
diff changeset
  1246
  
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: 13601
diff changeset
  1247
  
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: 13601
diff changeset
  1248
lemma map_upds_upds_eq_length_prefix_simp:
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: 13601
diff changeset
  1249
  "\<And> tab qs. length ps = length qs
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: 13601
diff changeset
  1250
              \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
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: 13601
diff changeset
  1251
proof (induct ps)
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: 13601
diff changeset
  1252
  case Nil thus ?case by simp
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: 13601
diff changeset
  1253
next
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: 13601
diff changeset
  1254
  case (Cons p ps tab qs)
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: 13601
diff changeset
  1255
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
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: 13601
diff changeset
  1256
    by (cases qs) auto
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: 13601
diff changeset
  1257
  from eq_length 
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: 13601
diff changeset
  1258
  have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
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: 13601
diff changeset
  1259
    by (rule Cons.hyps)
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: 13601
diff changeset
  1260
  with qs 
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: 13601
diff changeset
  1261
  show ?case by simp
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: 13601
diff changeset
  1262
qed
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: 13601
diff changeset
  1263
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: 13601
diff changeset
  1264
lemma map_upd_cut_irrelevant:
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: 13601
diff changeset
  1265
"\<lbrakk>(tab(x\<mapsto>y)) vn = Some el; (tab'(x\<mapsto>y)) vn = None\<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: 13601
diff changeset
  1266
    \<Longrightarrow> tab vn = Some el"
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: 13601
diff changeset
  1267
by (cases "tab' vn = None") (simp add: fun_upd_def)+
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: 13601
diff changeset
  1268
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: 13601
diff changeset
  1269
lemma map_upd_Some_expand: