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