theory VCOpt = SALOverflowFWInst_deep:

text {* We define an optimizer for verfication condtions and prove that
the transformations it does preserve validity. *}

consts isconstant ::"expr \<Rightarrow> bool"

primrec
"isconstant (V n) = False"
"isconstant (Lv v) = False"
"isconstant (C tv) = True"
"isconstant Pc = False"
"isconstant Rp = False"
"isconstant Tm = False"
"isconstant (Add ex1 ex2) = (isconstant ex1 \<and> isconstant ex2)"
"isconstant (Minus ex1 ex2) = (isconstant ex1 \<and> isconstant ex2)"
"isconstant (Mult ex1 ex2) = (isconstant ex1 \<and> isconstant ex2)"
"isconstant (Deref ex) = False"
"isconstant (Ifeq ex1 ex2 ex3 ex4) = (isconstant ex1 \<and> isconstant ex2 \<and> isconstant ex3 \<and> isconstant ex4)"
"isconstant (Old ex) = isconstant ex"

consts isconstantF ::"SALform \<Rightarrow> bool"

recdef isconstantF "measure sizeF" 
"isconstantF T = True"
"isconstantF F = True"
"isconstantF (And []) = True"
"isconstantF (And (f#fs)) = (isconstantF f \<and> isconstantF (And fs))"
"isconstantF (Imp f1 f2) = (isconstantF f1 \<and> isconstantF f2)"
"isconstantF (Neg f) = (isconstantF f)"
"isconstantF (Eq ex1 ex2) = (isconstant ex1 \<and> isconstant ex2)"
"isconstantF (Leq ex1 ex2) = (isconstant ex1 \<and> isconstant ex2)"
"isconstantF (Less ex1 ex2) = (isconstant ex1 \<and> isconstant ex2)"
"isconstantF (Ty ex vt) = (isconstant ex)"
"isconstantF (Forall n f) = False" 
"isconstantF (Yields ex vs) = isconstant ex"

consts flattenAnd::"SALform \<Rightarrow> SALform list"
consts flattenAndL::"SALform list \<Rightarrow> SALform list"

primrec 
"flattenAndL [] = []"
"flattenAndL (f#fs) = (flattenAnd f)@(flattenAndL fs)"
"flattenAnd T = []"
"flattenAnd F = [F]"
"flattenAnd (And fs) = (flattenAndL fs)"
"flattenAnd (Imp f1 f2) = [Imp f1 f2]"
"flattenAnd (Neg f) = [Neg f]" 
"flattenAnd (Eq ex1 ex2) = [Eq ex1 ex2]"
"flattenAnd (Leq ex1 ex2) = [Leq ex1 ex2]"
"flattenAnd (Less ex1 ex2) = [Less ex1 ex2]"
"flattenAnd (Ty ex vt) = [Ty ex vt]"
"flattenAnd (Forall n f) = [Forall n f]"
"flattenAnd (Yields ex L) = [Yields ex L]"

constdefs "I0"::"nat \<Rightarrow> tval"
"I0 \<equiv> \<lambda> x. ILLEGAL"

consts vcopt::"SALform list \<Rightarrow> SALform \<Rightarrow> SALform"
       vcoptL::"SALform list \<Rightarrow>  SALform list \<Rightarrow> SALform list"

primrec
"vcoptL G [] = []"

"vcoptL G (f#fs) = (vcopt G f)#(vcoptL G fs)"

"vcopt G T = T"

"vcopt G F = F"

"vcopt G (And fs) = (case (And fs mem G) 
                     of True \<Rightarrow> T
                     | False \<Rightarrow> (let fs2 = (delL T (flattenAndL (vcoptL G fs)))
                                 in (case fs2
                                     of [] \<Rightarrow> T
                                     | (f2'#fs2') \<Rightarrow> (case (F mem fs2)
                                                      of True \<Rightarrow> F
                                                      | False \<Rightarrow> And fs2))))"

"vcopt G (Imp f1 f2) = (case (Imp f1 f2 mem G)
                        of True \<Rightarrow> T
                        | False \<Rightarrow> (let f1' = vcopt G f1;
                                        G' = G @ (flattenAnd f1');
                                        f2' = vcopt G' f2 
                                    in (case (f1' = T)
                                        of True \<Rightarrow> f2'
                                        | False \<Rightarrow> 
                                       (case (f1' = F)
                                        of True \<Rightarrow> T
                                        | False \<Rightarrow>
                                       (case (f2' = T) 
                                        of True \<Rightarrow> T
                                        | False \<Rightarrow> Imp f1' f2')))))"

"vcopt G (Neg f) = (let f' = vcopt G f 
                    in (case (f' = T) 
                        of True \<Rightarrow> F
                        | False \<Rightarrow> (case (f' = F)
                                    of True \<Rightarrow> T
                                    | False \<Rightarrow> Neg f')))"

"vcopt G (Eq ex1 ex2) = (case (Eq ex1 ex2 mem G)
                         of True \<Rightarrow> T
                         | False \<Rightarrow>
                          (case (isconstant ex1 & isconstant ex2)
                           of True \<Rightarrow> (case (eval I0 initialState ex1 = (eval I0 initialState ex2))
                                       of True \<Rightarrow> T
                                       | False \<Rightarrow> F)
                           |  False \<Rightarrow> Eq ex1 ex2))"

"vcopt G (Leq ex1 ex2) = (case (Leq ex1 ex2 mem G)
                         of True \<Rightarrow> T
                         | False \<Rightarrow>
                          (case (isconstant ex1 & isconstant ex2)
                           of True \<Rightarrow> (case (nv (eval I0 initialState ex1) \<le> nv (eval I0 initialState ex2))
                                       of True \<Rightarrow> T
                                       | False \<Rightarrow> F)
                           | False \<Rightarrow> Leq ex1 ex2))"

"vcopt G (Less ex1 ex2) = (case (Less ex1 ex2 mem G)
                         of True \<Rightarrow> T
                         | False \<Rightarrow>
                          (case (isconstant ex1 & isconstant ex2)
                           of True \<Rightarrow> (case (nv (eval I0 initialState ex1) < nv (eval I0 initialState ex2))
                                       of True \<Rightarrow> T
                                       | False \<Rightarrow> F)
                          | False \<Rightarrow> Less ex1 ex2))"


"vcopt G (Ty ex vt) = (case (Ty ex vt mem G) 
                       of True \<Rightarrow> T
                       | False \<Rightarrow> (case (isconstant ex)
                                   of True \<Rightarrow> (case (eval I0 initialState ex)
                                               of ILLEGAL \<Rightarrow> F
                                               | NAT n \<Rightarrow> (if vt = Nat then T else F)
                                               | POS p \<Rightarrow> (if vt = Pos then T else F))
                                   | False \<Rightarrow> Ty ex vt))"
"vcopt G (Forall v f) = (case (Forall v f mem G) 
                         of True \<Rightarrow> T
                         | False \<Rightarrow> Forall v f)"
"vcopt G (Yields ex vs) = Yields ex vs"


subsection {* Soundness of the optimizer *}

lemma delT_And_validF:
"(validF I s (And (delL T fs))) = (validF I s (And fs))"
(*<*)
apply (induct fs)
apply (simp add: delL_def)+
(*>*)
done

lemma delT_validFs:
"(validFs I s (delL T fs)) = (validFs I s fs)"
(*<*)
apply (induct fs)
apply (simp add: delL_def)+
(*>*)
done


lemma validF_And_split:
"(validF I s (And (fs1 @ fs2))) = (validF I s (And fs1) \<and> validF I s (And fs2))"
(*<*)
apply (induct fs1)
apply simp+
(*>*)
done

lemma validFs_split:
"(validFs I s (fs1 @ fs2)) = (validFs I s fs1 \<and> validFs I s fs2)"
(*<*)
apply (induct fs1)
apply simp+
(*>*)
done

lemma flattenAnd_validF:
"(validF I s (And (flattenAnd f))) = (validF I s f)" 
(*<*)
apply (induct f)
apply simp+
thm validFs_split
apply (simp add: validFs_split)
(*>*)
done

lemma flattenAnd_validFs:
"(validFs I s (flattenAnd f)) = (validF I s f)" 
(*<*)
apply (induct f)
apply simp+
apply (simp add: validFs_split)
(*>*)
done

lemma flattenAndL_validF:
"validF I s (And (flattenAndL fs)) = validF I s (And fs)"
(*<*)
apply (induct fs)
apply simp+
apply (simp add: validFs_split flattenAnd_validF flattenAnd_validFs)
(*>*)
done

lemma flattenAndL_validFs:
"validFs I s (flattenAndL fs) = validFs I s fs"
(*<*)
apply (induct fs)
apply simp+
apply (simp add: validFs_split flattenAnd_validF flattenAnd_validFs)
(*>*)
done

lemma delL_split:
"delL a (l1 @ l2) = (delL a l1) @ (delL a l2)"
(*<*)
apply (induct l1)
apply (simp add: delL_def)+
(*>*)
done

lemma F_And:
"F \<in> set fs \<Longrightarrow> \<not> (validF I s (And fs))"
(*<*)
apply (induct fs)
apply simp+
apply (case_tac "form = F")
apply simp
apply (drule_tac s="F" in not_sym)
apply simp
(*>*)
done

lemma F_invalid:
"F \<in> set fs \<Longrightarrow> \<not> (validFs I s fs)"
(*<*)
apply (induct fs)
apply simp+
apply (erule disjE)
apply simp
apply simp
(*>*)
done

lemma vcoptL_src:
"\<And> x y. (x \<in> (set (vcoptL G fs))) \<Longrightarrow> (\<exists> y \<in> (set fs). x = (vcopt G y))"
(*<*)
apply (induct fs)
apply simp+
apply (erule disjE)
apply simp
apply simp
(*>*)
done

lemma not_And_validF:
"\<not> (validF I s (And fs)) \<Longrightarrow> (\<exists> f\<in> set fs. \<not> (validF I s f))"
(*<*)
apply (induct fs)
apply simp+
(*>*)
done

lemma And_validF_all:
"validF I s (And fs) = (\<forall> f\<in> set fs. validF I s f)"
(*<*)
apply (induct fs)
apply simp+
(*>*)
done

lemma isconstant_eval:
"\<And> s s'. isconstant ex \<Longrightarrow> eval I s ex = eval I' s' ex"
(*<*)
apply (induct ex)
apply simp+
--{* Add *}
apply atomize
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="s'" in allE)
apply (simp add: split_paired_all)
--{* Minus *}
apply atomize
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="s'" in allE)
apply (simp add: split_paired_all)
--{* Mult *}
apply atomize
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="s'" in allE)
apply (simp add: split_paired_all)
--{* Deref *}
apply atomize
apply (erule_tac x="s" in allE)
apply (erule_tac x="s'" in allE)
apply (simp add: split_paired_all)
--{* Ifeq *}
apply atomize
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="s'" in allE)
apply (simp add: split_paired_all)
apply (case_tac "(eval I' ((ab,bb),ac,bc) expr1) = (eval I' ((ab,bb),ac,bc) expr2)")
apply simp
apply simp
--{* Old *}
apply (simp add: Let_def split_def)
(*>*)
done

lemma isconstant_validF:
"\<And> f. isconstantF f \<Longrightarrow> (validF I s f) = (validF I' s' f)"
(*<*)
apply (subgoal_tac "\<exists> k. k = sizeF f")
 prefer 2
 apply (simp (no_asm))
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch2)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)+
apply (simp only:)
apply (erule_tac V="n = sizeF f" in thin_rl)
apply (case_tac "f")
--{* T *}
apply (simp add: valid_def validF_validFs.simps Let_def)
--{* F *}
apply (simp add: valid_def validF_validFs.simps Let_def)
--{* And *}
apply (case_tac "list")
apply (simp add: valid_def validF_validFs.simps Let_def)

apply (simp (no_asm_simp) add: valid_def validF_validFs.simps Let_def)
apply (subgoal_tac "(validF I s a) = (validF I' s' a)")
 prefer 2
 apply (erule_tac x="sizeF a" in allE)
 apply simp 

apply (subgoal_tac "(validF I s (And lista)) = (validF I' s' (And lista))")
 prefer 2
 apply (erule_tac x="sizeF (And lista)" in allE)
 apply simp
 apply (erule_tac x="And lista" in allE)
 apply simp

apply simp

--{* Imp form1 form2 *}
apply (simp add: valid_def validF_validFs.simps Let_def)

apply (subgoal_tac "(validF I s form1) = (validF I' s' form1)")
 prefer 2
 apply (erule_tac x="sizeF form1" in allE)
 apply simp

apply (subgoal_tac "(validF I s form2) = (validF I' s' form2)")
 prefer 2
 apply (erule_tac x="sizeF form2" in allE)
 apply simp

apply simp
--{* Neg form *}

apply (simp add: valid_def validF_validFs.simps Let_def)

apply (subgoal_tac "(validF I s form) = (validF I' s' form)")
 prefer 2
 apply (erule_tac x="sizeF form" in allE)
 apply simp

apply simp
--{* Eq expr1 expr2 *}
apply (simp add: valid_def validF_validFs.simps Let_def)
apply (subgoal_tac "(eval I s expr1) = (eval I' s' expr1)")
 prefer 2
 apply (simp only: isconstant_eval)
apply (subgoal_tac "(eval I s expr2) = (eval I' s' expr2)")
 prefer 2
 apply (simp only: isconstant_eval)
apply simp
--{* Leq expr1 expr2 *}
apply (simp  add: valid_def validF_validFs.simps Let_def)
apply (subgoal_tac "(eval I s expr1) = (eval I' s' expr1)")
 prefer 2
 apply (simp only: isconstant_eval)
apply (subgoal_tac "(eval I s expr2) = (eval I' s' expr2)")
 prefer 2
 apply (simp only: isconstant_eval)
apply simp
--{* Less expr1 expr2 *}
apply (simp  add: valid_def validF_validFs.simps Let_def)
apply (subgoal_tac "(eval I s expr1) = (eval I' s' expr1)")
 prefer 2
 apply (simp only: isconstant_eval)
apply (subgoal_tac "(eval I s expr2) = (eval I' s' expr2)")
 prefer 2
 apply (simp only: isconstant_eval)
apply simp
--{* Ty expr vtype *}
apply (simp  add: valid_def validF_validFs.simps Let_def)
apply (subgoal_tac "(eval I s expr) = (eval I' s' expr)")
 prefer 2
 apply (simp only: isconstant_eval)
apply simp
--{* Forall nat vtype *}
apply (simp  add: valid_def validF_validFs.simps Let_def)
--{* Yields *}
apply simp
apply (subgoal_tac "(eval I s expr) = (eval I' s' expr)")
 prefer 2
 apply (simp only: isconstant_eval)
apply simp
(*>*)
done

declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
simpset_ref() := simpset() delloop "split_all_tac";
claset_ref () := claset () delSWrapper "split_all_tac"
*}


lemma vcopt_sound:
"\<And> f G (I::var \<Rightarrow> tval). (\<forall> f' \<in> set G. I,s \<Turnstile> f') \<Longrightarrow> (I,s \<Turnstile> vcopt G f) = (I,s \<Turnstile> f)"
(*<*)
apply (subgoal_tac "\<exists> k. k = sizeF f")
 prefer 2
 apply (simp (no_asm))
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch4)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)+
apply (case_tac "f")
--{* T *}
apply (simp add: vcopt_vcoptL.simps validF_validFs.simps)
--{* F *}
apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps)
--{* And list *}
apply (simp add: vcopt_vcoptL.simps  validF_validFs.simps)
apply (case_tac "And list mem G")
apply (simp add: set_mem_eq)
apply (erule_tac x="And list" in ballE)
apply simp
apply simp

apply (simp add: Let_def fst_conv snd_conv split_def)
apply (case_tac "list")
apply (simp add: delL_def)

apply simp
apply (subgoal_tac "validF I s (vcopt G a) = validF I s a")
 prefer 2
 apply (erule_tac x="sizeF a" in allE)
 apply (subgoal_tac "(sizeF a) < (Suc (Suc (((sizeF a) + (sizeFs lista)) + (length lista))))")
  prefer 2
  apply (simp (no_asm))
 apply (drule mp, assumption)
 apply (erule_tac x="G" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="a" in allE)
 apply (simp add: split_paired_all)
apply (subgoal_tac "validF I s (vcopt G (And lista)) = validF I s (And lista)")
 prefer 2
 apply (erule_tac x="sizeF (And lista)" in allE)
 apply (subgoal_tac "(sizeF (And lista)) < (Suc (Suc (((sizeF a) + (sizeFs lista)) + (length lista))))")
  prefer 2
  apply (simp (no_asm))
 apply (drule mp, assumption)
 apply (erule_tac x="G" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="And lista" in allE)
 apply (simp add: split_paired_all)
apply (case_tac "(delL T ((flattenAnd (vcopt G a)) @ (flattenAndL (vcoptL G lista))))")
apply simp
apply (subgoal_tac "validF I s (And (delL T (flattenAnd (vcopt G a)))) \<and> validF I s (And (delL T (flattenAndL (vcoptL G lista))))")
 prefer 2
 apply (simp only: validF_And_split[THEN sym])
 apply (simp only: delL_split[THEN sym])
 apply simp
apply (erule conjE)+
apply (simp add: delT_validFs flattenAnd_validFs flattenAndL_validFs)
apply (case_tac "(\<Lambda> lista) mem G")
apply simp

apply (simp add: Let_def)
apply (case_tac "(delL T (flattenAndL (vcoptL G lista)))")
apply simp

apply (simp only: delL_split)
apply simp

--{* case : ((delL T ((flattenAnd (vcopt G a)) @ (flattenAndL (vcoptL G lista)))) = (aa  listb)) *}

apply (simp only: list.cases)

apply (case_tac "(F mem (delL T (flattenAndL (vcoptL G (a # lista)))))")
apply (simp only: bool.cases vcopt_vcoptL.simps flattenAnd_flattenAndL.simps)
apply (drule_tac t="aa # listb" in sym)
apply (simp only: delL_split set_mem_eq set_append mem_simps)
apply (case_tac "(F \<in> (set (delL T (flattenAnd (vcopt G a)))))")
apply (subgoal_tac "\<not> (validF I s (And (delL T (flattenAnd (vcopt G a)))))")
 prefer 2
 apply (rule F_And)
 apply assumption
apply (simp only: delT_validFs flattenAnd_validFs validF_validFs.simps simp_thms)

apply (simp only: simp_thms)
apply (case_tac "And lista \<in> set G")
apply simp (* Hier kein subgoal complete ? *)

apply (subgoal_tac "\<not> (validF I s (\<Lambda> (delL T (flattenAndL (vcoptL G lista)))))")
 prefer 2
 apply (rule F_And)
 apply assumption
apply (simp only: simp_thms delT_validFs delT_And_validF flattenAndL_validF)
apply (drule not_And_validF)
apply (erule bexE)
apply (frule vcoptL_src)
apply (erule bexE)
apply (subgoal_tac "validF I s (And lista)")
 prefer 2
 apply (erule_tac x="And lista" in ballE)
 apply assumption
 apply simp
apply (simp only: And_validF_all)
apply (erule_tac x="y" and A="set lista" in ballE)
apply (subgoal_tac "validF I s (vcopt G y) = validF I s y")
 prefer 2
 apply (erule_tac x="sizeF y" in allE)
 apply (subgoal_tac "((sizeF y) < (Suc (Suc (((sizeF a) + (sizeFs lista)) + (length lista)))))")
  prefer 2
  apply (cut_tac "sizeF_sizeFs")
  apply (erule_tac x="lista" in allE)
  apply (erule_tac x="y" in allE)
  apply simp
 apply (drule mp, assumption)
 apply (erule_tac x="G" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="y" in allE)
 apply (simp only: split_paired_all)
apply simp

apply simp

apply simp (* Hier kein subgoal complete *)

apply (case_tac "(delL T (flattenAndL (vcoptL G lista)))")
apply simp

apply (simp add: Let_def) 

apply (simp only: bool.cases vcopt_vcoptL.simps flattenAnd_flattenAndL.simps)
apply (drule_tac t="aa # listb" in sym)
apply (simp only: delT_And_validF delT_validFs flattenAnd_validF flattenAnd_validFs validF_And_split simp_thms) (* Hier kein subgoal complete *)

apply (case_tac "And lista mem G")
apply simp
apply (subgoal_tac "(validF I s (\<Lambda> (flattenAndL (vcoptL G lista))))")
 prefer 2
 apply (rule classical)
 apply (simp only: flattenAndL_validF)
 apply (drule not_And_validF)
 apply (erule bexE)
 apply (drule vcoptL_src)
 apply (erule bexE)
 apply (subgoal_tac "validF I s (And lista)")
  prefer 2
  apply (erule_tac x="And lista" in ballE)
  apply assumption
  apply simp
 apply (simp only: And_validF_all)
 apply (erule_tac x="y" and A="set lista" in ballE)
 apply (subgoal_tac "validF I s (vcopt G y) = validF I s y")
 prefer 2
 apply (erule_tac x="sizeF y" in allE)
 apply (subgoal_tac "((sizeF y) < (Suc (Suc (((sizeF a) + (sizeFs lista)) + (length lista)))))")
  prefer 2
  apply (cut_tac "sizeF_sizeFs")
  apply (erule_tac x="lista" in allE)
  apply (erule_tac x="y" in allE)
  apply simp
 apply (drule mp, assumption)
 apply (erule_tac x="G" in allE)
 apply (erule_tac x="I" in allE)
 apply (erule_tac x="y" in allE)
 apply (simp only: split_paired_all)
apply simp

apply simp

apply simp

--{* case not (And lista mem G) *}

apply (simp add: Let_def)
apply (case_tac "(delL T (flattenAndL (vcoptL G lista)))")
apply simp
apply (subgoal_tac "validF I s (And (delL T (flattenAndL (vcoptL G lista))))")
 prefer 2
 apply simp
apply (erule_tac P="validF I s (And (delL T ?a))" in rev_mp)
apply (simp (no_asm) only: delT_And_validF delT_validFs simp_thms)
apply (rule impI)
apply simp

--{* delL T (flattenAndL (vcoptL G lista)) = ab  listc *}
apply (simp only: list.cases)
apply (drule_tac t="ab # listc" in sym)
apply (simp only:) (* Hier kein subgoal complete *)

apply (subgoal_tac "\<not> (F mem (delL T (flattenAndL (vcoptL G lista))))")
 prefer 2
 apply (subgoal_tac "delL T ((flattenAnd (vcopt G a)) @ (flattenAndL (vcoptL G lista))) =
                     (delL T ((flattenAnd (vcopt G a)))) @ (delL T (flattenAndL (vcoptL G lista)))")
  prefer 2
  apply (simp only: delL_split)
 apply (simp add: set_mem_eq set_append)

apply (simp add: bool.cases delT_And_validF delT_validFs)

--{* Imp form1 form2 *}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps)

apply (subgoal_tac "validF I s (vcopt G form1) = validF I s form1")
 prefer 2
 apply (erule_tac x="sizeF form1" in allE)
 apply simp
 
apply (subgoal_tac "validF I s (vcopt G form2) = validF I s form2")
 prefer 2
 apply (erule_tac x="sizeF form2" in allE)
 apply simp

apply (case_tac "(form1 \<supset> form2) mem G")
apply simp
apply (erule_tac x="Imp form1 form2" in ballE) 
apply (simp add: validF_validFs.simps)

apply (simp add: set_mem_eq)

--{* case: not (Imp form1 form2) mem G *}
apply (simp add: Let_def)

apply (case_tac "((vcopt G form1) = T)")
apply simp

--{* case not  ((vcopt G form1) = T *}
apply simp
apply (case_tac "(vcopt G form1) = F")
apply simp

--{* case (vcopt G form1) ~= F *}
apply simp
apply (case_tac "(vcopt (G @ (flattenAnd (vcopt G form1))) form2) = T")
apply simp
apply (rule impI)
apply (drule_tac s="validF I s (vcopt G form1)" in sym)
apply (simp only:)
apply (subgoal_tac "validF I s (And (flattenAnd (vcopt G form1)))")
 prefer 2
 apply (simp only: flattenAnd_validF)
apply (subgoal_tac "\<forall> x \<in> set (G @ (flattenAnd (vcopt G form1))). validF I s x")
 prefer 2
 apply (rule ballI)
 apply (simp add: set_append del: validF_validFs.simps)
 apply (erule disjE)
 apply (erule_tac x="x" in ballE)
 apply assumption
 apply simp

 apply (simp only: And_validF_all)

apply (erule_tac x="sizeF form2" in allE)
apply simp
apply (erule_tac x="G @ (flattenAnd (vcopt G form1)) " in allE)
apply (erule_tac x="I" in allE)
apply (erule_tac x="form2" in allE)
apply simp

--{* case:   ((vcopt (G @ (flattenAnd (vcopt G form1))) form2) ~= T *}
apply simp
apply (case_tac "validF I s form1")
apply simp (* Hier kein subgoal complete *)

apply (subgoal_tac "validF I s (And (flattenAnd (vcopt G form1)))")
 prefer 2
 apply (simp only: flattenAnd_validF)
apply (subgoal_tac "\<forall> x \<in> set (G @ (flattenAnd (vcopt G form1))). validF I s x")
 prefer 2
 apply (rule ballI)
 apply (simp add: set_append del: validF_validFs.simps)
 apply (erule disjE)
 apply (erule_tac x="x" in ballE)
 apply assumption
 apply simp
 apply (simp only: And_validF_all)

apply (erule_tac x="sizeF form2" in allE)
apply simp

apply simp

--{* Neg f *}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps Let_def)

apply (subgoal_tac "validF I s (vcopt G form) = validF I s form")
 prefer 2
 apply (fastsimp)

apply (case_tac "(vcopt G form) = T")
apply simp

apply simp
apply (case_tac "(vcopt G form) = F")
apply simp

apply simp

--{* Eq expr1 expr2 *}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps Let_def)
apply (case_tac "(expr1 \<doteq> expr2) mem G")
apply simp
apply (erule_tac x="(expr1 \<doteq> expr2)" in ballE)
apply simp
apply (simp add: set_mem_eq)

--{* case not (Eq expr1 expr2) mem G *}
apply simp
apply (case_tac "(isconstant expr1) \<and> (isconstant expr2)")
apply simp
apply (subgoal_tac "(eval I0 initialState expr1) = (eval I s expr1)")
 prefer 2
 apply (rule isconstant_eval)
 apply simp

apply (subgoal_tac "(eval I0 initialState expr2) = (eval I s expr2)")
 prefer 2
 apply (rule isconstant_eval)
 apply simp

apply simp
apply (case_tac "(eval I s expr1) = (eval I s expr2)")
apply simp

apply simp

--{* case not (isconstant expr1 and isconstant expr2) *}
apply (simp only: bool.cases)
apply simp

--{* Leq expr1 expr2 *}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps Let_def)
apply (case_tac "(Leq expr1 expr2) mem G")
apply simp
apply (erule_tac x="(Leq expr1 expr2)" in ballE)
apply simp
apply (simp add: set_mem_eq)

--{* case not (Leq expr1 expr2) mem G *}
apply simp
apply (case_tac "(isconstant expr1) \<and> (isconstant expr2)")
apply simp
apply (subgoal_tac "(eval I0 initialState expr1) = (eval I s expr1)")
 prefer 2
 apply (rule isconstant_eval)
 apply simp

apply (subgoal_tac "(eval I0 initialState expr2) = (eval I s expr2)")
 prefer 2
 apply (rule isconstant_eval)
 apply simp

apply simp
apply (case_tac "((nv (eval I s expr1)) \<le> (nv (eval I s expr2)))")
apply simp

apply simp

--{* case not (isconstant expr1 and isconstant expr2) *}
apply (simp only: bool.cases)
apply simp

--{* Less  expr1 expr2*}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps Let_def)
apply (case_tac "(Less expr1 expr2) mem G")
apply simp
apply (erule_tac x="(Less expr1 expr2)" in ballE)
apply simp
apply (simp add: set_mem_eq)

--{* case not (Less expr1 expr2) mem G *}
apply simp
apply (case_tac "(isconstant expr1) \<and> (isconstant expr2)")
apply simp
apply (subgoal_tac "(eval I0 initialState expr1) = (eval I s expr1)")
 prefer 2
 apply (rule isconstant_eval)
 apply simp

apply (subgoal_tac "(eval I0 initialState expr2) = (eval I s expr2)")
 prefer 2
 apply (rule isconstant_eval)
 apply simp

apply simp
apply (case_tac "((nv (eval I s expr1)) < (nv (eval I s expr2)))")
apply simp

apply simp

--{* case not (isconstant expr1 and isconstant expr2) *}
apply (simp only: bool.cases)
apply simp

--{* Ty expr vtype *}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps Let_def)
apply (case_tac "(Ty expr vtype) mem G")
apply simp
apply (erule_tac x="(Ty expr vtype)" in ballE)
apply simp
apply (case_tac "eval I s expr")
apply simp
apply simp
apply simp

apply (simp add: set_mem_eq)
--{* case not (Ty expr vtype) mem G *}
apply simp
apply (case_tac "(isconstant expr)")
apply simp
apply (subgoal_tac "(eval I0 initialState expr) = (eval I s expr)")
 prefer 2
 apply (rule isconstant_eval)
 apply simp

apply simp
apply (case_tac "eval I s expr")
apply simp
apply (case_tac "vtype")
apply simp
apply simp

apply simp
apply (case_tac "vtype")
apply simp
apply simp

apply simp
apply (case_tac "vtype")
apply simp
apply simp

--{* case not (isconstant expr1 and isconstant expr2) *}
apply (simp only: bool.cases)
apply simp
apply (case_tac "eval I s expr")
apply simp
apply (case_tac "vtype")
apply simp
apply simp

apply (case_tac "vtype")
apply simp
apply simp

apply (case_tac "vtype")
apply simp
apply simp
--{* Forall nat. form *}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps Let_def)

apply (case_tac "(Forall nat form) mem G")
apply simp
apply (erule_tac x="(Forall nat form)" in ballE)
apply (simp add: Let_def)
apply (simp add: set_mem_eq)

apply (simp add: Let_def)

--{* Yields expr list *}

apply (simp add: vcopt_vcoptL.simps valid_def validF_validFs.simps Let_def)
(*>*)
done

theorem vcopt_soundness:
"((prg::SALprogram),s \<Turnstile> vcopt [] f) = (prg,s \<Turnstile> f)"
(*<*)
apply (simp add: valid_def)
apply (rule doubleAllI)
apply (rule allI)
apply (rule vcopt_sound)
apply simp
(*>*)
done



end