(* Author: Alexander Maletzky *) section ‹Utilities› theory Utils imports Main Well_Quasi_Orders.Almost_Full_Relations begin lemma subset_imageE_inj: assumes "B ⊆ f ` A" obtains C where "C ⊆ A" and "B = f ` C" and "inj_on f C" proof - define g where "g = (λx. SOME a. a ∈ A ∧ f a = x)" have "g b ∈ A ∧ f (g b) = b" if "b ∈ B" for b proof - from that assms have "b ∈ f ` A" .. then obtain a where "a ∈ A" and "b = f a" .. hence "a ∈ A ∧ f a = b" by simp thus ?thesis unfolding g_def by (rule someI) qed hence 1: "⋀b. b ∈ B ⟹ g b ∈ A" and 2: "⋀b. b ∈ B ⟹ f (g b) = b" by simp_all let ?C = "g ` B" show ?thesis proof show "?C ⊆ A" by (auto intro: 1) next show "B = f ` ?C" proof (rule set_eqI) fix b show "b ∈ B ⟷ b ∈ f ` ?C" proof assume "b ∈ B" moreover from this have "f (g b) = b" by (rule 2) ultimately show "b ∈ f ` ?C" by force next assume "b ∈ f ` ?C" then obtain b' where "b' ∈ B" and "b = f (g b')" unfolding image_image .. moreover from this(1) have "f (g b') = b'" by (rule 2) ultimately show "b ∈ B" by simp qed qed next show "inj_on f ?C" proof fix x y assume "x ∈ ?C" then obtain bx where "bx ∈ B" and x: "x = g bx" .. moreover from this(1) have "f (g bx) = bx" by (rule 2) ultimately have *: "f x = bx" by simp assume "y ∈ ?C" then obtain "by" where "by ∈ B" and y: "y = g by" .. moreover from this(1) have "f (g by) = by" by (rule 2) ultimately have "f y = by" by simp moreover assume "f x = f y" ultimately have "bx = by" using * by simp thus "x = y" by (simp only: x y) qed qed qed lemma wfP_chain: assumes "¬(∃f. ∀i. r (f (Suc i)) (f i))" shows "wfP r" proof - from assms wf_iff_no_infinite_down_chain[of "{(x, y). r x y}"] have "wf {(x, y). r x y}" by auto thus "wfP r" unfolding wfp_def . qed lemma transp_sequence: assumes "transp r" and "⋀i. r (seq (Suc i)) (seq i)" and "i < j" shows "r (seq j) (seq i)" proof - have "⋀k. r (seq (i + Suc k)) (seq i)" proof - fix k::nat show "r (seq (i + Suc k)) (seq i)" proof (induct k) case 0 from assms(2) have "r (seq (Suc i)) (seq i)" . thus ?case by simp next case (Suc k) note assms(1) moreover from assms(2) have "r (seq (Suc (Suc i + k))) (seq (Suc (i + k)))" by simp moreover have "r (seq (Suc (i + k))) (seq i)" using Suc.hyps by simp ultimately have "r (seq (Suc (Suc i + k))) (seq i)" by (rule transpD) thus ?case by simp qed qed hence "r (seq (i + Suc(j - i - 1))) (seq i)" . thus "r (seq j) (seq i)" using ‹i < j› by simp qed lemma almost_full_on_finite_subsetE: assumes "reflp P" and "almost_full_on P S" obtains T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. P t s)" proof - define crit where "crit = (λU s. s ∈ S ∧ (∀u∈U. ¬ P u s))" have critD: "s ∉ U" if "crit U s" for U s proof assume "s ∈ U" from ‹crit U s› have "∀u∈U. ¬ P u s" unfolding crit_def .. from this ‹s ∈ U› have "¬ P s s" .. moreover from assms(1) have "P s s" by (rule reflpD) ultimately show False .. qed define "fun" where "fun = (λU. (if (∃s. crit U s) then insert (SOME s. crit U s) U else U ))" define seq where "seq = rec_nat {} (λ_. fun)" have seq_Suc: "seq (Suc i) = fun (seq i)" for i by (simp add: seq_def) have seq_incr_Suc: "seq i ⊆ seq (Suc i)" for i by (auto simp add: seq_Suc fun_def) have seq_incr: "i ≤ j ⟹ seq i ⊆ seq j" for i j proof - assume "i ≤ j" hence "i = j ∨ i < j" by auto thus "seq i ⊆ seq j" proof assume "i = j" thus ?thesis by simp next assume "i < j" with _ seq_incr_Suc show ?thesis by (rule transp_sequence, simp add: transp_def) qed qed have sub: "seq i ⊆ S" for i proof (induct i, simp add: seq_def, simp add: seq_Suc fun_def, rule) fix i assume "Ex (crit (seq i))" hence "crit (seq i) (Eps (crit (seq i)))" by (rule someI_ex) thus "Eps (crit (seq i)) ∈ S" by (simp add: crit_def) qed have "∃i. seq (Suc i) = seq i" proof (rule ccontr, simp) assume "∀i. seq (Suc i) ≠ seq i" with seq_incr_Suc have "seq i ⊂ seq (Suc i)" for i by blast define seq1 where "seq1 = (λn. (SOME s. s ∈ seq (Suc n) ∧ s ∉ seq n))" have seq1: "seq1 n ∈ seq (Suc n) ∧ seq1 n ∉ seq n" for n unfolding seq1_def proof (rule someI_ex) from ‹seq n ⊂ seq (Suc n)› show "∃x. x ∈ seq (Suc n) ∧ x ∉ seq n" by blast qed have "seq1 i ∈ S" for i proof from seq1[of i] show "seq1 i ∈ seq (Suc i)" .. qed (fact sub) with assms(2) obtain a b where "a < b" and "P (seq1 a) (seq1 b)" by (rule almost_full_onD) from ‹a < b› have "Suc a ≤ b" by simp from seq1 have "seq1 a ∈ seq (Suc a)" .. also from ‹Suc a ≤ b› have "... ⊆ seq b" by (rule seq_incr) finally have "seq1 a ∈ seq b" . from seq1 have "seq1 b ∈ seq (Suc b)" and "seq1 b ∉ seq b" by blast+ hence "crit (seq b) (seq1 b)" by (simp add: seq_Suc fun_def someI split: if_splits) hence "∀u∈seq b. ¬ P u (seq1 b)" by (simp add: crit_def) from this ‹seq1 a ∈ seq b› have "¬ P (seq1 a) (seq1 b)" .. from this ‹P (seq1 a) (seq1 b)› show False .. qed then obtain i where "seq (Suc i) = seq i" .. show ?thesis proof show "finite (seq i)" by (induct i, simp_all add: seq_def fun_def) next fix s assume "s ∈ S" let ?s = "Eps (crit (seq i))" show "∃t∈seq i. P t s" proof (rule ccontr, simp) assume "∀t∈seq i. ¬ P t s" with ‹s ∈ S› have "crit (seq i) s" by (simp only: crit_def) hence "crit (seq i) ?s" and eq: "seq (Suc i) = insert ?s (seq i)" by (auto simp add: seq_Suc fun_def intro: someI) from this(1) have "?s ∉ seq i" by (rule critD) hence "seq (Suc i) ≠ seq i" unfolding eq by blast from this ‹seq (Suc i) = seq i› show False .. qed qed (fact sub) qed subsection ‹Lists› lemma map_upt: "map (λi. f (xs ! i)) [0..<length xs] = map f xs" by (auto intro: nth_equalityI) lemma map_upt_zip: assumes "length xs = length ys" shows "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] = map (λ(x, y). f x y) (zip xs ys)" (is "?l = ?r") proof - have len_l: "length ?l = length ys" by simp from assms have len_r: "length ?r = length ys" by simp show ?thesis proof (simp only: list_eq_iff_nth_eq len_l len_r, rule, rule, intro allI impI) fix i assume "i < length ys" hence "i < length ?l" and "i < length ?r" by (simp_all only: len_l len_r) thus "map (λi. f (xs ! i) (ys ! i)) [0..<length ys] ! i = map (λ(x, y). f x y) (zip xs ys) ! i" by simp qed qed lemma distinct_sorted_wrt_irrefl: assumes "irreflp rel" and "transp rel" and "sorted_wrt rel xs" shows "distinct xs" using assms(3) proof (induct xs) case Nil show ?case by simp next case (Cons x xs) from Cons(2) have "sorted_wrt rel xs" and *: "∀y∈set xs. rel x y" by (simp_all) from this(1) have "distinct xs" by (rule Cons(1)) show ?case proof (simp add: ‹distinct xs›, rule) assume "x ∈ set xs" with * have "rel x x" .. with assms(1) show False by (simp add: irreflp_def) qed qed lemma distinct_sorted_wrt_imp_sorted_wrt_strict: assumes "distinct xs" and "sorted_wrt rel xs" shows "sorted_wrt (λx y. rel x y ∧ ¬ x = y) xs" using assms proof (induct xs) case Nil show ?case by simp next case step: (Cons x xs) show ?case proof (cases "xs") case Nil thus ?thesis by simp next case (Cons y zs) from step(2) have "x ≠ y" and 1: "distinct (y # zs)" by (simp_all add: Cons) from step(3) have "rel x y" and 2: "sorted_wrt rel (y # zs)" by (simp_all add: Cons) from 1 2 have "sorted_wrt (λx y. rel x y ∧ x ≠ y) (y # zs)" by (rule step(1)[simplified Cons]) with ‹x ≠ y› ‹rel x y› show ?thesis using step.prems by (auto simp: Cons) qed qed lemma sorted_wrt_distinct_set_unique: assumes "antisymp rel" assumes "sorted_wrt rel xs" "distinct xs" "sorted_wrt rel ys" "distinct ys" "set xs = set ys" shows "xs = ys" proof - from assms have 1: "length xs = length ys" by (auto dest!: distinct_card) from assms(2-6) show ?thesis proof(induct rule:list_induct2[OF 1]) case 1 show ?case by simp next case (2 x xs y ys) from 2(4) have "x ∉ set xs" and "distinct xs" by simp_all from 2(6) have "y ∉ set ys" and "distinct ys" by simp_all have "x = y" proof (rule ccontr) assume "x ≠ y" from 2(3) have "∀z∈set xs. rel x z" by (simp) moreover from ‹x ≠ y› have "y ∈ set xs" using 2(7) by auto ultimately have *: "rel x y" .. from 2(5) have "∀z∈set ys. rel y z" by (simp) moreover from ‹x ≠ y› have "x ∈ set ys" using 2(7) by auto ultimately have "rel y x" .. with assms(1) * have "x = y" by (rule antisympD) with ‹x ≠ y› show False .. qed from 2(3) have "sorted_wrt rel xs" by (simp) moreover note ‹distinct xs› moreover from 2(5) have "sorted_wrt rel ys" by (simp) moreover note ‹distinct ys› moreover from 2(7) ‹x ∉ set xs› ‹y ∉ set ys› have "set xs = set ys" by (auto simp add: ‹x = y›) ultimately have "xs = ys" by (rule 2(2)) with ‹x = y› show ?case by simp qed qed lemma sorted_wrt_refl_nth_mono: assumes "reflp P" and "sorted_wrt P xs" and "i ≤ j" and "j < length xs" shows "P (xs ! i) (xs ! j)" proof (cases "i < j") case True from assms(2) this assms(4) show ?thesis by (rule sorted_wrt_nth_less) next case False with assms(3) have "i = j" by simp from assms(1) show ?thesis unfolding ‹i = j› by (rule reflpD) qed fun merge_wrt :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ 'a list" where "merge_wrt _ xs [] = xs"| "merge_wrt rel [] ys = ys"| "merge_wrt rel (x # xs) (y # ys) = (if x = y then y # (merge_wrt rel xs ys) else if rel x y then x # (merge_wrt rel xs (y # ys)) else y # (merge_wrt rel (x # xs) ys) )" lemma set_merge_wrt: "set (merge_wrt rel xs ys) = set xs ∪ set ys" proof (induct rel xs ys rule: merge_wrt.induct) case (1 rel xs) show ?case by simp next case (2 rel y ys) show ?case by simp next case (3 rel x xs y ys) show ?case proof (cases "x = y") case True thus ?thesis by (simp add: 3(1)) next case False show ?thesis proof (cases "rel x y") case True with ‹x ≠ y› show ?thesis by (simp add: 3(2) insert_commute) next case False with ‹x ≠ y› show ?thesis by (simp add: 3(3)) qed qed qed lemma sorted_merge_wrt: assumes "transp rel" and "⋀x y. x ≠ y ⟹ rel x y ∨ rel y x" and "sorted_wrt rel xs" and "sorted_wrt rel ys" shows "sorted_wrt rel (merge_wrt rel xs ys)" using assms proof (induct rel xs ys rule: merge_wrt.induct) case (1 rel xs) from 1(3) show ?case by simp next case (2 rel y ys) from 2(4) show ?case by simp next case (3 rel x xs y ys) show ?case proof (cases "x = y") case True show ?thesis proof (auto simp add: True) fix z assume "z ∈ set (merge_wrt rel xs ys)" hence "z ∈ set xs ∪ set ys" by (simp only: set_merge_wrt) thus "rel y z" proof assume "z ∈ set xs" with 3(6) show ?thesis by (simp add: True) next assume "z ∈ set ys" with 3(7) show ?thesis by (simp) qed next note True 3(4, 5) moreover from 3(6) have "sorted_wrt rel xs" by (simp) moreover from 3(7) have "sorted_wrt rel ys" by (simp) ultimately show "sorted_wrt rel (merge_wrt rel xs ys)" by (rule 3(1)) qed next case False show ?thesis proof (cases "rel x y") case True show ?thesis proof (auto simp add: False True) fix z assume "z ∈ set (merge_wrt rel xs (y # ys))" hence "z ∈ insert y (set xs ∪ set ys)" by (simp add: set_merge_wrt) thus "rel x z" proof assume "z = y" with True show ?thesis by simp next assume "z ∈ set xs ∪ set ys" thus ?thesis proof assume "z ∈ set xs" with 3(6) show ?thesis by (simp) next assume "z ∈ set ys" with 3(7) have "rel y z" by (simp) with 3(4) True show ?thesis by (rule transpD) qed qed next note False True 3(4, 5) moreover from 3(6) have "sorted_wrt rel xs" by (simp) ultimately show "sorted_wrt rel (merge_wrt rel xs (y # ys))" using 3(7) by (rule 3(2)) qed next assume "¬ rel x y" from ‹x ≠ y› have "rel x y ∨ rel y x" by (rule 3(5)) with ‹¬ rel x y› have *: "rel y x" by simp show ?thesis proof (auto simp add: False ‹¬ rel x y›) fix z assume "z ∈ set (merge_wrt rel (x # xs) ys)" hence "z ∈ insert x (set xs ∪ set ys)" by (simp add: set_merge_wrt) thus "rel y z" proof assume "z = x" with * show ?thesis by simp next assume "z ∈ set xs ∪ set ys" thus ?thesis proof assume "z ∈ set xs" with 3(6) have "rel x z" by (simp) with 3(4) * show ?thesis by (rule transpD) next assume "z ∈ set ys" with 3(7) show ?thesis by (simp) qed qed next note False ‹¬ rel x y› 3(4, 5, 6) moreover from 3(7) have "sorted_wrt rel ys" by (simp) ultimately show "sorted_wrt rel (merge_wrt rel (x # xs) ys)" by (rule 3(3)) qed qed qed qed lemma set_fold: assumes "⋀x ys. set (f (g x) ys) = set (g x) ∪ set ys" shows "set (fold (λx. f (g x)) xs ys) = (⋃x∈set xs. set (g x)) ∪ set ys" proof (induct xs arbitrary: ys) case Nil show ?case by simp next case (Cons x xs) have eq: "set (fold (λx. f (g x)) xs (f (g x) ys)) = (⋃x∈set xs. set (g x)) ∪ set (f (g x) ys)" by (rule Cons) show ?case by (simp add: o_def assms set_merge_wrt eq ac_simps) qed subsection ‹Sums and Products› lemma additive_implies_homogenous: assumes "⋀x y. f (x + y) = f x + ((f (y::'a::monoid_add))::'b::cancel_comm_monoid_add)" shows "f 0 = 0" proof - have "f (0 + 0) = f 0 + f 0" by (rule assms) hence "f 0 = f 0 + f 0" by simp thus "f 0 = 0" by simp qed lemma fun_sum_commute: assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y" shows "f (sum g A) = (∑a∈A. f (g a))" proof (cases "finite A") case True thus ?thesis proof (induct A) case empty thus ?case by (simp add: assms(1)) next case step: (insert a A) show ?case by (simp add: sum.insert[OF step(1) step(2)] assms(2) step(3)) qed next case False thus ?thesis by (simp add: assms(1)) qed lemma fun_sum_commute_canc: assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)" shows "f (sum g A) = (∑a∈A. f (g a))" by (rule fun_sum_commute, rule additive_implies_homogenous, fact+) lemma fun_sum_list_commute: assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y" shows "f (sum_list xs) = sum_list (map f xs)" proof (induct xs) case Nil thus ?case by (simp add: assms(1)) next case (Cons x xs) thus ?case by (simp add: assms(2)) qed lemma fun_sum_list_commute_canc: assumes "⋀x y. f (x + y) = f x + ((f y)::'a::cancel_comm_monoid_add)" shows "f (sum_list xs) = sum_list (map f xs)" by (rule fun_sum_list_commute, rule additive_implies_homogenous, fact+) lemma sum_set_upt_eq_sum_list: "(∑i = m..<n. f i) = (∑i←[m..<n]. f i)" using sum_set_upt_conv_sum_list_nat by auto lemma sum_list_upt: "(∑i←[0..<(length xs)]. f (xs ! i)) = (∑x←xs. f x)" by (simp only: map_upt) lemma sum_list_upt_zip: assumes "length xs = length ys" shows "(∑i←[0..<(length ys)]. f (xs ! i) (ys ! i)) = (∑(x, y)←(zip xs ys). f x y)" by (simp only: map_upt_zip[OF assms]) lemma sum_list_zeroI: assumes "set xs ⊆ {0}" shows "sum_list xs = 0" using assms by (induct xs, auto) lemma fun_prod_commute: assumes "f 1 = 1" and "⋀x y. f (x * y) = f x * f y" shows "f (prod g A) = (∏a∈A. f (g a))" proof (cases "finite A") case True thus ?thesis proof (induct A) case empty thus ?case by (simp add: assms(1)) next case step: (insert a A) show ?case by (simp add: prod.insert[OF step(1) step(2)] assms(2) step(3)) qed next case False thus ?thesis by (simp add: assms(1)) qed end (* theory *)