src/HOL/Bali/AxCompl.thy
author schirmer
Mon, 28 Jan 2002 17:00:19 +0100
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     1
(*  Title:      isabelle/Bali/AxCompl.thy
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
    Copyright   1999 Technische Universitaet Muenchen
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
header {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
Completeness proof for Axiomatic semantics of Java expressions and statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
theory AxCompl = AxSem:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\item proof structured by Most General Formulas (-> Thomas Kleymann)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
section "set of not yet initialzed classes"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
 "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
lemmas finite_nyinitcls [simp] =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
lemma nyinitcls_set_locals_cong [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
  "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
lemma card_nyinitcls_abrupt_congE [elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
        "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
lemma nyinitcls_new_xcpt_var [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
apply (induct_tac "s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
lemma nyinitcls_init_lvars [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
  "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
apply (induct_tac "s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
apply (simp (no_asm) add: init_lvars_def2 split add: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
lemma card_Suc_lemma: "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
apply (rotate_tac 1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
lemma nyinitcls_le_SucD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
"\<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
    86
  card (nyinitcls G (x,init_class_obj G C s)) \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
apply (subgoal_tac 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
        "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
apply  (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
apply   (auto dest!: not_initedD elim!: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
              simp add: nyinitcls_def inited_def split add: split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
ML {* bind_thm("inited_gext'",permute_prems 0 1 (thm "inited_gext")) *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
apply (unfold nyinitcls_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
apply (force dest!: inited_gext')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
lemma card_nyinitcls_gext: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
  "\<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
   105
apply (rule le_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
apply  (rule card_mono)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
apply   (rule finite_nyinitcls)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
apply  (erule nyinitcls_gext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
apply assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
section "init-le"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"            ("_\<turnstile>init\<le>_"  [51,51] 50)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
 "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
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
   120
apply (unfold init_le_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
lemma All_init_leD: "\<forall>n::nat. G,A\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply (rule card_nyinitcls_bound)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
section "Most General Triples and Formulas"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
  remember_init_state :: "state assn"                ("\<doteq>")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
  "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
apply (unfold remember_init_state_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
  MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
defs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
  MGF_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
  "{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
   153
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
  MGFn_def:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
  "{=: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
   156
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
lemma MGF_valid: "G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
apply (force dest!: evaln_eval simp add: ax_valids_def triple_valid_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
lemma MGF_res_eq_lemma [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
  "(\<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
   165
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
lemma MGFn_def2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
"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
   170
                    t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply (unfold MGFn_def MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
lemma MGF_MGFn_iff: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
apply  (erule_tac [2] All_init_leD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
lemma MGFnD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
 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
   186
 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
   187
apply (unfold init_le_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
apply (simp (no_asm_use) add: MGFn_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
apply (erule (1) eval_gext [THEN card_nyinitcls_gext])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
  G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
apply  (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
apply (rule ax_derivs.Abrupt [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
apply (clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
lemma MGFNormalD: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
lemma MGFn_NormalI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
"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
   213
 {\<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
   214
apply (simp (no_asm_use) add: MGFn_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
apply  (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
apply (rule ax_derivs.Abrupt [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
apply (clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
lemma MGFn_free_wt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
  "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
    \<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
   \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
apply (rule MGFn_NormalI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
apply (rule ax_free_wt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
section "main lemmas"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
declare fun_upd_apply [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
declare splitI2 [rule del] (*prevents ugly renaming of state variables*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
ML_setup {* 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
Delsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
*} (*prevents modifying rhs of MGF*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
val eval_css = (claset() delrules [thm "eval.Abrupt"] addSIs (thms "eval.intros") 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
                delrules[thm "eval.Expr", thm "eval.Init", thm "eval.Try"] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
                addIs   [thm "eval.Expr", thm "eval.Init"]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
                addSEs[thm "eval.Try"] delrules[equalityCE],
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
                simpset() addsimps [split_paired_all,Let_def]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
 addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
val eval_Force_tac = force_tac eval_css;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
val wt_prepare_tac = EVERY'[
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
    rtac (thm "MGFn_free_wt"),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
    clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
val compl_prepare_tac = EVERY'[rtac (thm "MGFn_NormalI"), Simp_tac]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
val forw_hyp_tac = EVERY'[etac (thm "MGFnD'" RS thm "conseq12"), Clarsimp_tac]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
val forw_hyp_eval_Force_tac = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
         EVERY'[TRY o rtac allI, forw_hyp_tac, eval_Force_tac]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
lemma MGFn_Init: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}) \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
  G,(A::state triple set)\<turnstile>{=:n} In1r (Init C)\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
apply (tactic "wt_prepare_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
(* requires is_class G C two times for nyinitcls *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
apply (tactic "compl_prepare_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
apply (rule_tac C = "initd C" in ax_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
apply  (rule ax_derivs.Done [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
apply  (clarsimp intro!: init_done)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
apply (rule_tac y = n in nat.exhaust, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
apply  (rule ax_impossible [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
apply  (force dest!: nyinitcls_emptyD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
apply (drule_tac x = "nat" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
apply (rule_tac Q = " (\<lambda>Y s' (x,s) . G\<turnstile> (x,init_class_obj G C s) \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s' \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>nat" in ax_derivs.Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
apply   simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
apply  (rule_tac P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>nat) " in conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
apply   (force elim!: nyinitcls_le_SucD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
apply  (simp split add: split_if, rule conjI, clarify)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
apply   (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
apply  clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
apply  (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
apply  (erule MGFnD' [THEN conseq12])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
apply  (tactic "force_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
apply (erule MGFnD' [THEN conseq12])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
apply (tactic {* pair_tac "sa" 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
apply (tactic"clarsimp_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
apply (rule eval_Init, force+)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
lemma MGFn_Call: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
"\<lbrakk>\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>};  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
  G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In3 ps\<succ> {G\<rightarrow>}\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
  G,A\<turnstile>{=:n} In1l ({statT,mode}e\<cdot>mn({pTs'}ps))\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
apply (tactic "wt_prepare_tac 1") (* required for equating mode = invmode m e *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
apply (tactic "compl_prepare_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
apply (rule_tac R = "\<lambda>a'. (\<lambda>Y (x2,s2) (x,s) . x = None \<and> (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a'\<rightarrow> s1 \<and> Y = In3 pvs \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2))) \<and>. G\<turnstile>init\<le>n" in ax_derivs.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
apply  (erule MGFnD [THEN ax_NormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
apply  (erule_tac V = "All ?P" in thin_rl, tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
apply (drule spec, drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
apply (erule MGFnD' [THEN conseq12])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
apply (tactic "clarsimp_tac eval_css 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
apply (erule (1) eval_Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
apply   (rule HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
apply  (simp (no_asm_simp))+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
lemma MGF_altern: "G,A\<turnstile>{Normal (\<doteq> \<and>. p)} t\<succ> {G\<rightarrow>} =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
 G,A\<turnstile>{Normal ((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z) \<and>. p)} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
  t\<succ> {\<lambda>Y s Z. (Y,s) = Z}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
apply (auto del: conjI elim!: conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
apply  (fast dest: unique_eval)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
apply (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
apply (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
apply (drule split_paired_All [THEN subst])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
apply (clarsimp elim!: state_not_single)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
lemma MGFn_Loop: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
"\<lbrakk>G,(A::state triple set)\<turnstile>{=:n} In1l expr\<succ> {G\<rightarrow>};G,A\<turnstile>{=:n} In1r stmnt\<succ> {G\<rightarrow>} \<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
\<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
  G,A\<turnstile>{=:n} In1r (l\<bullet> While(expr) stmnt)\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
apply (rule MGFn_NormalI, simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
apply (rule_tac p2 = "\<lambda>s. card (nyinitcls G s) \<le> n" in 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
          MGF_altern [unfolded MGF_def, THEN iffD2, THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
apply (rule_tac P' = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
"((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>In1r (l\<bullet>  While(expr) stmnt) \<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
  \<and>. (\<lambda>s. card (nyinitcls G s) \<le> n))" in conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
apply  (tactic "smp_tac 1 1", erule_tac V = "All ?P" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
apply  (rule_tac [2] P' = " (\<lambda>b s (Y',s') . (\<exists>s0. G\<turnstile>s0 \<midarrow>In1l expr\<succ>\<rightarrow> (b,s)) \<and> (if normal s \<and> the_Bool (the_In1 b) then (\<forall>s'' w s0. G\<turnstile>s \<midarrow>stmnt\<rightarrow> s'' \<and> G\<turnstile>(abupd (absorb (Cont l)) s'') \<midarrow>In1r (l\<bullet> While(expr) stmnt) \<succ>\<rightarrow> (w,s0) \<longrightarrow> (w,s0) = (Y',s')) else (\<diamondsuit>,s) = (Y',s'))) \<and>. G\<turnstile>init\<le>n" in polymorphic_Loop)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
apply   (force dest!: eval.Loop split add: split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
apply  (erule MGFnD' [THEN conseq12])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
apply  (erule_tac V = "card (nyinitcls G s') \<le> n" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
apply  (tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
apply (erule MGFnD' [THEN conseq12] , clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
apply (rule conjI, erule exI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
apply (tactic "clarsimp_tac eval_css 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
apply (case_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
apply  (clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
apply (clarsimp split add: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
apply (rule conjI, (tactic {* force_tac (claset() addSDs [thm "eval.Loop"],
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
  simpset() addsimps [split_paired_all] addsimprocs [eval_stmt_proc]) 1*})+)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
lemma MGFn_lemma [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
 "\<forall>n C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>} \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
  \<forall>t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
apply (rule full_nat_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
apply (drule_tac x = n in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
apply (drule_tac psi = "All ?P" in asm_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
apply (subgoal_tac "\<forall>v e c es. G,A\<turnstile>{=:n} In2 v\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1r c\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In3 es\<succ> {G\<rightarrow>}")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
apply  (tactic "Clarify_tac 2")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
apply  (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
apply    (induct_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
apply     fast+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
apply (rule var_expr_stmt.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
(* 28 subgoals *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
prefer 14 apply fast (* Methd *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
prefer 13 apply (erule (2) MGFn_Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
apply (erule_tac [24] MGFn_Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
prefer 19 apply (erule (1) MGFn_Loop)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
apply (tactic "ALLGOALS compl_prepare_tac")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
apply (rule ax_derivs.FVar)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
apply  (erule MGFn_InitD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
apply (tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
apply (rule ax_derivs.AVar)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
apply  (erule MGFnD [THEN ax_NormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
apply (tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
apply (rule ax_derivs.NewC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
apply (erule MGFn_InitD [THEN conseq2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
apply (tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
apply (rule_tac Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty ty) \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.NewA)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
apply  (simp add: init_comp_ty_def split add: split_if)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
apply   (rule conjI, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
apply   (erule MGFn_InitD [THEN conseq2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
apply   (tactic "clarsimp_tac eval_css 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
apply  clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
apply  (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
apply (tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast],tactic"eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
apply (rule ax_derivs.Ass)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
apply  (erule MGFnD [THEN ax_NormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
apply (tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
apply (rule ax_derivs.Cond)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
apply  (erule MGFnD [THEN ax_NormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
apply  (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
apply  (tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
apply (case_tac "b")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
apply  (simp, tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
apply (simp, tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init pid_field_type\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Body)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
 apply (erule MGFn_InitD [THEN conseq2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
 apply (tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
apply (tactic "forw_hyp_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
apply (erule (1) eval.Body)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
apply (tactic "clarsimp_tac eval_css 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
apply (rule ax_derivs.Comp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
apply  (erule MGFnD [THEN ax_NormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
apply (tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
apply (rule ax_derivs.If)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
apply  (erule MGFnD [THEN ax_NormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
apply  (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
apply  (tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
apply (case_tac "b")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
apply  (simp, tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
apply (simp, tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
apply (rule ax_derivs.Do [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
apply (tactic {* force_tac (eval_css addsimps2 [thm "abupd_def2"]) 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
apply (tactic "clarsimp_tac eval_css 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>In1r stmt1\<succ>\<rightarrow> (Y',s'') \<and> G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.Try)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
apply   (tactic "eval_Force_tac 3")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
apply  (tactic "forw_hyp_eval_Force_tac 2")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
apply (erule MGFnD [THEN ax_NormalD, THEN conseq2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
apply (tactic "clarsimp_tac eval_css 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
apply  (tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
apply (tactic "forw_hyp_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
apply (tactic {* pair_tac "sb" 1 *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
apply (drule (1) eval.Fin)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
apply (rule ax_derivs.Cons)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
apply  (erule MGFnD [THEN ax_NormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
apply (tactic "forw_hyp_eval_Force_tac 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
lemma MGF_asm: "\<forall>C sig. is_methd G C sig \<longrightarrow> G,A\<turnstile>{\<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>} \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
  G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
apply (simp (no_asm_use) add: MGF_MGFn_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
apply (rule MGFn_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
apply (intro strip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
apply (rule MGFn_free_wt)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
apply (force dest: wt_Methd_is_methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
declare splitI2 [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
ML_setup {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
Addsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
section "nested version"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
lemma nesting_lemma' [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
  !!A pn. !b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
  !!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t};  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
          finite U; uA = mgf_call`U |] ==>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
  !A. A <= uA --> n <= card uA --> card A = card uA - n --> (!t. P A {mgf t})"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
  assume ax_derivs_asm:    "!!A ts. ts <= A ==> P A ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
  assume MGF_nested_Methd: "!!A pn. !b:bdy pn. P (insert (mgf_call pn) A) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
                                                  {mgf b} ==> P A {mgf_call pn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
  assume MGF_asm:          "!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
  assume "finite U" "uA = mgf_call`U"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
    apply -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
    apply (induct_tac "n")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
    apply  (tactic "ALLGOALS Clarsimp_tac")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
    apply  (tactic "dtac (permute_prems 0 1 card_seteq) 1")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
    apply    simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
    apply   (erule finite_imageI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
    apply  (simp add: MGF_asm ax_derivs_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
    apply (rule MGF_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
    apply (rule ballI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
    apply (case_tac "mgf_call pn : A")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
    apply  (fast intro: ax_derivs_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
    apply (rule MGF_nested_Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
    apply (rule ballI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
    apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] impE, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
           erule_tac [4] spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
    apply   fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
    apply  (erule Suc_leD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
    apply (drule finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
    apply (erule finite_imageI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
    apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
    apply arith
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
  done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
lemma nesting_lemma [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
  !!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
          !!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
          finite U |] ==> P {} {mgf t}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
  assume 2: "!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
  assume 3: "!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
  assume "!!A ts. ts <= A ==> P A ts" "finite U"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
  then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
    apply -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
    apply (rule_tac mgf = "mgf" in nesting_lemma')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
    apply (erule_tac [2] 2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
    apply (rule_tac [2] 3)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
    apply (rule_tac [6] le_refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
    apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
  done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
lemma MGF_nested_Methd: "\<lbrakk>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
  G,insert ({Normal \<doteq>} In1l (Methd  C sig) \<succ>{G\<rightarrow>}) A\<turnstile>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
            {Normal \<doteq>} In1l (body G C sig) \<succ>{G\<rightarrow>}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
 \<rbrakk> \<Longrightarrow>  G,A\<turnstile>{Normal \<doteq>} In1l (Methd  C sig) \<succ>{G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
apply (rule ax_MethdN)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
apply (erule MethdI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
lemma MGF_deriv: "ws_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
apply (rule MGFNormalI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
                bdy = "\<lambda> (C,sig) .{In1l (body G C sig) }" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
                f = "\<lambda> (C,sig) . In1l (Methd C sig) " in nesting_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
apply    (erule ax_derivs.asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
apply   (clarsimp simp add: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
apply   (erule MGF_nested_Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
apply  (erule_tac [2] finite_is_methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
apply (rule MGF_asm [THEN MGFNormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
apply (rule MGFNormalI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
section "simultaneous version"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
  G,A\<union> (\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) ` ms  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
     |\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (body G C sig)\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
  G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) ` ms"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
apply (rule ax_derivs.Methd [unfolded mtriples_def])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
apply (erule ax_finite_pointwise)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
apply  (rule ax_derivs.asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
apply  fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
apply (rule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
apply  (erule (1) ax_methods_spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
apply (erule eval_Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
lemma MGF_simult_Methd: "ws_prog G \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
   G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
   ` Collect (split (is_methd G)) "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
apply (frule finite_is_methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
apply (rule MGF_simult_Methd_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
apply  assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
apply (erule ax_finite_pointwise)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
prefer 2
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
apply  (rule ax_derivs.asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
apply  blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
apply (rule MGF_asm [THEN MGFNormalD])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
apply (rule MGFNormalI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
lemma MGF_deriv: "ws_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
apply (rule MGF_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
apply (intro strip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
apply (rule MGFNormalI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
apply (rule ax_derivs.weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
apply  (erule MGF_simult_Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
section "corollaries"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
lemma MGF_complete: "G,{}\<Turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
  G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
apply (rule ax_no_hazard)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
apply (unfold MGF_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
apply (simp (no_asm_use) add: ax_valids_def triple_valid_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
apply (fast dest!: eval_evaln)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
theorem ax_complete: "ws_prog G \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
  G,{}\<Turnstile>{P::state assn} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
apply (erule MGF_complete)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
apply (erule MGF_deriv)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
end