"a \<le> b \<Longrightarrow> (a::'a::order) \<in> {a..b}"
by simp
lemma construct_singleton:
"\<lbrakk> S \<noteq> {}; \<forall>s\<in>S. \<forall>s'. s \<noteq> s' \<longrightarrow> s' \<notin> S \<rbrakk> \<Longrightarrow> \<exists>x. S = {x}"
by (simp add: graph_of_def restrict_map_def subset_iff)
lemma graph_ofD:
"(x,y) \<in> graph_of f \<Longrightarrow> f x = Some y"
by (simp add: graph_of_def)
lemma graph_ofI:
"m x = Some y \<Longrightarrow> (x, y) \<in> graph_of m"
by (simp add: graph_of_def)
lemma graph_of_empty :
"graph_of empty = {}"
by (simp add: graph_of_def)
lemma in_set_zip_refl :
"(x,y) \<in> set (zip xs xs) = (y = x \<and> x \<in> set xs)"
by (induct xs) auto
lemma map_conv_upd:
"m v = None \<Longrightarrow> m o (f (x := v)) = (m o f) (x := None)"
by (rule ext) (clarsimp simp: o_def)
lemma sum_all_ex [simp]:
"(\<forall>a. x \<noteq> Inl a) = (\<exists>a. x = Inr a)"
"(\<forall>a. x \<noteq> Inr a) = (\<exists>a. x = Inl a)"
by (metis Inr_not_Inl sum.exhaust)+
lemma split_distrib: "case_prod (\<lambda>a b. T (f a b)) = (\<lambda>x. T (case_prod (\<lambda>a b. f a b) x))"
by (clarsimp simp: split_def)
lemma case_sum_triv [simp]:
"(case x of Inl x \<Rightarrow> Inl x | Inr x \<Rightarrow> Inr x) = x"
by (clarsimp split: sum.splits)
lemma set_eq_UNIV: "({a. P a} = UNIV) = (\<forall>a. P a)"
by force
lemma allE2:
"\<lbrakk>\<forall>x y. P x y; P x y \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by blast
lemma allE3: "\<lbrakk> \<forall>x y z. P x y z; P x y z \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
by auto
lemma my_BallE: "\<lbrakk> \<forall>x \<in> A. P x; y \<in> A; P y \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
by (simp add: Ball_def)
lemma unit_Inl_or_Inr [simp]:
"\<And>a. (a \<noteq> Inl ()) = (a = Inr ())"
"\<And>a. (a \<noteq> Inr ()) = (a = Inl ())"
by (case_tac a; clarsimp)+
lemma disjE_L: "\<lbrakk> a \<or> b; a \<Longrightarrow> R; \<lbrakk> \<not> a; b \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
by blast
lemma disjE_R: "\<lbrakk> a \<or> b; \<lbrakk> \<not> b; a \<rbrakk> \<Longrightarrow> R; \<lbrakk> b \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
by blast
lemma int_max_thms:
"(a :: int) \<le> max a b"
"(b :: int) \<le> max a b"
by (auto simp: max_def)
lemma sgn_negation [simp]:
"sgn (-(x::int)) = - sgn x"
by (clarsimp simp: sgn_if)
lemma sgn_sgn_nonneg [simp]:
"sgn (a :: int) * sgn a \<noteq> -1"
by (clarsimp simp: sgn_if)
lemma inj_inj_on:
"inj f \<Longrightarrow> inj_on f A"
by (metis injD inj_onI)
lemma ex_eqI:
"\<lbrakk>\<And>x. f x = g x\<rbrakk> \<Longrightarrow> (\<exists>x. f x) = (\<exists>x. g x)"
by simp
lemma pre_post_ex:
"\<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> \<exists>x. Q x"
by auto
lemma ex_conj_increase:
"((\<exists>x. P x) \<and> Q) = (\<exists>x. P x \<and> Q)"
"(R \<and> (\<exists>x. S x)) = (\<exists>x. R \<and> S x)"
by simp+
lemma all_conj_increase:
"(( \<forall>x. P x) \<and> Q) = (\<forall>x. P x \<and> Q)"
"(R \<and> (\<forall>x. S x)) = (\<forall>x. R \<and> S x)"
by simp+
lemma Ball_conj_increase:
"xs \<noteq> {} \<Longrightarrow> (( \<forall>x \<in> xs. P x) \<and> Q) = (\<forall>x \<in> xs. P x \<and> Q)"
"xs \<noteq> {} \<Longrightarrow> (R \<and> (\<forall>x \<in> xs. S x)) = (\<forall>x \<in> xs. R \<and> S x)"
by auto
(***************
* Union rules *
***************)
lemma disjoint_subset:
assumes "A' \<subseteq> A" and "A \<inter> B = {}"
shows "A' \<inter> B = {}"
using assms by auto
lemma disjoint_subset2:
assumes "B' \<subseteq> B" and "A \<inter> B = {}"
shows "A \<inter> B' = {}"
using assms by auto
lemma UN_nth_mem:
"i < length xs \<Longrightarrow> f (xs ! i) \<subseteq> (\<Union>x\<in>set xs. f x)"
by (metis UN_upper nth_mem)
lemma Union_equal:
"f ` A = f ` B \<Longrightarrow> (\<Union>x \<in> A. f x) = (\<Union>x \<in> B. f x)"
by (subst Union_image_eq [symmetric]) simp
lemma UN_Diff_disjoint:
"i < length xs \<Longrightarrow> (A - (\<Union>x\<in>set xs. f x)) \<inter> f (xs ! i) = {}"
by (metis Diff_disjoint Int_commute UN_nth_mem disjoint_subset)
lemma image_list_update:
"f a = f (xs ! i)
\<Longrightarrow> f ` set (xs [i := a]) = f ` set xs"
by (metis list_update_id map_update set_map)
lemma Union_list_update_id:
"f a = f (xs ! i) \<Longrightarrow> (\<Union>x\<in>set (xs [i := a]). f x) = (\<Union>x\<in>set xs. f x)"
by (rule Union_equal) (erule image_list_update)
lemma Union_list_update_id':
"\<lbrakk>i < length xs; \<And>x. g (f x) = g x\<rbrakk>
\<Longrightarrow> (\<Union>x\<in>set (xs [i := f (xs ! i)]). g x) = (\<Union>x\<in>set xs. g x)"
by (metis Union_list_update_id)
lemma Union_subset:
"\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> (f x) \<subseteq> (g x)\<rbrakk> \<Longrightarrow> (\<Union>x \<in> A. f x) \<subseteq> (\<Union>x \<in> A. g x)"
by (metis UN_mono order_refl)
lemma UN_sub_empty:
"\<lbrakk>list_all P xs; \<And>x. P x \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> (\<Union>x\<in>set xs. f x) - (\<Union>x\<in>set xs. g x) = {}"
by (metis Ball_set_list_all Diff_cancel SUP_cong)
(*******************
* bij_betw rules. *
*******************)
lemma bij_betw_fun_updI:
"\<lbrakk>x \<notin> A; y \<notin> B; bij_betw f A B\<rbrakk> \<Longrightarrow> bij_betw (f(x := y)) (insert x A) (insert y B)"
by (clarsimp simp: bij_betw_def fun_upd_image inj_on_fun_updI split: split_if_asm)
definition
"bij_betw_map f A B \<equiv> bij_betw f A (Some ` B)"
lemma bij_betw_map_fun_updI:
"\<lbrakk>x \<notin> A; y \<notin> B; bij_betw_map f A B\<rbrakk>
\<Longrightarrow> bij_betw_map (f(x \<mapsto> y)) (insert x A) (insert y B)"
unfolding bij_betw_map_def by clarsimp (erule bij_betw_fun_updI; clarsimp)
lemma bij_betw_map_imp_inj_on:
"bij_betw_map f A B \<Longrightarrow> inj_on f A"
by (simp add: bij_betw_map_def bij_betw_imp_inj_on)
lemma bij_betw_empty_dom_exists:
"r = {} \<Longrightarrow> \<exists>t. bij_betw t {} r"
by (clarsimp simp: bij_betw_def)
lemma bij_betw_map_empty_dom_exists:
"r = {} \<Longrightarrow> \<exists>t. bij_betw_map t {} r"
by (clarsimp simp: bij_betw_map_def bij_betw_empty_dom_exists)
(*
* Function and Relation Powers.
*)
lemma funpow_add [simp]:
fixes f :: "'a \<Rightarrow> 'a"
shows "(f ^^ a) ((f ^^ b) s) = (f ^^ (a + b)) s"
by (metis comp_apply funpow_add)
lemma funpow_unfold:
fixes f :: "'a \<Rightarrow> 'a"
assumes "n > 0"
shows "f ^^ n = (f ^^ (n - 1)) \<circ> f"
by (metis Suc_diff_1 assms funpow_Suc_right)
lemma relpow_unfold: "n > 0 \<Longrightarrow> S ^^ n = (S ^^ (n - 1)) O S"
by (cases n, auto)
(*
* Equivalence relations.
*)
(* Convert a projection into an equivalence relation. *)
by (erule contrapos_nn, erule trancl_into_rtrancl)
lemma set_neqI:
"\<lbrakk> x \<in> S; x \<notin> S' \<rbrakk> \<Longrightarrow> S \<noteq> S'"
by clarsimp
lemma set_pair_UN:
"{x. P x} = UNION {xa. \<exists>xb. P (xa, xb)} (\<lambda>xa. {xa} \<times> {xb. P (xa, xb)})"
by fastforce
lemma singleton_elemD: "S = {x} \<Longrightarrow> x \<in> S"
by simp
lemma singleton_eqD: "A = {x} \<Longrightarrow> x \<in> A"
by blast
lemma ball_ran_fun_updI:
"\<lbrakk> \<forall>v \<in> ran m. P v; \<forall>v. y = Some v \<longrightarrow> P v \<rbrakk> \<Longrightarrow> \<forall>v \<in> ran (m (x := y)). P v"
by (auto simp add: ran_def)
lemma ball_ran_eq:
"(\<forall>y \<in> ran m. P y) = (\<forall>x y. m x = Some y \<longrightarrow> P y)"
by (auto simp add: ran_def)
lemma cart_helper:
"({} = {x} \<times> S) = (S = {})"
by blast
lemmas converse_trancl_induct' = converse_trancl_induct [consumes 1, case_names base step]
lemma disjCI2: "(\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q" by blast
lemma insert_UNIV :
"insert x UNIV = UNIV"
by blast
lemma not_singletonE:
"\<lbrakk> \<forall>p. S \<noteq> {p}; S \<noteq> {}; \<And>p p'. \<lbrakk> p \<noteq> p'; p \<in> S; p' \<in> S \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
by blast
lemma not_singleton_oneE:
"\<lbrakk> \<forall>p. S \<noteq> {p}; p \<in> S; \<And>p'. \<lbrakk> p \<noteq> p'; p' \<in> S \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
using not_singletonE by fastforce
lemma ball_ran_modify_map_eq:
"\<lbrakk> \<forall>v. m x = Some v \<longrightarrow> P (f v) = P v \<rbrakk>
\<Longrightarrow> (\<forall>v \<in> ran (modify_map m x f). P v) = (\<forall>v \<in> ran m. P v)"
"\<lbrakk> S = {x} \<rbrakk> \<Longrightarrow> x \<in> S"
by simp
lemma if_eq_elem_helperE:
"\<lbrakk> x \<in> (if P then S else S'); \<lbrakk> P; x \<in> S \<rbrakk> \<Longrightarrow> a = b; \<lbrakk> \<not> P; x \<in> S' \<rbrakk> \<Longrightarrow> a = c \<rbrakk>
\<Longrightarrow> a = (if P then b else c)"
by fastforce
lemma if_option_Some:
"((if P then None else Some x) = Some y) = (\<not>P \<and> x = y)"
by simp
lemma insert_minus_eq:
"x \<notin> A \<Longrightarrow> A - S = (A - (S - {x}))"
by auto
lemma modify_map_K_D:
"modify_map m p (\<lambda>x. y) p' = Some v \<Longrightarrow> (m (p \<mapsto> y)) p' = Some v"
by (simp add: modify_map_def split: split_if_asm)
lemma tranclE2:
assumes trancl: "(a, b) \<in> r\<^sup>+"
and base: "(a, b) \<in> r \<Longrightarrow> P"
and step: "\<And>c. \<lbrakk>(a, c) \<in> r; (c, b) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> P"
shows "P"
using trancl base step
proof -
note rl = converse_trancl_induct [where P = "\<lambda>x. x = a \<longrightarrow> P"]
from trancl have "a = a \<longrightarrow> P"
by (rule rl, (iprover intro: base step)+)
thus ?thesis by simp
qed
lemmas tranclE2' = tranclE2 [consumes 1, case_names base trancl]
lemma weak_imp_cong:
"\<lbrakk> P = R; Q = S \<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) = (R \<longrightarrow> S)"
by simp
lemma Collect_Diff_restrict_simp:
"T - {x \<in> T. Q x} = T - {x. Q x}"
by (auto intro: Collect_cong)
lemma Collect_Int_pred_eq:
"{x \<in> S. P x} \<inter> {x \<in> T. P x} = {x \<in> (S \<inter> T). P x}"
by (simp add: Collect_conj_eq [symmetric] conj_comms)
lemma Collect_restrict_predR:
"{x. P x} \<inter> T = {} \<Longrightarrow> {x. P x} \<inter> {x \<in> T. Q x} = {}"
by (fastforce simp: disjoint_iff_not_equal)
lemma Diff_Un2:
assumes emptyad: "A \<inter> D = {}"
and emptybc: "B \<inter> C = {}"
shows "(A \<union> B) - (C \<union> D) = (A - C) \<union> (B - D)"
proof -
have "(A \<union> B) - (C \<union> D) = (A \<union> B - C) \<inter> (A \<union> B - D)"
by (rule Diff_Un)
also have "\<dots> = ((A - C) \<union> B) \<inter> (A \<union> (B - D))" using emptyad emptybc
by (simp add: Un_Diff Diff_triv)
also have "\<dots> = (A - C) \<union> (B - D)"
proof -
have "(A - C) \<inter> (A \<union> (B - D)) = A - C" using emptyad emptybc
by (metis Diff_Int2 Diff_Int_distrib2 inf_sup_absorb)
moreover
have "B \<inter> (A \<union> (B - D)) = B - D" using emptyad emptybc
by (metis Int_Diff Un_Diff Un_Diff_Int Un_commute Un_empty_left inf_sup_absorb)
ultimately show ?thesis
by (simp add: Int_Un_distrib2)
qed
finally show ?thesis .
qed
lemma ballEI:
"\<lbrakk> \<forall>x \<in> S. Q x; \<And>x. \<lbrakk> x \<in> S; Q x \<rbrakk> \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> \<forall>x \<in> S. P x"
by auto
lemma dom_if_None:
"dom (\<lambda>x. if P x then None else f x) = dom f - {x. P x}"
by (simp add: dom_def) fastforce
lemma restrict_map_Some_iff:
"((m |` S) x = Some y) = (m x = Some y \<and> x \<in> S)"
by (cases "x \<in> S", simp_all)
lemma context_case_bools:
"\<lbrakk> \<And>v. P v \<Longrightarrow> R v; \<lbrakk> \<not> P v; \<And>v. P v \<Longrightarrow> R v \<rbrakk> \<Longrightarrow> R v \<rbrakk> \<Longrightarrow> R v"
by (cases "P v", simp_all)
lemma inj_on_fun_upd_strongerI:
"\<lbrakk>inj_on f A; y \<notin> f ` (A - {x})\<rbrakk> \<Longrightarrow> inj_on (f(x := y)) A"
by (fastforce simp: inj_on_def)
lemma less_handy_casesE:
"\<lbrakk> m < n; m = 0 \<Longrightarrow> R; \<And>m' n'. \<lbrakk> n = Suc n'; m = Suc m'; m < n \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
by (case_tac n; simp) (case_tac m; simp)
lemma subset_drop_Diff_strg:
"(A \<subseteq> C) \<longrightarrow> (A - B \<subseteq> C)"
by blast
lemma inj_case_bool:
"inj (case_bool a b) = (a \<noteq> b)"
by (auto dest: inj_onD[where x=True and y=False] intro: inj_onI split: bool.split_asm)
lemma foldl_fun_upd:
"foldl (\<lambda>s r. s (r := g r)) f rs = (\<lambda>x. if x \<in> set rs then g x else f x)"
by (induct rs arbitrary: f) (auto simp: fun_eq_iff)
lemma all_rv_choice_fn_eq_pred:
"\<lbrakk> \<And>rv. P rv \<Longrightarrow> \<exists>fn. f rv = g fn \<rbrakk> \<Longrightarrow> \<exists>fn. \<forall>rv. P rv \<longrightarrow> f rv = g (fn rv)"
apply (rule_tac x="\<lambda>rv. SOME h. f rv = g h" in exI)
"\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z > y. P (z :: 'a :: linorder) \<rbrakk> \<Longrightarrow> \<forall>z > x. P z"
using not_le by blast
lemma range_convergence2:
"\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> P z; \<forall>z. z > y \<and> z < w \<longrightarrow> P (z :: 'a :: linorder) \<rbrakk>
\<Longrightarrow> \<forall>z. z > x \<and> z < w \<longrightarrow> P z"
using range_convergence1[where P="\<lambda>z. z < w \<longrightarrow> P z" and x=x and y=y]
by auto
lemma zip_upt_Cons:
"a < b \<Longrightarrow> zip [a ..< b] (x # xs) = (a, x) # zip [Suc a ..< b] xs"
by (simp add: upt_conv_Cons)
lemma map_comp_eq:
"f \<circ>\<^sub>m g = case_option None f \<circ> g"
apply (rule ext)
apply (case_tac "g x")
by auto
lemma dom_If_Some:
"dom (\<lambda>x. if x \<in> S then Some v else f x) = (S \<union> dom f)"
by (auto split: split_if)
lemma foldl_fun_upd_const:
"foldl (\<lambda>s x. s(f x := v)) s xs
= (\<lambda>x. if x \<in> f ` set xs then v else s x)"
by (induct xs arbitrary: s) auto
lemma foldl_id:
"foldl (\<lambda>s x. s) s xs = s"
by (induct xs) auto
lemma SucSucMinus: "2 \<le> n \<Longrightarrow> Suc (Suc (n - 2)) = n" by arith
lemma ball_to_all:
"(\<And>x. (x \<in> A) = (P x)) \<Longrightarrow> (\<forall>x \<in> A. B x) = (\<forall>x. P x \<longrightarrow> B x)"
by blast
lemma case_option_If:
"case_option P (\<lambda>x. Q) v = (if v = None then P else Q)"
by clarsimp
lemma case_option_If2:
"case_option P Q v = If (v \<noteq> None) (Q (the v)) P"
by (simp split: option.split)
lemma if3_fold:
"(if P then x else if Q then y else x) = (if P \<or> \<not> Q then x else y)"
by simp
lemma rtrancl_insert:
assumes x_new: "\<And>y. (x,y) \<notin> R"
shows "R^* `` insert x S = insert x (R^* `` S)"
proof -
have "R^* `` insert x S = R^* `` ({x} \<union> S)" by simp
"distinct xs \<Longrightarrow> filter (\<lambda>v. v = x) xs = (if x \<in> set xs then [x] else [])"
by (induct xs) auto
lemma (in semigroup_add) foldl_assoc:
shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
by (induct zs arbitrary: y) (simp_all add:add.assoc)
lemma (in monoid_add) foldl_absorb0:
shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
by (induct zs) (simp_all add:foldl_assoc)
lemma foldl_conv_concat:
"foldl (op @) xs xss = xs @ concat xss"
proof (induct xss arbitrary: xs)
case Nil show ?case by simp
next
interpret monoid_add "op @" "[]" proof qed simp_all
case Cons then show ?case by (simp add: foldl_absorb0)
qed
lemma foldl_concat_concat:
"foldl op @ [] (xs @ ys) = foldl op @ [] xs @ foldl op @ [] ys"
by (simp add: foldl_conv_concat)
lemma foldl_does_nothing:
"\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f s x = s \<rbrakk> \<Longrightarrow> foldl f s xs = s"
by (induct xs) auto
lemma foldl_use_filter:
"\<lbrakk> \<And>v x. \<lbrakk> \<not> g x; x \<in> set xs \<rbrakk> \<Longrightarrow> f v x = v \<rbrakk> \<Longrightarrow> foldl f v xs = foldl f v (filter g xs)"