(*<*) theory Trivia imports Main "HOL-Library.Sublist" begin lemma measure_induct2[case_names IH]: fixes meas :: "'a ⇒ 'b ⇒ nat" assumes "⋀x1 x2. (⋀y1 y2. meas y1 y2 < meas x1 x2 ⟹ S y1 y2) ⟹ S x1 x2" shows "S x1 x2" proof- let ?m = "λ x1x2. meas (fst x1x2) (snd x1x2)" let ?S = "λ x1x2. S (fst x1x2) (snd x1x2)" have "?S (x1,x2)" apply(rule measure_induct[of ?m ?S]) using assms by (metis fst_conv snd_conv) thus ?thesis by auto qed text‹Right cons:› abbreviation Rcons (infix ‹##› 70) where "xs ## x ≡ xs @ [x]" lemma two_singl_Rcons: "[a,b] = [a] ## b" by auto lemma length_gt_1_Cons_snoc: assumes "length ys > 1" obtains x1 xs x2 where "ys = x1 # xs ## x2" using assms proof (cases ys) case (Cons x1 xs) with assms obtain xs' x2 where "xs = xs' ## x2" by (cases xs rule: rev_cases) auto with Cons show thesis by (intro that) auto qed auto abbreviation lmember (‹(_/ ∈∈ _)› [50, 51] 50) where "x ∈∈ xs ≡ x ∈ set xs" lemma right_cons_left[simp]: "i < length as ⟹ (as ## a)!i = as!i" by (metis butlast_snoc nth_butlast)+ definition "update2 f x y a ≡ λ x' y'. if x = x' ∧ y = y' then a else f x' y'" fun fst3 where "fst3 (a,b,c) = a" fun snd3 where "snd3 (a,b,c) = b" fun trd3 where "trd3 (a,b,c) = c" lemma subliteq_induct[consumes 1, case_names Nil Cons1 Cons2, induct pred: subseq]: assumes 0: "subseq xs ys" and Nil: "⋀ ys. φ [] ys" and Cons1: "⋀ xs ys y. ⟦subseq xs ys; φ xs ys⟧ ⟹ φ xs (y#ys)" and Cons2: "⋀ xs ys x. ⟦subseq xs ys; φ xs ys⟧ ⟹ φ (x#xs) (x#ys)" shows "φ xs ys" using assms by (induct) auto lemma append_ex_unique_list_ex: assumes e: "∃!i. i < length as ∧ pred (as!i)" and as: "as = as1 @ [a] @ as2" and pred: "pred a" shows "¬ list_ex pred as1 ∧ ¬ list_ex pred as2" proof let ?i = "length as1" have a: "a = as!?i" using as by auto have i: "?i < length as" using as by auto {fix j assume jl: "j < length as1" and pj: "pred (as1!j)" hence "pred (as!j)" apply(subst as) by (metis nth_append) moreover have "?i ≠ j" and "j < length as" using jl as by auto ultimately have False using e pred[unfolded a] i by blast } thus "¬ list_ex pred as1" unfolding list_ex_length by auto {fix j assume jl: "j < length as2" and pj: "pred (as2!j)" define k where "k ≡ Suc (length as1) + j" have "pred (as!k)" unfolding k_def apply(subst as) using pj nth_append[of "as1 @ [a]" as2] by simp moreover have "?i ≠ k" and "k < length as" using jl as unfolding k_def by auto ultimately have False using e pred[unfolded a] i by blast } thus "¬ list_ex pred as2" unfolding list_ex_length by auto qed lemma list_ex_find: assumes "list_ex P xs" shows "List.find P xs ≠ None" using assms by (induct xs) auto lemma list_all_map: "list_all (h o i) l ⟷ list_all h (map i l)" by (induction l) auto lemma list_ex_list_all_inj: assumes "list_ex (Q u) l" and "list_all (Q v) l" and "⋀ u v x. Q u x ⟹ Q v x ⟹ u = v" shows "u = v" using assms by (induction l) auto definition fun_upd2 where "fun_upd2 f a b c ≡ λ a' b'. if a = a' ∧ b = b' then c else f a' b'" lemma fun_upd2_eq_but_a_b: assumes "a' ≠ a ∨ b' ≠ b" shows "(fun_upd2 f a b c) a' b' = f a' b'" using assms unfolding fun_upd2_def by auto lemma fun_upd2_comm: assumes "a' = a ∧ b' = b ⟶ c' = c" shows "fun_upd2 (fun_upd2 f a b c) a' b' c' = fun_upd2 (fun_upd2 f a' b' c') a b c" using assms unfolding fun_upd2_def by (intro ext) auto lemma fun_upd2_absorb: shows "fun_upd2 (fun_upd2 f a b c) a b c' = fun_upd2 f a b c'" unfolding fun_upd2_def by (intro ext) auto definition "zip3 as bs cs ≡ zip as (zip bs cs)" definition "zip4 as bs cs ds ≡ zip as (zip bs (zip cs ds))" lemma set_map_fst: "set as ⊆ set bs ⟹ set (map fst as) ⊆ set (map fst bs)" by auto lemma set_map_snd: "set as ⊆ set bs ⟹ set (map snd as) ⊆ set (map snd bs)" by auto lemma filter_cong_empty: assumes "∀ x. ¬ pred1 x ∧ ¬ pred2 x" shows "filter pred1 xl1 = filter pred2 xl2" using assms by auto (*****************) abbreviation "cmap ff aal ≡ concat (map ff aal)" lemma cmap_empty: assumes "∀ x. x ∈∈ xl ⟶ ff x = []" shows "cmap ff xl = []" using assms by (induct xl) auto lemma cmap_cong_empty: assumes "∀ x. ff x = [] ∧ gg x = []" shows "cmap ff xl = cmap gg yl" using assms by (auto simp: cmap_empty) lemma list_ex_cmap: "list_ex P (cmap f xs) ⟷ (∃ x. x ∈∈ xs ∧ list_ex P (f x))" by (induction xs) auto lemma not_list_ex_filter: assumes "¬ list_ex P xs" shows "filter P xs = []" using assms by (induct xs) auto lemma cmap_filter_cong: assumes "⋀ x u. x ∈∈ xs ⟹ u ∈∈ ff x ⟹ (q x ⟷ p u)" and "⋀ x. x ∈∈ xs ⟹ q x ⟹ gg x = ff x" shows "cmap ((filter p) o ff) xs = cmap gg (filter q xs)" using assms by (induction xs) fastforce+ lemma cmap_cong: assumes "xs = ys" and "⋀x. x ∈∈ xs ⟹ ff x = gg x" shows "cmap ff xs = cmap gg ys" using assms by (induction xs arbitrary: ys) auto lemma cmap_empty_singl_filter[simp]: "cmap (λx. if pred x then [x] else []) xl = filter pred xl" by (induct xl) auto lemma cmap_insort_empty: assumes "ff x = []" shows "cmap ff (insort_key f x xs) = cmap ff xs" using assms by (induction xs) auto lemma cmap_insort_empty_cong: assumes "xs = ys" and "⋀x. x ∈∈ xs ⟹ ff x = gg x" and x: "ff x = []" shows "cmap ff (insort_key f x xs) = cmap gg ys" using assms by (auto intro: cmap_cong simp: cmap_insort_empty) abbreviation never :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where "never U ≡ list_all (λ a. ¬ U a)" lemma never_list_ex: "never pred tr ⟷ ¬ list_ex pred tr" by (induction tr) auto lemma notNil_list_all_list_ex: assumes "xs ≠ Nil" and "list_all pred xs" shows "list_ex pred xs" using assms by (induct xs) auto fun remove1ByFirst :: "'a ⇒ ('a × 'b) list ⇒ ('a × 'b) list" where "remove1ByFirst a [] = []" | "remove1ByFirst a ((a1,b1) # a_bs) = (if a = a1 then a_bs else (a1,b1) # (remove1ByFirst a a_bs))" (* "insert2 a b ab_s" searches in the list of pairs ab_s for a the first component a and replaces the second component with b; if no match is found, (a,b) is added at the end. It's similar to a function update applied to a list of pairs, with adding if missing. *) definition "insert2 a b ab_s ≡ if a ∈∈ map fst ab_s then map (λ (a',b'). if a' = a then (a',b) else (a',b')) ab_s else ab_s ## (a,b)" lemma test_insert2: "insert2 (1::nat) (2::nat) [(2,3),(1,5)] = [(2,3),(1,2)]" "insert2 (1::nat) (2::nat) [(2,3),(4,5)] = [(2,3),(4,5),(1,2)]" unfolding insert2_def by simp_all lemma map_prod_cong: "map (fst o f) xys = map (fst o f2) xys' ⟹ map (snd o f) xys = map (snd o f2) xys' ⟹ map f xys = map f2 xys'" by (simp add: pair_list_eqI) lemma map_const_eq: "length xs = length xs' ⟹ map (λ x. a) xs = map (λ x. a) xs'" by (simp add: map_replicate_const) fun these :: "'a option list ⇒ 'a list" where "these [] = []" | "these (None # xs) = these xs" | "these (Some x # xs) = x # these xs" lemma [simp]: "these (map Some xs) = xs" by (induction xs) auto lemma these_map_Some[simp]: "these (map (Some o f) xs) = map f xs" by (induction xs) auto end (*>*)