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