Theory Trivia

(*<*)
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
(*>*)