src/HOL/Bali/AxCompl.thy
author wenzelm
Sat, 17 Oct 2009 14:43:18 +0200
changeset 32960 69916a850301
parent 31945 d5f186aa0bed
child 35069 09154b995ed8
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/AxCompl.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
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
     3
    Author:     David von Oheimb and Norbert Schirmer
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
Completeness proof for Axiomatic semantics of Java expressions and statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
    10
theory AxCompl imports AxSem begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\item proof structured by Most General Formulas (-> Thomas Kleymann)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
*}
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
    18
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
    19
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
    20
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
    21
           
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
section "set of not yet initialzed classes"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
 "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
lemmas finite_nyinitcls [simp] =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
lemma nyinitcls_set_locals_cong [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
  "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
lemma card_nyinitcls_abrupt_congE [elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
        "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
lemma nyinitcls_new_xcpt_var [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
apply (induct_tac "s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
lemma nyinitcls_init_lvars [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
  "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
apply (induct_tac "s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
apply (simp (no_asm) add: init_lvars_def2 split add: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
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
    82
lemma card_Suc_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
    83
  "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
lemma nyinitcls_le_SucD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
"\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
  card (nyinitcls G (x,init_class_obj G C s)) \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
apply (subgoal_tac 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
        "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
apply  clarsimp
13601
fd3e3d6b37b2 Adapted to new simplifier.
berghofe
parents: 13524
diff changeset
    93
apply  (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
apply   (auto dest!: not_initedD elim!: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
              simp add: nyinitcls_def inited_def split add: split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
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
    99
lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   100
by (rule inited_gext)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
apply (force dest!: inited_gext')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
lemma card_nyinitcls_gext: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
  "\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
apply (rule le_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
apply  (rule card_mono)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
apply   (rule finite_nyinitcls)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
apply  (erule nyinitcls_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
apply assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
section "init-le"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"            ("_\<turnstile>init\<le>_"  [51,51] 50)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
 "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
apply (unfold init_le_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
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
   128
lemma All_init_leD: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
 "\<forall>n::nat. G,(A::'a triple set)\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q::'a assn} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   130
  \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
apply (rule card_nyinitcls_bound)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
section "Most General Triples and Formulas"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
  remember_init_state :: "state assn"                ("\<doteq>")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
  "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
apply (unfold remember_init_state_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
  MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
  MGF_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
  MGFn_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
  "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
(* unused *)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   164
lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
apply (unfold MGF_def)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   166
apply (simp add:  ax_valids_def triple_valid_def2)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   167
apply (auto elim: evaln_eval)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   170
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
lemma MGF_res_eq_lemma [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
  "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
lemma MGFn_def2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
                    t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
apply (unfold MGFn_def MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
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
   183
lemma MGF_MGFn_iff: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   184
"G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
apply  (erule_tac [2] All_init_leD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
lemma MGFnD: 
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
   193
"G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
 G,A\<turnstile>{(\<lambda>Y' s' s. s' = s           \<and> P s) \<and>. G\<turnstile>init\<le>n}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
 t\<succ>  {(\<lambda>Y' s' s. G\<turnstile>s\<midarrow>t\<succ>\<rightarrow>(Y',s') \<and> P s) \<and>. G\<turnstile>init\<le>n}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
apply (unfold init_le_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
apply (simp (no_asm_use) add: MGFn_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
apply (erule (1) eval_gext [THEN card_nyinitcls_gext])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
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
   204
text {* To derive the most general formula, we can always assume a normal
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   205
state in the precondition, since abrupt cases can be handled uniformally by
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   206
the abrupt 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
   207
*}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
  G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
apply  (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
apply (rule ax_derivs.Abrupt [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
apply (clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
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
   218
lemma MGFNormalD: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   219
"G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
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
   225
text {* Additionally to @{text MGFNormalI}, we also expand the definition of 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   226
the most general formula here *} 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
lemma MGFn_NormalI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
"G,(A::state triple set)\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}t\<succ> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
 {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
apply (simp (no_asm_use) add: MGFn_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
apply  (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
apply (rule ax_derivs.Abrupt [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
apply (clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
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
   238
text {* To derive the most general formula, we can restrict ourselves to 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   239
welltyped terms, since all others can be uniformally handled by the hazard
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   240
rule. *} 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
lemma MGFn_free_wt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
  "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
    \<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
   \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
apply (rule MGFn_NormalI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
apply (rule ax_free_wt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
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
   250
text {* To derive the most general formula, we can restrict ourselves to 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   251
welltyped terms and assume that the state in the precondition conforms 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
   252
environment. All type violations can be uniformally handled by the hazard
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   253
rule. *} 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   254
lemma MGFn_free_wt_NormalConformI: 
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
   255
"(\<forall> T L C . \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T 
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   256
  \<longrightarrow> G,(A::state triple set)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   257
      \<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n) \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))}
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   258
      t\<succ> 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   259
      {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   260
 \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   261
apply (rule MGFn_NormalI)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   262
apply (rule ax_no_hazard)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   263
apply (rule ax_escape)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   264
apply (intro strip)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   265
apply (simp only: type_ok_def peek_and_def)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   266
apply (erule conjE)+
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
   267
apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   268
       erule conjE)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   269
apply (drule spec,drule spec, drule spec, drule (1) mp)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   270
apply (erule conseq12)
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   271
apply blast
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   272
done
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   273
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
   274
text {* To derive the most general formula, we can restrict ourselves to 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   275
welltyped terms and assume that the state in the precondition conforms 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
   276
environment and that the term is definetly assigned with respect to this state.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   277
All type violations can be uniformally handled by the hazard 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
   278
lemma MGFn_free_wt_da_NormalConformI: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   279
"(\<forall> T L C B. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>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
   280
  \<longrightarrow> G,(A::state triple set)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   281
      \<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n) \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   282
        \<and>. (\<lambda> s. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>B)}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   283
      t\<succ> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   284
      {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   285
 \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   286
apply (rule MGFn_NormalI)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   287
apply (rule ax_no_hazard)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   288
apply (rule ax_escape)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   289
apply (intro strip)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   290
apply (simp only: type_ok_def peek_and_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
   291
apply (erule conjE)+
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   292
apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   293
       erule conjE)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   294
apply (drule spec,drule spec, drule spec,drule spec, drule (1) mp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   295
apply (erule conseq12)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   296
apply blast
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   297
done
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
section "main lemmas"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
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
   301
lemma MGFn_Init: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   302
 assumes mgf_hyp: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   303
 shows "G,(A::state triple set)\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
proof (rule MGFn_free_wt [rule_format],elim exE,rule MGFn_NormalI)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
  fix T L accC
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
  assume "\<lparr>prg=G, cls=accC, lcl= L\<rparr>\<turnstile>\<langle>Init C\<rangle>\<^sub>s\<Colon>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
   307
  hence is_cls: "is_class G C"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
    by cases 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
   309
  show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>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
   310
            .Init C.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
            {\<lambda>Y s' s. G\<turnstile>s \<midarrow>\<langle>Init C\<rangle>\<^sub>s\<succ>\<rightarrow> (Y, s')}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   312
       (is "G,A\<turnstile>{Normal ?P} .Init C. {?R}")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   313
  proof (rule ax_cases [where ?C="initd C"])
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   314
    show "G,A\<turnstile>{Normal ?P  \<and>. initd C} .Init C. {?R}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   315
      by (rule ax_derivs.Done [THEN conseq1]) (fastsimp intro: init_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
   316
  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
   317
    have "G,A\<turnstile>{Normal (?P  \<and>. Not \<circ> initd C)} .Init C. {?R}" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   318
    proof (cases 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
   319
      case 0
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   320
      with is_cls
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   321
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   322
        by - (rule ax_impossible [THEN conseq1],fastsimp dest: nyinitcls_emptyD)
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
   323
    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
   324
      case (Suc m)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   325
      with mgf_hyp have mgf_hyp': "\<And> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   326
        by simp
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
   327
      from is_cls obtain c where c: "the (class G C) = c"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   328
        by auto
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
   329
      let ?Q= "(\<lambda>Y s' (x,s) . 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   330
          G\<turnstile> (x,init_class_obj G C s) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   331
             \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s'
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   332
          \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>m"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   333
      from c
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   334
      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
   335
      proof (rule ax_derivs.Init [where ?Q="?Q"])
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   336
        let ?P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s 
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
   337
                           \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>m)" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   338
        show "G,A\<turnstile>{Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
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
   339
                  .(if C = Object then Skip else Init (super c)). 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   340
                  {?Q}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   341
        proof (rule conseq1 [where ?P'="?P'"])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   342
          show "G,A\<turnstile>{?P'} .(if C = Object then Skip else Init (super c)). {?Q}"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   343
          proof (cases "C=Object")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   344
            case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   345
            have "G,A\<turnstile>{?P'} .Skip. {?Q}"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   346
              by (rule ax_derivs.Skip [THEN conseq1])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   347
                 (auto simp add: True intro: eval.Skip)
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
   348
            with True show ?thesis 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   349
              by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   350
          next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   351
            case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   352
            from mgf_hyp'
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   353
            have "G,A\<turnstile>{?P'} .Init (super c). {?Q}"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   354
              by (rule MGFnD' [THEN conseq12]) (fastsimp simp add: False c)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   355
            with False show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   356
              by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   357
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   358
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   359
          from Suc is_cls
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   360
          show "Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))
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
   361
                \<Rightarrow> ?P'"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   362
            by (fastsimp elim: nyinitcls_le_SucD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   363
        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
   364
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   365
        from mgf_hyp'
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   366
        show "\<forall>l. G,A\<turnstile>{?Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty} 
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
   367
                      .init c.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   368
                      {set_lvars l .; ?R}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   369
          apply (rule MGFnD' [THEN conseq12, THEN allI])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   370
          apply (clarsimp simp add: split_paired_all)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   371
          apply (rule eval.Init [OF c])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   372
          apply (insert c)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   373
          apply auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   374
          done
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   375
      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
   376
    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
   377
    thus "G,A\<turnstile>{Normal ?P  \<and>. Not \<circ> initd C} .Init C. {?R}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   378
      by clarsimp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   379
  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
   380
qed
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
lemma MGFn_Call: 
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
   384
  assumes mgf_methds: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   385
           "\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>(Methd C sig)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   386
  and mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   387
  and mgf_ps: "G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   388
  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
   389
  shows "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   390
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   391
  note inj_term_simps [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
   392
  fix T L accC' 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
   393
  assume wt: "\<lparr>prg=G,cls=accC',lcl = L\<rparr>\<turnstile>\<langle>({accC,statT,mode}e\<cdot>mn( {pTs'}ps))\<rangle>\<^sub>e\<Colon>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
   394
  then obtain pTs statDeclT statM where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   395
                 wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" 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
   396
              wt_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>ps\<Colon>\<doteq>pTs" 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
   397
                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   398
                         = {((statDeclT,statM),pTs')}" 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
   399
                 mode: "mode = invmode statM e" 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
   400
                    T: "T =Inl (resTy statM)" 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
   401
        eq_accC_accC': "accC=accC'"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   402
        by cases fastsimp+
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
   403
  let ?Q="(\<lambda>Y s1 (x,s) . x = None \<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
   404
              (\<exists>a. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<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
   405
                   (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>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
   406
                   \<and> Y = In1 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
   407
              (\<exists> P. normal 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
   408
                  \<longrightarrow> \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright>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
   409
          \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))::state assn"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   410
  let ?R="\<lambda>a. ((\<lambda>Y (x2,s2) (x,s) . x = None \<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
   411
                (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<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
   412
                          (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)\<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
   413
                          Y = \<lfloor>pvs\<rfloor>\<^sub>l \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2))) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   414
               \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L)))::state assn"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   415
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
   416
  show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>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
   417
                     (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<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
   418
                     (\<lambda>s. \<lparr>prg=G, cls=accC',lcl=L\<rparr> \<turnstile> dom (locals (store s)) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   419
                           \<guillemotright> \<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> 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
   420
             {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   421
             {\<lambda>Y s' s. \<exists>v. Y = \<lfloor>v\<rfloor>\<^sub>e \<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
   422
                           G\<turnstile>s \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v\<rightarrow> s'}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   423
    (is "G,A\<turnstile>{Normal ?P} {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ> {?S}")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   424
  proof (rule ax_derivs.Call [where ?Q="?Q" and ?R="?R"])
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   425
    from mgf_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
   426
    show "G,A\<turnstile>{Normal ?P} e-\<succ> {?Q}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   427
    proof (rule MGFnD' [THEN conseq12],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   428
      fix s0 s1 a
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   429
      assume conf_s0: "Norm s0\<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
   430
      assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   431
                     dom (locals s0) \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> 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
   432
      assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> 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
   433
      show "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<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
   434
            (abrupt s1 = None \<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
   435
              (\<exists>P. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> 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
   436
            \<and> s1\<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
   437
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   438
        from da obtain C where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   439
          da_e:  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
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
   440
                    dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   441
          da_ps: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm C \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> E" 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   442
          by cases (simp add: eq_accC_accC')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   443
        from eval_e conf_s0 wt_e da_e wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   444
        obtain "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   445
          and  "s1\<Colon>\<preceq>(G, L)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   446
          by (rule eval_type_soundE) simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   447
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   448
        {
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   449
          assume normal_s1: "normal s1"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   450
          have "\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   451
          proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   452
            from eval_e wt_e da_e wf normal_s1
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   453
            have "nrm C \<subseteq>  dom (locals (store s1))"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   454
              by (cases rule: da_good_approxE') iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   455
            with da_ps show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   456
              by (rule da_weakenE) iprover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   457
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   458
        }
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   459
        ultimately show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   460
          using eq_accC_accC' by simp
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
   461
      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
   462
    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
   463
  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
   464
    show "\<forall>a. G,A\<turnstile>{?Q\<leftarrow>In1 a} ps\<doteq>\<succ> {?R a}" (is "\<forall> a. ?PS a")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   465
    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
   466
      fix a  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   467
      show "?PS a"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   468
      proof (rule MGFnD' [OF mgf_ps, THEN conseq12],
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   469
             clarsimp simp add: eq_accC_accC' [symmetric])
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   470
        fix s0 s1 s2 vs
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   471
        assume conf_s1: "s1\<Colon>\<preceq>(G, L)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   472
        assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   473
        assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   474
        assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   475
        assume da_ps: "abrupt s1 = None \<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
   476
                       (\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   477
                               dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   478
        show "(\<exists>s1. G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1 \<and>
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
   479
                (abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<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
   480
                G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2) \<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
   481
              s2\<Colon>\<preceq>(G, L)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   482
        proof (cases "normal s1")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   483
          case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   484
          with da_ps obtain P where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   485
           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   486
            by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   487
          from eval_ps conf_s1 wt_args this wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   488
          have "s2\<Colon>\<preceq>(G, L)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   489
            by (rule eval_type_soundE)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   490
          with eval_e conf_a eval_ps 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   491
          show ?thesis 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   492
            by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   493
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   494
          case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   495
          with eval_ps have "s2=s1" by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   496
          with eval_e conf_a eval_ps conf_s1 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   497
          show ?thesis 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   498
            by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   499
        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
   500
      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
   501
    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
   502
  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
   503
    show "\<forall>a vs invC declC 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
   504
      G,A\<turnstile>{?R a\<leftarrow>\<lfloor>vs\<rfloor>\<^sub>l \<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
   505
             (\<lambda>s. 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
   506
                  invocation_declclass G mode (store 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
   507
                      \<lparr>name=mn, parTs=pTs'\<rparr> \<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
   508
                  invC = invocation_class mode (store s) a statT \<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
   509
                  l = locals (store s)) ;.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   510
             init_lvars G declC \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs \<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
   511
             (\<lambda>s. normal s \<longrightarrow> 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
   512
          Methd declC \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   513
          {set_lvars l .; ?S}" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   514
      (is "\<forall> a vs invC declC l. ?METHD a vs invC declC 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
   515
    proof (intro allI)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   516
      fix a vs invC declC 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
   517
      from mgf_methds [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
   518
      show "?METHD a vs invC declC 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
   519
      proof (rule MGFnD' [THEN conseq12],clarsimp)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   520
        fix s4 s2 s1::state
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   521
        fix s0 v
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   522
        let ?D= "invocation_declclass G mode (store s2) a statT 
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
   523
                    \<lparr>name=mn,parTs=pTs'\<rparr>"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   524
        let ?s3= "init_lvars G ?D \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs s2"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   525
        assume inv_prop: "abrupt ?s3=None 
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
   526
             \<longrightarrow> G\<turnstile>mode\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   527
        assume conf_s2: "s2\<Colon>\<preceq>(G, L)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   528
        assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   529
        assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   530
        assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   531
        assume eval_mthd: "G\<turnstile>?s3 \<midarrow>Methd ?D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   532
        show "G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v
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
   533
                        \<rightarrow> (set_lvars (locals (store s2))) s4"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   534
        proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   535
          obtain D where D: "D=?D" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   536
          obtain s3 where s3: "s3=?s3" by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   537
          obtain s3' where 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   538
            s3': "s3' = check_method_access G accC statT mode 
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
   539
                           \<lparr>name=mn,parTs=pTs'\<rparr> a s3"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   540
            by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   541
          have eq_s3'_s3: "s3'=s3"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   542
          proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   543
            from inv_prop s3 mode
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   544
            have "normal s3 \<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
   545
             G\<turnstile>invmode statM e\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   546
              by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   547
            with eval_ps wt_e statM conf_s2 conf_a [rule_format] 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   548
            have "check_method_access G accC statT (invmode statM e)
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
   549
                      \<lparr>name=mn,parTs=pTs'\<rparr> a s3 = s3"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   550
              by (rule error_free_call_access) (auto simp add: s3 mode wf)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   551
            thus ?thesis 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   552
              by (simp add: s3' mode)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   553
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   554
          with eval_mthd D s3
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   555
          have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   556
            by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   557
          with eval_e eval_ps D _ s3' 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   558
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   559
            by (rule eval_Call) (auto simp add: s3 mode D)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   560
        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
   561
      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
   562
    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
   563
  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
   564
qed
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   565
                  
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
   566
lemma eval_expression_no_jump':
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   567
  assumes eval: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<rightarrow> 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
   568
  and   no_jmp: "abrupt s0 \<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
   569
  and      wt: "\<lparr>prg=G, cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-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
   570
  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
   571
shows "abrupt s1 \<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
   572
using eval no_jmp wt wf
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   573
by - (rule eval_expression_no_jump 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   574
            [where ?Env="\<lparr>prg=G, cls=C,lcl=L\<rparr>",simplified],auto)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
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
   576
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   577
text {* To derive the most general formula for the loop statement, we need to
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   578
come up with a proper loop invariant, which intuitively states that we are 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   579
currently inside the evaluation of the loop. To define such an invariant, we
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   580
unroll the loop in iterated evaluations of the expression and evaluations 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
   581
the loop body. *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   582
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   583
constdefs
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   584
 unroll:: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   585
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   586
 "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   587
                             G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<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
   588
                             G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   589
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   590
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   591
lemma unroll_while:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
  assumes unroll: "(s, t) \<in> (unroll G l e c)\<^sup>*"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   593
  and     eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   594
  and     normal_termination: "normal s'  \<longrightarrow> \<not> the_Bool v"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   595
  and     wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-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
   596
  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
   597
  shows "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   598
using unroll (* normal_s *)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   599
proof (induct rule: converse_rtrancl_induct) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
  show "G\<turnstile>t \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   601
  proof (cases "normal 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
   602
    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
   603
    with eval_e have "s'=t" by 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
   604
    with False show ?thesis by 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
   605
  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
   606
    case True
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   607
    note normal_t = this
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
    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
   609
    proof (cases "normal s'")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   610
      case True
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   611
      with normal_t eval_e normal_termination
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   613
        by (auto intro: eval.Loop)
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
   614
    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
   615
      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
   616
      note abrupt_s' = this
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      from eval_e _ wt wf
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      have no_cont: "abrupt s' \<noteq> Some (Jump (Cont l))"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   619
        by (rule eval_expression_no_jump') (insert normal_t,simp)
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
   620
      have
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   621
        "if the_Bool v 
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
   622
             then (G\<turnstile>s' \<midarrow>c\<rightarrow> s' \<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
   623
                   G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s')
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   624
             else s' = s'"
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
   625
      proof (cases "the_Bool v")
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   626
        case False thus ?thesis by simp
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
   627
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   628
        case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   629
        with abrupt_s' have "G\<turnstile>s' \<midarrow>c\<rightarrow> s'" by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   630
        moreover from abrupt_s' no_cont 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   631
        have no_absorb: "(abupd (absorb (Cont l)) s')=s'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   632
          by (cases s') (simp add: absorb_def split: split_if)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   633
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   634
        from no_absorb abrupt_s'
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   635
        have "G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   636
          by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   637
        ultimately show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   638
          using True by simp
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
   639
      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
   640
      with eval_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
   641
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   642
        using normal_t by (auto intro: eval.Loop)
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
   643
    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
   644
  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
   645
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
   646
  fix s s3
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   647
  assume unroll: "(s,s3) \<in> unroll G l e c"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   648
  assume while: "G\<turnstile>s3 \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   649
  show "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   650
  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
   651
    from unroll obtain v s1 s2 where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   652
      normal_s1: "normal s1" 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
   653
      eval_e: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1" 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
   654
      continue: "the_Bool v" 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
   655
      eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" 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
   656
      s3: "s3=(abupd (absorb (Cont l)) s2)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   657
      by  (unfold unroll_def) fast 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   658
    from eval_e normal_s1 have
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   659
      "normal s"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   660
      by (rule eval_no_abrupt_lemma [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
   661
    with while eval_e continue eval_c s3 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
   662
      by (auto intro!: eval.Loop)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   663
  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
   664
qed
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
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
   666
lemma MGFn_Loop:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   667
  assumes mfg_e: "G,(A::state triple set)\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   668
  and     mfg_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   669
  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
   670
shows "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   671
proof (rule MGFn_free_wt [rule_format],elim exE)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   672
  fix T L C
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   673
  assume wt: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>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
   674
  then obtain eT where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   675
    wt_e: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   676
    by cases 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
   677
  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
   678
  proof (rule MGFn_NormalI)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
    show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>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
   680
              .l\<bullet> While(e) c.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
              {\<lambda>Y s' s. G\<turnstile>s \<midarrow>In1r (l\<bullet> While(e) c)\<succ>\<rightarrow> (Y, s')}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   682
    proof (rule conseq12 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   683
           [where ?P'="(\<lambda> Y s' s. (s,s') \<in> (unroll G l e c)\<^sup>* ) \<and>. G\<turnstile>init\<le>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
   684
             and  ?Q'="((\<lambda> Y s' s. (\<exists> t b. (s,t) \<in> (unroll G l e c)\<^sup>* \<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
   685
                          Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   686
                        \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>"])
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   687
      show  "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>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
   688
                  .l\<bullet> While(e) c.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   689
                 {((\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<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
   690
                                  Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   691
                              \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   692
      proof (rule ax_derivs.Loop)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   693
        from mfg_e
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   694
        show "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n} 
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
   695
                   e-\<succ>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   696
                  {(\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<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
   697
                                     Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   698
                   \<and>. G\<turnstile>init\<le>n}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   699
        proof (rule MGFnD' [THEN conseq12],clarsimp)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   700
          fix s Z s' v
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   701
          assume "(Z, s) \<in> (unroll G l e c)\<^sup>*"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   702
          moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   703
          assume "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   704
          ultimately
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   705
          show "\<exists>t. (Z, t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   706
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   707
        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
   708
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   709
        from mfg_c
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   710
        show "G,A\<turnstile>{Normal (((\<lambda>Y s' s. \<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and>
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
   711
                                       Y = \<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s') 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   712
                          \<and>. G\<turnstile>init\<le>n)\<leftarrow>=True)}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   713
                  .c.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   714
                  {abupd (absorb (Cont 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
   715
                   ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n)}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   716
        proof (rule MGFnD' [THEN conseq12],clarsimp)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   717
          fix Z s' s v t
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   718
          assume unroll: "(Z, t) \<in> (unroll G l e c)\<^sup>*"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   719
          assume eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> Norm s" 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   720
          assume true: "the_Bool v"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   721
          assume eval_c: "G\<turnstile>Norm s \<midarrow>c\<rightarrow> s'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   722
          show "(Z, abupd (absorb (Cont l)) s') \<in> (unroll G l e c)\<^sup>*"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   723
          proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   724
            note unroll
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   725
            also
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   726
            from eval_e true eval_c
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   727
            have "(t,abupd (absorb (Cont l)) s') \<in> unroll G l e c" 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   728
              by (unfold unroll_def) force
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   729
            ultimately show ?thesis ..
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   730
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   731
        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
   732
      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
   733
    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
   734
      show 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   735
        "\<forall>Y s Z.
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   736
         (Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)) Y s Z 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   737
         \<longrightarrow> (\<forall>Y' s'.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   738
               (\<forall>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
   739
                 ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n) Y s Z' 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   740
                 \<longrightarrow> (((\<lambda>Y s' s. \<exists>t b. (s,t) \<in> (unroll G l e c)\<^sup>* 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   741
                                       \<and> Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s') 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   742
                     \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>) Y' s' Z') 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   743
               \<longrightarrow> G\<turnstile>Z \<midarrow>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ>\<rightarrow> (Y', s'))"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   744
      proof (clarsimp)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   745
        fix Y' s' s
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   746
        assume asm:
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   747
          "\<forall>Z'. (Z', Norm s) \<in> (unroll G l e c)\<^sup>* 
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
   748
                 \<longrightarrow> card (nyinitcls G s') \<le> 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
   749
                     (\<exists>v. (\<exists>t. (Z', t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s') \<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
   750
                     (fst s' = None \<longrightarrow> \<not> the_Bool v)) \<and> Y' = \<diamondsuit>"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   751
        show "Y' = \<diamondsuit> \<and> G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   752
        proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   753
          from asm obtain v t where 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   754
            -- {* @{term "Z'"} gets instantiated with @{term "Norm s"} *}  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   755
            unroll: "(Norm s, t) \<in> (unroll G l e c)\<^sup>*" and
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
   756
            eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" 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
   757
            normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v" and
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   758
             Y': "Y' = \<diamondsuit>"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   759
            by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   760
          from unroll eval_e normal_termination wt_e wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   761
          have "G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   762
            by (rule unroll_while)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   763
          with Y' 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   764
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   765
            by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   766
        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
   767
      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
   768
    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
   769
  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
   770
qed
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   772
lemma MGFn_FVar:
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
   773
  fixes A :: "state triple set"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   774
 assumes mgf_init: "G,A\<turnstile>{=:n} \<langle>Init statDeclC\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   775
  and    mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   776
  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
   777
  shows "G,A\<turnstile>{=:n} \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   778
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   779
  note inj_term_simps [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
   780
  fix T L accC' V
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   781
  assume wt: "\<lparr>prg = G, cls = accC', lcl = L\<rparr>\<turnstile>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<Colon>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
   782
  then obtain statC f where
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   783
    wt_e: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" 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
   784
    accfield: "accfield G accC' statC fn = Some (statDeclC,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
   785
    eq_accC: "accC=accC'" 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
   786
    stat: "stat=is_static  f"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   787
    by (cases) (auto simp add: member_is_static_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
   788
  let ?Q="(\<lambda>Y s1 (x,s) . x = None \<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
   789
                (G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s1) \<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
   790
                (\<exists> E. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> 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
   791
                \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   792
  show "G,A\<turnstile>{Normal
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   793
             ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>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
   794
              (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<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
   795
              (\<lambda>s. \<lparr>prg=G,cls=accC',lcl=L\<rparr>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   796
                 \<turnstile> dom (locals (store s)) \<guillemotright> \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V))
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   797
             } {accC,statDeclC,stat}e..fn=\<succ>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   798
             {\<lambda>Y s' s. \<exists>vf. Y = \<lfloor>vf\<rfloor>\<^sub>v \<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
   799
                        G\<turnstile>s \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>vf\<rightarrow> s'}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   800
    (is "G,A\<turnstile>{Normal ?P} {accC,statDeclC,stat}e..fn=\<succ> {?R}")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   801
  proof (rule ax_derivs.FVar [where ?Q="?Q" ])
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   802
    from mgf_init
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   803
    show "G,A\<turnstile>{Normal ?P} .Init statDeclC. {?Q}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   804
    proof (rule MGFnD' [THEN conseq12],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   805
      fix s s'
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   806
      assume conf_s: "Norm s\<Colon>\<preceq>(G, L)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   807
      assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   808
                    \<turnstile> dom (locals s) \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   809
      assume eval_init: "G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s'"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   810
      show "(\<exists>E. \<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals (store s')) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E) \<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
   811
            s'\<Colon>\<preceq>(G, L)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   812
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   813
        from da 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   814
        obtain E where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   815
          "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals s) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   816
          by cases simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   817
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   818
        from eval_init
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   819
        have "dom (locals s) \<subseteq> dom (locals (store s'))"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   820
          by (rule dom_locals_eval_mono [elim_format]) simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   821
        ultimately obtain E' where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   822
          "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals (store s')) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   823
          by (rule da_weakenE)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   824
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   825
        have "s'\<Colon>\<preceq>(G, L)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   826
        proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   827
          have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   828
          proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   829
            from wf wt_e 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   830
            have iscls_statC: "is_class G statC"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   831
              by (auto dest: ty_expr_is_type type_is_class)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   832
            with wf accfield 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   833
            have iscls_statDeclC: "is_class G statDeclC"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   834
              by (auto dest!: accfield_fields dest: fields_declC)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   835
            thus ?thesis by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   836
          qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   837
          obtain I where 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   838
            da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
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
   839
               \<turnstile> dom (locals (store ((Norm s)::state))) \<guillemotright>\<langle>Init statDeclC\<rangle>\<^sub>s\<guillemotright> I"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   840
            by (auto intro: da_Init [simplified] assigned.select_convs)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   841
          from eval_init conf_s wt_init da_init  wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   842
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   843
            by (rule eval_type_soundE)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   844
        qed
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   845
        ultimately show ?thesis by iprover
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
   846
      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
   847
    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
   848
  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
   849
    from mgf_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
   850
    show "G,A\<turnstile>{?Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; ?R}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
    proof (rule MGFnD' [THEN conseq12],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   852
      fix s0 s1 s2 E a
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   853
      let ?fvar = "fvar statDeclC stat fn a s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   854
      assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> 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
   855
      assume eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   856
      assume conf_s1: "s1\<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
   857
      assume da_e: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> 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
   858
      show "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>fst ?fvar\<rightarrow> snd ?fvar"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   860
        obtain v s2' where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   861
          v: "v=fst ?fvar" and s2': "s2'=snd ?fvar"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   862
          by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   863
        obtain s3 where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   864
          s3: "s3= check_field_access G accC' statDeclC fn stat a s2'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   865
          by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   866
        have eq_s3_s2': "s3=s2'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   867
        proof -
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   868
          from eval_e conf_s1 wt_e da_e wf obtain
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   869
            conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   870
            conf_a: "normal s2 \<Longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   871
            by (rule eval_type_soundE) simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   872
          from accfield wt_e eval_init eval_e conf_s2 conf_a _ wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   873
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   874
            by (rule  error_free_field_access 
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
   875
                      [where ?v=v and ?s2'=s2',elim_format])
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   876
               (simp add: s3 v s2' stat)+
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
   877
        qed
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   878
        from eval_init eval_e 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   879
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   880
          apply (rule eval.FVar [where ?s2'=s2'])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   881
          apply  (simp add: s2')
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   882
          apply  (simp add: s3 [symmetric]   eq_s3_s2' eq_accC s2' [symmetric])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   883
          done
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   884
      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
   885
    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
   886
  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
   887
qed
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   888
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   889
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
   890
lemma MGFn_Fin:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   891
  assumes 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
   892
  and     mgf_c1: "G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   893
  and     mgf_c2: "G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   894
  shows "G,(A\<Colon>state triple set)\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   895
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   896
  fix T L accC C 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   897
  assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>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
   898
  then obtain
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   899
    wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" 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
   900
    wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   901
    by cases 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
   902
  let  ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>c1\<rightarrow> s' \<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
   903
               (\<exists> C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   904
               \<and> s\<Colon>\<preceq>(G, L)) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   905
             \<and>. G\<turnstile>init\<le>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
   906
  show "G,A\<turnstile>{Normal
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   907
              ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>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
   908
              (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<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
   909
              (\<lambda>s. \<lparr>prg=G,cls=accC,lcl =L\<rparr>  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   910
                     \<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C))}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   911
             .c1 Finally c2. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   912
             {\<lambda>Y s' s. Y = \<diamondsuit> \<and> G\<turnstile>s \<midarrow>c1 Finally c2\<rightarrow> s'}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   913
    (is "G,A\<turnstile>{Normal ?P} .c1 Finally c2. {?R}")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   914
  proof (rule ax_derivs.Fin [where ?Q="?Q"])
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   915
    from mgf_c1
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   916
    show "G,A\<turnstile>{Normal ?P} .c1. {?Q}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   917
    proof (rule MGFnD' [THEN conseq12],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   918
      fix s0
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   919
      assume "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   920
      thus "\<exists>C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   921
        by cases (auto simp add: inj_term_simps)
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
   922
    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
   923
  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
   924
    from mgf_c2
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
    show "\<forall>abr. G,A\<turnstile>{?Q \<and>. (\<lambda>s. abr = abrupt s) ;. abupd (\<lambda>abr. None)} .c2.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
          {abupd (abrupt_if (abr \<noteq> None) abr) .; ?R}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
    proof (rule MGFnD' [THEN conseq12, THEN allI],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      fix s0 s1 s2 C1
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      assume da_c1:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      assume conf_s0: "Norm s0\<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
   931
      assume eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> 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
   932
      assume eval_c2: "G\<turnstile>abupd (\<lambda>abr. None) s1 \<midarrow>c2\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
      show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
               \<rightarrow> abupd (abrupt_if (\<exists>y. abrupt s1 = Some y) (abrupt s1)) s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   935
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   936
        obtain abr1 str1 where s1: "s1=(abr1,str1)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   937
          by (cases s1)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   938
        with eval_c1 eval_c2 obtain
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   939
          eval_c1': "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (abr1,str1)" and
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   940
          eval_c2': "G\<turnstile>Norm str1 \<midarrow>c2\<rightarrow> s2"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   941
          by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   942
        obtain s3 where 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   943
          s3: "s3 = (if \<exists>err. abr1 = Some (Error err) 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   944
                        then (abr1, str1)
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
   945
                        else abupd (abrupt_if (abr1 \<noteq> None) abr1) s2)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   946
          by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   947
        from eval_c1' conf_s0 wt_c1 _ wf 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   948
        have "error_free (abr1,str1)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   949
          by (rule eval_type_soundE) (insert da_c1,auto)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   950
        with s3 have eq_s3: "s3=abupd (abrupt_if (abr1 \<noteq> None) abr1) s2"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   951
          by (simp add: error_free_def)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   952
        from eval_c1' eval_c2' s3
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   953
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
   954
          by (rule eval.Fin [elim_format]) (simp add: s1 eq_s3)
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
   955
      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
   956
    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
   957
  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
   958
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
   959
      
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   960
lemma Body_no_break:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   961
 assumes eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> 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
   962
   and      eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
   and       jmpOk: "jumpNestingOkS {Ret} c"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the 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
   and        wt_c: "\<lparr>prg=G, cls=C, lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   965
   and        clsD: "class G D=Some d"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   966
   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
   967
  shows "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l)) \<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
   968
              abrupt s2 \<noteq> Some (Jump (Cont 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
   969
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
   970
  fix l show "abrupt s2 \<noteq> Some (Jump (Break l)) \<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
   971
              abrupt s2 \<noteq> Some (Jump (Cont 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
   972
  proof -
26932
c398a3866082 avoid undeclared variables within proofs;
wenzelm
parents: 24783
diff changeset
   973
    fix accC from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
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
   974
      by 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
   975
    from eval_init wf
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   976
    have s1_no_jmp: "\<And> j. abrupt s1 \<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
   977
      by - (rule eval_statement_no_jump [OF _ _ _ wt_init],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
   978
    from eval_c _ wt_c wf
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   979
    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
   980
      apply (rule jumpNestingOk_eval [THEN conjE, elim_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
   981
      using jmpOk s1_no_jmp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   982
      apply 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
   983
      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
   984
  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
   985
qed
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
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
   987
lemma MGFn_Body:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   988
  assumes 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
   989
  and     mgf_init: "G,A\<turnstile>{=:n} \<langle>Init D\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   990
  and     mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   991
  shows  "G,(A\<Colon>state triple set)\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   992
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   993
  fix T L accC 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
   994
  assume wt: "\<lparr>prg=G, cls=accC,lcl=L\<rparr>\<turnstile>\<langle>Body D c\<rangle>\<^sub>e\<Colon>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
   995
  let ?Q="(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init D\<rightarrow> s' \<and> jumpNestingOkS {Ret} c) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   996
          \<and>. G\<turnstile>init\<le>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
   997
  show "G,A\<turnstile>{Normal
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   998
               ((\<lambda>Y' s' s. s' = s \<and> fst s = None) \<and>. G\<turnstile>init\<le>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
   999
                (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<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
  1000
                (\<lambda>s. \<lparr>prg=G,cls=accC,lcl=L\<rparr>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1001
                       \<turnstile> dom (locals (store s)) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> 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
  1002
             Body D c-\<succ> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1003
             {\<lambda>Y s' s. \<exists>v. Y = In1 v \<and> G\<turnstile>s \<midarrow>Body D c-\<succ>v\<rightarrow> s'}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1004
    (is "G,A\<turnstile>{Normal ?P} Body D c-\<succ> {?R}")
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1005
  proof (rule ax_derivs.Body [where ?Q="?Q"])
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1006
    from mgf_init
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1007
    show "G,A\<turnstile>{Normal ?P} .Init D. {?Q}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1008
    proof (rule MGFnD' [THEN conseq12],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1009
      fix s0
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1010
      assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> 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
  1011
      thus "jumpNestingOkS {Ret} c"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1012
        by cases simp
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
  1013
    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
  1014
  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
  1015
    from mgf_c
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1016
    show "G,A\<turnstile>{?Q}.c.{\<lambda>s.. abupd (absorb Ret) .; ?R\<leftarrow>\<lfloor>the (locals s Result)\<rfloor>\<^sub>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
  1017
    proof (rule MGFnD' [THEN conseq12],clarsimp)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1018
      fix s0 s1 s2
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1019
      assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> 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
  1020
      assume eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1021
      assume nestingOk: "jumpNestingOkS {Ret} c"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1022
      show "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1023
              \<rightarrow> abupd (absorb Ret) s2"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1024
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1025
        from wt obtain d where 
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
  1026
          d: "class G D=Some d" 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
  1027
          wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1028
          by cases auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1029
        obtain s3 where 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1030
          s3: "s3= (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
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
  1031
                           fst s2 = Some (Jump (Cont 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
  1032
                       then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1033
                       else s2)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1034
          by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1035
        from eval_init eval_c nestingOk wt_c d wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1036
        have eq_s3_s2: "s3=s2"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1037
          by (rule Body_no_break [elim_format]) (simp add: s3)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1038
        from eval_init eval_c s3
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1039
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1040
          by (rule eval.Body [elim_format]) (simp add: eq_s3_s2)
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
  1041
      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
  1042
    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
  1043
  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
  1044
qed
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
  1045
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
  1046
lemma MGFn_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
  1047
  assumes mgf_methds: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1048
           "\<And> n. \<forall> C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1049
  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
  1050
  shows "\<And> t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1051
proof (induct rule: full_nat_induct)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1052
  fix n 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
  1053
  assume hyp: "\<forall> m. Suc m \<le> n \<longrightarrow> (\<forall> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1054
  show "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1055
  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
  1056
  { 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1057
    fix v e c es
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1058
    have "G,A\<turnstile>{=:n} \<langle>v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}" 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
  1059
      "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" 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
  1060
      "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" 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
  1061
      "G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
18459
2b102759160d mutual induct with *.inducts;
wenzelm
parents: 18249
diff changeset
  1062
    proof (induct rule: var_expr_stmt.inducts)
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
  1063
      case (LVar v)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1064
      show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1065
        apply (rule MGFn_NormalI)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1066
        apply (rule ax_derivs.LVar [THEN conseq1])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1067
        apply (clarsimp)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1068
        apply (rule eval.LVar)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1069
        done
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1070
    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
  1071
      case (FVar accC statDeclC stat e fn)
23366
a1e61b5c000f tuned proofs: avoid implicit prems;
wenzelm
parents: 21669
diff changeset
  1072
      from MGFn_Init [OF hyp] and `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}` and wf
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
  1073
      show ?case
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1074
        by (rule MGFn_FVar)
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
  1075
    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
  1076
      case (AVar e1 e2)
23366
a1e61b5c000f tuned proofs: avoid implicit prems;
wenzelm
parents: 21669
diff changeset
  1077
      note mgf_e1 = `G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
a1e61b5c000f tuned proofs: avoid implicit prems;
wenzelm
parents: 21669
diff changeset
  1078
      note mgf_e2 = `G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
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
  1079
      show "G,A\<turnstile>{=:n} \<langle>e1.[e2]\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1080
        apply (rule MGFn_NormalI)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1081
        apply (rule ax_derivs.AVar)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1082
        apply  (rule MGFnD [OF mgf_e1, THEN ax_NormalD])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1083
        apply (rule allI)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1084
        apply (rule MGFnD' [OF mgf_e2, THEN conseq12])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1085
        apply (fastsimp intro: eval.AVar)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1086
        done
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1087
    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
  1088
      case (InsInitV c v)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1089
      show ?case
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1090
        by (rule MGFn_NormalI) (rule ax_derivs.InsInitV)
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
  1091
    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
  1092
      case (NewC C)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1093
      show ?case
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1094
        apply (rule MGFn_NormalI)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1095
        apply (rule ax_derivs.NewC)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1096
        apply (rule MGFn_InitD [OF hyp, THEN conseq2])
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1097
        apply (fastsimp intro: eval.NewC)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31945
diff changeset
  1098
        done
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
  1099
    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