header {* 
  \isaheader{Frequently Used Auxiliary Lemmas} 
*}

theory AuxBox = PCCFramework:

lemmas set_mem_eq = mem_iff

--{* changes the preprocessor for the simplifier, such that internally
   generated lemmas are augmented with proof objects *}
setup {* [Simplifier.change_simpset_of op setmksimps (setmp proofs 2 (mksimps mksimps_pairs))] *} 


lemma forall_switch2:
"(\<forall> x y. P x y) \<Longrightarrow> (\<forall> y x. P x y)"
(*<*) by simp (*>*)


lemma forall_switch3:
"(\<forall> z. (\<forall> x . (\<forall> y. P x y z))) \<Longrightarrow> (\<forall> x y z. P x y z)"
(*<*) by simp (*>*)


lemma forall_switch4: "(\<forall>z w x y. P w x y z) \<Longrightarrow> (\<forall>w x y z. P w x y z)"
(*<*) by simp (*>*)


lemma forall_switch5:
"\<forall> z v w x y. P v w x y z \<Longrightarrow> \<forall> v. \<forall> w. \<forall> x. \<forall> y. \<forall> z. P v w x y z"
(*<*) by simp (*>*)


lemma forall_switch6:
"\<forall> y q z v w x. P v w x y z q \<Longrightarrow> \<forall> q. \<forall> z. \<forall> v. \<forall> w. \<forall> x. \<forall> y. P v w x y z q"
(*<*) by simp (*>*)


lemma forall_switch7:
"\<forall> r v w x y z q. P v w x y z q r \<Longrightarrow> \<forall> v. \<forall> w. \<forall> x. \<forall> y. \<forall> z. \<forall> q. \<forall> r. P v w x y z q r"
(*<*) by simp (*>*)


lemma forall_switch8:
"\<forall> r v w x y z q s. P v w x y z q s r \<Longrightarrow> \<forall> v. \<forall> w. \<forall> x. \<forall> y. \<forall> z. \<forall> q. \<forall> s. \<forall> r. P v w x y z q s r"
(*<*) by simp (*>*)


lemma forall_switch9:
"\<forall> z r s t u v w x y . P r s t u v w x y z \<Longrightarrow> \<forall> r. \<forall> s. \<forall> t. \<forall> u. \<forall> v. \<forall> w. \<forall> x. \<forall> y. \<forall> z.  P r s t u v w x y z"
(*<*) by simp (*>*)


lemma forall_switch10:
"\<forall> z q r s t u v w x y . P q r s t u v w x y z \<Longrightarrow> \<forall> q. \<forall> r. \<forall> s. \<forall> t. \<forall> u. \<forall> v. \<forall> w. \<forall> x. \<forall> y. \<forall> z.  P q r s t u v w x y z"
(*<*) by simp (*>*)



lemma forall_switch11:
"\<forall> z p q r s t u v w x y . P p q r s t u v w x y z \<Longrightarrow> \<forall> p. \<forall> q. \<forall> r. \<forall> s. \<forall> t. \<forall> u. \<forall> v. \<forall> w. \<forall> x. \<forall> y. \<forall> z.  P p q r s t u v w x y z"
(*<*) by simp (*>*)


lemma forall_switch12:
"\<forall> z n p q r s t u v w x y. P n p q r s t u v w x y z \<Longrightarrow> \<forall>n. \<forall> p. \<forall> q. \<forall> r. \<forall> s. \<forall> t. \<forall> u. \<forall> v. \<forall> w. \<forall> x. \<forall> y. \<forall> z.  P n p q r s t u v w x y z"
(*<*) by simp (*>*)


lemma notin_union_E:
"x \<notin> (A \<union> B) = ((x \<notin> A) \<and> (x \<notin> B))"
(*<*) by simp (*>*)


lemma notin_subset:
"\<lbrakk> x \<notin> A; B \<subseteq> A \<rbrakk> \<Longrightarrow> x \<notin> B"
(*<*) by auto (*>*)


lemma notin_Union_iff:
"A \<notin> (\<Union> S) = (\<forall> X\<in>S. A \<notin> X)"
(*<*) by auto (*>*)


lemma refl_True:
"(t = t) = True"
(*<*) by simp (*>*)


lemma refl_Some:
"(Some x = Some y) = (x = y)"
(*<*) by simp (*>*)


lemma elem_set_append_cases:
"\<forall> x l1 l2.  x \<in> set (l1@l2) = (x \<in> set l1) \<or> (x \<in> set l2)"
(*<*) by auto (*>*)


lemma suc_minus_swap:
"\<lbrakk> a <= b \<rbrakk> \<Longrightarrow> (Suc b) - a = Suc (b - a)"
(*<*) by arith (*>*)


lemma rel_pow_step: "Re O Re ^ n = Re ^ (Suc n)"
(*<*) by simp (*>*)


lemma min_elim:
"(a::'a::order) < b \<Longrightarrow> (min a b) = a"
(*<*)
apply (simp add: min_def)
apply (rule impI)
apply (drule order_less_imp_le)
apply simp
done
(*>*)


lemma suc_eq_plus1:
"Suc x = x + 1"
(*<*) by simp (*>*)


lemma less_diff_conv2: "((a::nat) + b < c) = (a < c - b)"
(*<*) by arith (*>*)


lemma conjI':
"\<lbrakk> X; X \<Longrightarrow> Y \<rbrakk> \<Longrightarrow> (X \<and> Y)"
(*<*) by blast (*>*)


lemma disjE2: "a | b \<Longrightarrow> ~ a \<Longrightarrow> b"
(*<*) by auto (*>*)


lemma set_concat_map:
"set (concat (map f xs)) =  Union (set ` (f ` set xs))"
(*<*) by auto (*>*)


lemma doubleAllI:
"(\<forall> x. P x = Q x) \<Longrightarrow> (\<forall> x. P x) = (\<forall> y. Q y)"

(*<*) by simp (*>*)


constdefs
delL::"'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
"delL a xs == [x\<in>xs. x \<noteq> a]"


lemma delL_length:
"\<And> a. a \<in> set xs \<Longrightarrow> length (delL a xs) < length xs"
(*<*)
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (induct xs)
apply simp
apply (rule allI)
apply (case_tac "aa = a")
apply (simp add: delL_def)
apply (simp only: not_less_eq[THEN sym])
apply (simp only: linorder_not_less)
apply (rule length_filter_le)
apply (erule_tac x = "aa" in allE)
apply (rule impI)
apply (simp add: delL_def)
done
(*>*)


lemma delL_setdiff: "set (delL x xs) = (set xs) - {x}"
(*<*)
apply (simp add: delL_def)
apply auto
done
(*>*)


lemma setdiff_notin:
"x \<notin> B \<Longrightarrow> (x \<notin> (A - B)) = (x \<notin> A)"
(*<*) by auto (*>*)


lemma delL_subset:
"\<And> x. set (delL x xs) \<subseteq> set xs"
(*<*)
apply (simp add: delL_setdiff set_diff_def)
apply (rule subsetI)
apply simp
done
(*>*)


lemma eqSOME: "\<forall> x. P x = Q x \<Longrightarrow> ((SOME x. P x) = (SOME y. Q y))"
(*<*)
by simp
(*>*)


lemma not_Some_eq_pairs:
"\<forall>a b. x \<noteq> Some (a,b) \<Longrightarrow> x = None"
(*<*)
apply (case_tac "x=None")
apply simp
apply (simp only: not_None_eq)
apply (erule exE)
apply (erule_tac x="fst y" in allE)
apply (erule_tac x="snd y" in allE)
apply simp
done
(*>*)


lemma tl_drop:
"tl L = drop (Suc 0) L"
(*<*)
apply (induct L)
apply simp
apply simp
done
(*>*)


lemma remdups'_termination:
"\<forall>x xs. length [x'\<in>xs . x' \<noteq> x] < Suc (length xs)"
(*<*)
apply (rule allI)+
apply (induct_tac xs)
apply simp
apply simp
done
(*>*)

consts remdups'::"'a list \<Rightarrow> 'a list"

recdef remdups' "measure (\<lambda> xs. length xs)"
"remdups' [] = []"
"remdups' (x#xs) = x#(remdups' [x'\<in>xs. x' \<noteq> x])" 

(hints simp: remdups'_termination)


lemma set_remdups':
"\<And> xs. set (remdups' xs) = set xs"
(*<*)
apply (subgoal_tac "\<exists> k. k = length xs")
 prefer 2
 apply fastsimp
apply (erule exE | 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 (case_tac "xs")
apply simp

apply simp
apply (erule_tac x="length [x' \<in> list. x' \<noteq> a]" in allE)
apply (subgoal_tac "length [x' \<in> list. x' \<noteq> a] \<le> length list")
 prefer 2
 apply (rule length_filter_le)
apply simp
apply (erule_tac x="[x' \<in> list. x' \<noteq> a]" in allE)
apply simp

apply (rule set_ext)
apply simp
apply (case_tac "x=a")
apply simp
apply simp
done
(*>*)


lemma distinct_remdups':
"\<And> xs. distinct (remdups' xs)"
(*<*)
apply (subgoal_tac "\<exists> k. k = length xs")
 prefer 2
 apply fastsimp
apply (erule exE | 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 (case_tac "xs")
apply simp

apply simp
apply (erule_tac x="length [x' \<in> list. x' \<noteq> a]" in allE)
apply (subgoal_tac "length [x' \<in> list. x' \<noteq> a] \<le> length list")
 prefer 2
 apply (rule length_filter_le)
apply simp
apply (erule_tac x="[x' \<in> list. x' \<noteq> a]" in allE)
apply (simp add: set_remdups')
done
(*>*)


lemma filter_eq:
"\<forall> x \<in> set xs. P x = Q x \<Longrightarrow> [x\<in> xs. P x] = [x \<in> xs. Q x]"
(*<*)
apply (induct xs)
apply simp

apply simp
done
(*>*)


lemma remdups'_append:
"\<And> as bs. remdups' (as @ bs) = remdups' as @ [b\<in> remdups' bs. b \<notin> set as]"
(*<*)
apply (subgoal_tac "\<exists> k. k = length as")
 prefer 2
 apply fastsimp
apply (erule exE | erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch3)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)
apply (case_tac "as")
apply simp

apply simp
apply (erule_tac x="length [x' \<in> list. x' \<noteq> a]" in allE)
apply (subgoal_tac "length [x' \<in> list. x' \<noteq> a] < Suc (length list)")
 prefer 2
 apply (subgoal_tac "length [x' \<in> list. x' \<noteq> a] \<le> (length list)")
  prefer 2
  apply simp
 apply (simp (no_asm_simp))
apply (drule mp, assumption)
apply simp

apply (erule thin_rl)+
apply (subgoal_tac "\<exists> k. k = length bs")
 prefer 2
 apply fastsimp
apply (erule exE)+
apply (erule rev_mp)
apply (simp only: atomize_all)
apply (rule forall_switch6)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)


apply (case_tac "bs")
apply simp

apply (simp split del: split_if)
apply (case_tac "aa \<noteq> a")
apply simp
apply (erule_tac x="length [x'\<in>lista . x' \<noteq> aa]" in allE)
apply (subgoal_tac "length [x'\<in>lista . x' \<noteq> aa] \<le> length lista")
 prefer 2
 apply simp
apply simp
apply (erule_tac x="[x'\<in>lista . x' \<noteq> aa]" in allE)
apply simp
apply (erule_tac x="a" in  allE)
apply (erule_tac x="list" in allE)
apply (subgoal_tac "[x\<in>lista . x \<noteq> aa \<and> x \<noteq> a] = [x\<in>lista . x \<noteq> a \<and> x \<noteq> aa]")
 prefer 2
 apply (rule filter_eq) 
 apply (rule ballI)
 apply (rule iffI)
 apply simp
 apply simp
apply simp

apply simp
apply (erule_tac x="length [x'\<in>lista . x' \<noteq> a]" in allE)
apply (subgoal_tac "length [x'\<in>lista . x' \<noteq> a] \<le> length lista")
 prefer 2
 apply simp
apply simp
apply (erule_tac x="[x'\<in>lista . x' \<noteq> a]" in allE)
apply simp
apply (erule_tac x="a" in  allE)
apply (erule_tac x="list" in allE)
apply (subgoal_tac "[x\<in>lista . x \<noteq> a \<and> x \<noteq> a] = [x\<in>lista . x \<noteq> a]")
 prefer 2
 apply (rule filter_eq) 
 apply simp

apply simp
done
(*>*)


lemma remdups'_append_fst:
"a \<notin> set as \<Longrightarrow> remdups' (as@[a]@as') = remdups' as @ [a] @ ([a' \<in> (remdups' as'). a' \<notin> set (as @ [a])])"
(*<*)
apply (simp only: remdups'_append)
apply simp
done
(*>*)


lemma in_remdups'_split:
"x \<in> set (remdups' xs) \<Longrightarrow> \<exists>as bs. (remdups' xs) = as @ (x#bs) \<and> x\<notin> set as \<and> x \<notin> set bs"
(*<*)
apply (subgoal_tac "distinct (remdups' xs)")
 prefer 2
 apply (rule distinct_remdups')
apply (simp only: in_set_conv_decomp)
apply (erule exE)+
apply (rule_tac x="ys" in exI)
apply (rule_tac x="zs" in exI)
apply simp
apply (rule conjI)
apply (rule allI)+
apply (rule classical)
apply simp

apply (rule allI)+
apply (rule classical)
apply simp
done
(*>*)


lemma in_set_remdups':
"x \<in> set xs \<Longrightarrow> x \<in> set (remdups' xs)"
(*<*)
by (simp add: set_remdups')
(*>*)


lemma in_rd_sp:
"x \<in> set xs \<Longrightarrow> \<exists>as bs. (remdups' xs) = as @ (x#bs) \<and> x\<notin> set as \<and> x \<notin> set bs"
(*<*)
apply (rule in_remdups'_split)
apply (simp add: set_remdups')
done
(*>*)


lemma remdups'_empty [simp]:
"(remdups' l = []) = (l = [])"
(*<*)
apply (induct l)
apply simp
apply simp
done
(*>*)


lemma length_remdups_set:
"length (remdups' xs) \<le> Suc 0 = (\<forall> x y. x \<in> set xs \<and> y \<in> set xs \<longrightarrow> x = y)"
(*<*)
apply (rule iffI)
apply (case_tac "remdups' xs")
apply simp
apply (case_tac "list")
prefer 2
apply simp
apply simp
apply (subgoal_tac "set xs = set [a]")
 prefer 2
 apply (subgoal_tac "set (remdups' xs) = set xs")
   prefer 2
   apply (rule set_remdups')
 apply simp
apply simp

apply (case_tac "remdups' xs")
apply simp
apply (case_tac "list")
apply simp

apply simp
apply (subgoal_tac "set xs = set (a # aa # lista)")
 prefer 2
 apply (subgoal_tac "set (remdups' xs) = set xs")
   prefer 2
   apply (rule set_remdups')
 apply simp
apply simp
apply (erule_tac x="a" in allE)
apply (erule_tac x="aa" in allE)
apply simp
apply (subgoal_tac "distinct (remdups' xs)")
 prefer 2
 apply (rule distinct_remdups')
apply simp
done
(*>*)


lemma in_set_conv_decomp_fst':
"(x \<in> set xs) = (\<exists>ys zs. (xs = ys @ x # zs) \<and> x \<notin> set ys)"
(*<*)
apply (induct xs)
apply simp
apply (rule iffI)
apply simp
apply (case_tac "x=a")
apply simp
apply (rule_tac x="[]" in exI)
apply simp

apply simp
apply (erule exE)
apply (rule_tac x="a#ys" in exI)
apply simp

apply simp
apply (case_tac "x=a")
apply simp
apply simp
apply (erule exE)
apply (case_tac "ys")
apply simp
apply (rule_tac x="list" in exI)
apply simp
done
(*>*)


lemma in_set_conv_decomp_fst:
"(x \<in> set xs) \<Longrightarrow> (\<exists>ys zs. (xs = ys @ x # zs) \<and> x \<notin> set ys)"
(*<*)
apply (subgoal_tac "(\<exists>ys zs. (xs = ys @ x # zs) \<and> x \<notin> set ys) = (x \<in> set xs)")
 prefer 2
 apply (rule sym)
 apply (rule in_set_conv_decomp_fst')
apply simp
done
(*>*)


lemma in_set_conv_decomp_last:
"(x \<in> set xs) \<Longrightarrow> (\<exists>ys zs. (xs = ys @ x # zs) \<and> x \<notin> set zs)"
(*<*)
apply (induct xs)
apply simp

apply simp
apply (erule disjE)
apply (case_tac  "x \<in> set xs")
apply simp
apply (erule exE)+
apply (rule_tac x="a # ys" in exI)
apply (rule_tac x="zs" in exI)
apply simp
apply (rule_tac x="[]" in exI)
apply (rule_tac x="xs" in exI)
apply simp

apply simp
apply (erule exE)+
apply (rule_tac x="a # ys" in exI)
apply (rule_tac x="zs" in exI)
apply simp
done
(*>*)


lemma map_parts:
"\<And> ys ys'. map f xs = ys@ys' \<Longrightarrow> \<exists> xs' xs''. xs = xs' @ xs'' \<and> ys = map f xs' \<and> ys' = map f xs''"
(*<*)
apply (induct xs)
apply simp
apply atomize
apply (case_tac "ys")
apply (case_tac "ys'")
apply simp

apply (erule_tac x="[]" in allE)
apply (erule_tac x="list" in allE)
apply simp

apply (erule_tac x="list" in allE)
apply (erule_tac x="ys'" in allE)
apply simp
apply (erule exE)+
apply (rule_tac x="a # xs'" in exI)
apply (rule_tac x="xs''" in exI)
apply simp
done
(*>*)


lemma option_neq: "(Some x = None) = False"
(*<*) by simp (*>*)


lemma option_neq2:"(None = Some x) = False"
(*<*) by simp (*>*)

(*<*)
lemmas option_simp = option_neq option_neq2
(*>*)

lemma append_eq:
"(xs@xs' = xs@xs'') = (xs' = xs'')"
(*<*) by simp (*>*)

lemma list_set_pred:
"(\<exists> xs x xs'. ys = xs @ x # xs' \<and> P x) = (\<exists> x \<in> set ys. P x)"
(*<*)
apply (rule iffI)
apply (erule exE)+
apply (rule_tac x="x" in bexI)
apply simp
apply simp

apply (erule bexE)
apply (simp only: in_set_conv_decomp)
apply (erule exE )+
apply fastsimp
done
(*>*)


lemma in_set_conv_decomp_2:
"\<lbrakk> x \<in> set s; y \<in> set s; x \<noteq> y \<rbrakk> \<Longrightarrow> \<exists> s' s'' s'''. s = s' @ x # s'' @ y # s''' \<or> s = s' @ y # s'' @ x # s'''"
(*<*)
apply (induct s)
apply simp
apply atomize
apply simp
apply (case_tac "x = a")
apply (case_tac "y = a")
apply simp

apply simp
apply (rule_tac x="[]" in exI)
apply (simp add: in_set_conv_decomp)

apply (case_tac "y = a")
apply simp
apply (rule_tac x="[]" in exI)
apply (simp add: in_set_conv_decomp)
apply (erule exE)+
apply (rule_tac x="ys" in exI)
apply (rule_tac x="zs" in exI)
apply simp

apply simp
apply (erule exE)+
apply (rule_tac x="a # s'" in exI)
apply (rule_tac x="s''" in exI)
apply (rule_tac x="s'''" in exI)
apply simp
done
(*>*)


lemma list_prefix_eq: "\<And>as bs. \<lbrakk> as @ x # as' = bs @ x # bs'; x \<notin> set as; x \<notin> set bs \<rbrakk> 
 \<Longrightarrow> as = bs"
(*<*)
apply (subgoal_tac "\<exists>k. k = length as + length bs")
 prefer 2
 apply simp
apply (erule exE)
apply (erule rev_mp)+
apply (simp only: atomize_all)
apply (rule forall_switch3)
apply (rule allI)
apply (rule_tac n="k" in nat_less_induct)
apply (rule allI)+
apply (rule impI)+
apply (case_tac "as")
apply (case_tac "bs")
apply simp

apply simp

apply (case_tac "bs")
apply simp

apply (erule_tac x="length list + length lista" in allE)
apply simp
done
(*>*)


lemma distinct_list_match:
"\<lbrakk> as@[x]@as' = bs@[x]@bs'; distinct (as@[x]@as'); distinct (bs@[x]@bs') \<rbrakk> \<Longrightarrow> as = bs \<and> as' = bs'"
(*<*)
apply (erule_tac P="distinct (as @ [x] @ as')" in rev_mp)
apply (erule_tac P=" distinct (bs @ [x] @ bs')" in rev_mp)
apply (simp (no_asm))
apply (rule impI)+
apply (rule classical)
apply simp
apply (case_tac "as = bs")
apply simp
apply simp
apply (erule conjE)+
apply (subgoal_tac "as = bs")
 prefer 2
 apply (rule_tac x="x" and as'="as'" and bs'="bs'" in list_prefix_eq)
 apply assumption+ 
apply simp
done
(*>*)


lemma renSnd:
"x = x' \<Longrightarrow> \<forall>em. P em x = P em x'"
(*<*) by simp (*>*)


lemma allE2:
"\<lbrakk> \<forall> x y. P x y;  P x y \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
(*<*) by blast (*>*)


lemma rev_take_nth: "\<And> x y. \<lbrakk> x < length s; y < x \<rbrakk> \<Longrightarrow> s ! (x - Suc y) = rev (take x s) ! y"
(*<*)
apply (induct s)
apply simp

apply (case_tac "x - Suc y")
apply simp
apply (case_tac "x")
apply simp

apply (simp add: nth_append)

apply simp

apply (case_tac "x")
apply simp

apply (simp add: nth_append)
apply (rule conjI)
apply (rule impI)
apply atomize
apply (subgoal_tac "nata - (Suc y) = nat")
 prefer 2
 apply arith

apply (erule_tac x="nata" in allE)
apply (erule_tac x="y" in allE)
apply simp

apply arith
done
(*>*)


lemma split_if_False: "if B then A else False \<Longrightarrow> B \<and> A"
(*<*) by (simp split add: split_if_asm) (*>*)


lemma forall_expand: "(\<forall> x < Suc y. P x) = (P 0 \<and> (\<forall> x < y. P (Suc x)))"
(*<*)
apply (induct y)
apply simp

apply (rule iffI)
apply (rule conjI)
apply simp

apply simp

apply simp
apply (rule allI)
apply (rule impI)

apply (case_tac "x")
apply simp

apply simp
done
(*>*)


lemma not_Nil_case:
"x \<noteq> [] \<Longrightarrow> (case x of [] \<Rightarrow> a | l#ls \<Rightarrow> b l ls) = b (hd x) (tl x)"
(*<*)
apply (case_tac x)
apply simp

apply simp
done
(*>*)


lemma hd_arb:
"hd [] = arbitrary"
(*<*) by (simp add: hd_list_def) (*>*)


lemma prod_simp:
"(a,b) = (a',b') = (a = a' \<and> b = b')"
(*<*) by simp (*>*)


lemma length_filter_less:
"aa mem S \<Longrightarrow> length [a \<in> S. a \<noteq> aa] < length S"
(*<*)
apply (induct S)
apply simp

apply simp
apply (rule impI)
apply simp
apply (subgoal_tac "length [a\<in>S . a \<noteq> aa] \<le> length S")
 prefer 2
 apply (simp add: length_filter_le)
apply (subgoal_tac "Suc (length S) \<noteq> length S")
 prefer 2
 apply simp
apply (simp (no_asm_simp))
done
(*>*)


lemma insert_union_right:
"insert p (A \<union> B) = A \<union> (insert p B)"
(*<*) by (simp add: set_eq_subset) (*>*)


lemma insert_set_filter:
"(insert p {x. x \<in> set S \<and> x \<noteq> p}) = (insert p (set S))"
(*<*) by (simp add: set_eq_subset subset_def) (*>*)


lemma intersect_mono:
"set V \<inter> {x. x \<in> set S \<and> x \<noteq> p} \<subseteq>  set V \<inter> set S"
(*<*)
apply (simp add: set_eq_subset subset_def)
done
(*>*)


lemma Un_real_subset_iff:
"(X \<union> Y) \<subset> Z = (X \<subset> Z \<and> Y \<subset> Z \<and> X \<union> Y \<noteq> Z)"
(*<*)
apply (rule iffI)
apply (rule conjI)
apply (simp add: psubset_def)
apply (case_tac "X  = Z")
apply simp
apply (erule conjE)
apply (drule Un_absorb2)
apply simp

apply assumption

apply (simp add: psubset_def)
apply (case_tac "Y = Z")
apply simp
apply (erule conjE)
apply (drule Un_absorb1)
apply simp

apply assumption

apply (erule conjE)+
apply (simp add: psubset_def)
done
(*>*)


lemma map_fst_tuple :
"map fst (map (\<lambda>x. (x,f x)) L) = L"
(*<*)
apply (induct L)
apply simp

apply simp
done
(*>*)


lemma image_fst_tuple: " fst ` (\<lambda>p. (p, f p)) ` S = S"
(*<*)
apply (rule set_ext)
apply (rule iffI)
apply (erule imageE)
apply simp
apply (erule imageE)
apply simp
apply (rule_tac x="(\<lambda> p. (p, f p)) x" in image_eqI)
apply simp
apply (rule_tac x="id x" in image_eqI)
apply simp
apply simp
done
(*>*)


lemma list_length_split:
"\<And> n. n < length L \<Longrightarrow> \<exists> ls l ls'. L = ls@l#ls' \<and> length ls = n"
(*<*)
apply (induct L)
apply simp
apply simp
apply (case_tac "n")
apply simp
apply simp
apply atomize
apply (erule_tac x="nat" in allE)
apply simp
apply (erule exE | erule conjE)+
apply (rule_tac x="a#ls" in exI)
apply simp
done
(*>*)


lemma un_subset_drop:
"(X \<union> (Y \<union> Z)) \<subset> W \<Longrightarrow> (X \<union> Y) \<subset> W"
(*>*) by blast (*>*)


lemma un_subset_drop':
"(X \<union> (Y \<union> (Z \<union> (U \<union> V)))) \<subset> W \<Longrightarrow> (X \<union> (Z \<union> U)) \<subset> W"
(*<*) by blast (*>*)


lemma ListEq:
"(a#al = b#bl) = (a=b \<and> al=bl)"
(*<*) by auto (*>*)


lemma seteq_simp:
"(\<forall> x. (x \<in> A) = (x \<in> B)) \<Longrightarrow> A = B"
(*<*) by auto (*>*)


lemma map_simp2:
"(\<forall>x. x \<in> set l \<longrightarrow> f x = f' x) \<longrightarrow> map f l = map f' l"
(*<*) apply (induct l) apply auto done (*>*)


lemma map_simp:
"\<lbrakk> l = l'; (\<forall> x. x\<in> set l \<longrightarrow> (f x) = (f' x)) \<rbrakk> \<Longrightarrow> (map f l) = (map f' l')"
(*<*) apply hypsubst apply (simp only: map_simp2) done (*>*)


lemma notin_simp:
"\<lbrakk> pc'\<notin> set l \<rbrakk> \<Longrightarrow> pc'\<notin> set [x\<in>l. x\<noteq> pc]"
(*<*) by auto (*>*)


lemma neg_notin_simp:
"\<lbrakk> pc\<noteq>pc'; \<not> pc'\<notin> set l \<rbrakk> \<Longrightarrow> \<not> pc'\<notin> set [x\<in>l. x\<noteq> pc]"
(*<*) by auto (*>*)


lemma option_case_simp:
"\<lbrakk> x \<noteq> None \<rbrakk> \<Longrightarrow> \<exists> a. x = Some a"
(*<*) by auto (*>*)


lemma filter_list_simp:
"\<lbrakk> pc\<notin> set l \<rbrakk> \<Longrightarrow> [x\<in>l. x\<noteq>pc \<and> x\<noteq>pc'] = [a\<in>l. a\<noteq>pc']"
(*<*)
apply (subgoal_tac "\<forall> x\<in>set l. x\<noteq>pc")
prefer 2
apply clarsimp
apply (simp only: filter_filter [ THEN sym])
apply (simp only: filter_True)
done
(*>*)


lemma list_abr_simp:
"[x\<in>S. x\<noteq>pc \<and> x\<noteq>pc'] = [x\<in>[a\<in>S. a \<noteq> pc]. x\<noteq>pc']"
(*<*)
apply auto
done
(*>*)

lemma if_then_else_False:
"(if (A::bool) then (B::bool) else False) = (A \<and> B)"
(*<*)
apply (case_tac "A")
apply simp
apply simp
done
(*>*)

lemma map_of_append':
"\<lbrakk> x \<notin> set (map fst xs) \<rbrakk> \<Longrightarrow> (map_of (xs @ ys)) x = (map_of ys) x"
(*<*)
apply (induct xs)
apply simp
apply simp
done
(*>*)

lemma triple_simp:
"(fst x, fst (snd x), snd (snd x)) = x"
(*<*) by fastsimp (*>*)

(*<*)
lemma conjE1:
"\<lbrakk> A \<and> B; B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp

lemma conjE2:
"\<lbrakk> A \<and> B; A \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
(*>*)


(*<*)
text {* Functions that calculate the size of proof objects. *}

ML {*
fun prf_size () =
  let
    val proof_state = Toplevel.proof_of (Toplevel.get_state ());
    val (_, (_, st)) = Proof.get_goal proof_state;
    val {der = (_, prf), ...} = rep_thm st
  in Proofterm.size_of_proof (prf)
  end;
*}


ML {*
fun nprf_size () =
  let
    val proof_state = Toplevel.proof_of (Toplevel.get_state ());
    val (_, (_, st)) = Proof.get_goal proof_state;
    val {der = (_, prf), ...} = rep_thm st
  in Proofterm.size_of_proof (Proofterm.rewrite_proof_notypes ([],
ProofRewriteRules.rprocs false) prf)
  end;
*}
(*>*)

end