Theory Preliminaries

section "Preliminaries"

theory Preliminaries
  imports Complex_Main 
    "List-Index.List_Index"
    "HOL-Library.AList"
    "HOL-Library.Sublist"
    "HOL-Eisbach.Eisbach" 
    "HOL-Library.Simps_Case_Conv"
begin

text ‹Stuff about options›

fun the_default :: "'a ⇒ 'a option ⇒ 'a" where
  "the_default a None = a"
| "the_default _ (Some b) = b"

abbreviation Or :: "'a option ⇒ 'a option ⇒ 'a option" (infixl ‹OR› 60) where
  "e1 OR e2 ≡ case e1 of None ⇒ e2 | p ⇒ p"

lemma Or_Some: "(e1 OR e2) = Some x ⟷ e1 = Some x ∨ (e1 = None ∧ e2 = Some x)"
  by(auto split: option.split)

lemma Or_None: "(e1 OR e2) = None ⟷ e1 = None ∧ e2 = None"
  by(auto split: option.split)

fun lift2_option :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a option ⇒ 'b option ⇒ 'c option" where
  "lift2_option _ None _ = None" |
  "lift2_option _ _ None = None" |
  "lift2_option f (Some x) (Some y) = Some (f x y)"

lemma lift2_option_not_None: "lift2_option f x y ≠ None ⟷ (x ≠ None ∧ y ≠ None)" 
  using lift2_option.elims by blast
lemma lift2_option_None: "lift2_option f x y = None ⟷ (x = None ∨ y = None)" 
  using lift2_option.elims by blast

text ‹Lookup functions for assoc lists›

fun find :: "('a ⇒ 'b option) ⇒ 'a list ⇒ 'b option" where
"find f [] = None" |
"find f (x#xs) = f x OR find f xs"

lemma findD:
  "find f xs = Some p ⟹ ∃x ∈ set xs. f x = Some p"
  by(induction xs arbitrary: p) (auto split: option.splits)

lemma find_None:
  "find f xs = None ⟷ (∀x ∈ set xs. f x = None)"
  by(induction xs) (auto split: option.splits)

lemma find_ListFind: "find f l = Option.bind (List.find (λx. case f x of None ⇒ False | _ ⇒ True) l) f" 
  by (induction l) (auto split: option.split)
     
lemma "List.find P l = Some p ⟹ ∃p ∈ set l . P p"
  by (induction l) (auto split: if_splits)

lemma find_the_pair:
  assumes "distinct (map fst pairs)" 
    and "⋀x y. x∈set (map fst pairs) ⟹ y∈set (map fst pairs) ⟹ P x ⟹ P y ⟹ x = y"
    and "(x,y) ∈ set pairs" and "P x" 
  shows "List.find (λ(x,_) . P x) pairs = Some (x,y)"
  using assms(1-3)
proof (induction pairs)
  case Nil
  then show ?case by simp
next
  case (Cons pair pairs)
  thm Cons.prems

  show ?case
  proof(cases "fst pair = x")
    case True
    then show ?thesis
      using eq_key_imp_eq_value[OF Cons.prems(1,3)] assms(4) by force
  next
    case False
    hence "(x,y) ∈ set pairs"
      using Cons.prems(3) by fastforce
    moreover have "⋀x y. x ∈ set (map fst pairs) ⟹ y ∈ set (map fst pairs) ⟹ P x ⟹ P y ⟹ x = y"
      using Cons.prems(2) by (metis list.set_intros(2) list.simps(9))
    ultimately have I: "List.find (λ(x,_) . P x) pairs = Some (x,y)"
      using Cons.prems(1,3) by (auto intro!: Cons.IH)
    moreover have "⋀y. y ∈ set (map fst (pair # pairs)) ⟹ P y ⟹ x = y"
      using Cons.prems(2,3) assms(4) by (metis set_zip_leftD zip_map_fst_snd)
    ultimately show ?thesis
      using False by fastforce
  qed
qed

fun remdups_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
  "remdups_on  _ [] = []" 
| "remdups_on cmp (x # xs) = 
    (if ∃x' ∈ set xs . cmp x x' then remdups_on cmp xs else x # remdups_on cmp xs)"

fun distinct_on :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "distinct_on _ [] ⟷ True"
| "distinct_on cmp (x # xs) ⟷ ¬(∃x' ∈ set xs . cmp x x') ∧ distinct_on cmp xs"

lemma "remdups_on (=) xs = remdups xs"
  by (induction xs) auto

lemma remdups_on_antimono:
  "(⋀x y . f x y ⟹ g x y) ⟹ set (remdups_on g xs) ⊆ set (remdups_on f xs)"
  by (induction xs) auto

lemma remdups_on_subset_input: "set (remdups_on f xs) ⊆ set xs"
  by (induction xs) auto

lemma distinct_on_remdups_on: "distinct_on f (remdups_on f xs)" 
proof (induction xs)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs)
  then show ?case 
    using remdups_on_subset_input by fastforce
qed
  

lemma distinct_on_no_compare: "(⋀x y . f x y ⟹ f y x)⟹ 
  distinct_on f xs ⟹ x∈set xs ⟹ y∈set xs ⟹ x≠y ⟹ ¬ f x y"
  by (induction xs) auto

fun lookup :: "('a ⇒ bool) ⇒ ('a × 'b) list ⇒ 'b option" where
  "lookup _ [] = None"
| "lookup f ((x,y)#xs) = (if f x then Some y else lookup f xs)"

lemma lookup_present_eq_key: "distinct (map fst al) ⟹ (k, v) ∈ set al ⟷ lookup (λx. x=k) al = Some v"
  by (induction al) (auto simp add: rev_image_eqI split: if_splits)

lemma lookup_None_iff: "lookup P xs = None ⟷ ¬ (∃x. x ∈ set (map fst xs) ∧ P x)"
  by (induction xs) (auto split: if_splits)

lemma find_Some: "List.find P l = Some p ⟹ p∈set l ∧ P p"
  by (induction l) (auto split: if_splits) 

(* This means lookup seems somewhat superflouus *)
lemma find_Some_imp_lookup_Some: 
  "List.find (λ(k,_). P k) xs = Some (k,v) ⟹ lookup P xs = Some v"
  by (induction xs) auto

lemma lookup_Some_imp_find_Some: 
  "lookup P xs = Some v ⟹ ∃x. List.find (λ(k,_). P k) xs = Some (x,v)"
  by (induction xs) auto

lemma lookup_None_iff_find_None: "lookup P xs = None ⟷ List.find (λ(k,_). P k) xs = None"
  by (induction xs) auto

lemma lookup_eq_order_irrelevant:
  assumes "distinct (map fst pairs)" and "distinct (map fst pairs')" and "set pairs = set pairs'"
  shows "lookup (λx. x=k) pairs = lookup (λx. x=k) pairs'"
proof (cases "lookup (λx. x=k) pairs")
  case None
  then show ?thesis using lookup_None_iff
    by (metis assms(3) set_map)
next
  case (Some v)
  hence "(k,v)∈set pairs" 
    using assms(1) by (simp add: lookup_present_eq_key)
  hence el: "(k,v)∈set pairs'" using assms(3) by blast
  show ?thesis using lookup_present_eq_key[OF assms(2)] el Some by simp
qed

lemma lookup_Some_append_back:
  "lookup (λx. x=k) insts = Some v ⟹ lookup (λx. x=k) (insts@[(k,v')]) = Some v"
  by (induction insts arbitrary: ) auto

lemma lookup_eq_key_not_present: "key ∉ set (map fst inst) ⟹ lookup (λx. x = key) inst = None"
  by (induction inst) auto

lemma lookup_in_empty[simp]: "lookup f [] = None" by simp
lemma lookup_in_single[simp]: "lookup f [(k, v)] = (if f k then Some v else None)" by simp

lemma lookup_present_eq_key': "lookup (λx. x=k) al = Some v ⟹ (k, v) ∈ set al "
  by (induction al) (auto simp add: rev_image_eqI split: if_splits)

lemma lookup_present_eq_key'': "distinct (map fst al) ⟹ lookup (λx. x=k) al = Some v ⟷ (k, v) ∈ set al "
  by (induction al) (auto simp add: rev_image_eqI split: if_splits)

lemma key_present_imp_eq_lookup_finds_value: "k ∈ fst ` set al ⟹ ∃v . lookup (λx. x=k) al = Some v"
  by (induction al) (auto simp add: rev_image_eqI)

lemma list_allI: "(⋀x. x∈set l ⟹ P x) ⟹ list_all P l"
  by (induction l) auto

lemma map2_sym: "(⋀x y . f x y = f y x) ⟹ map2 f xs ys = map2 f ys xs"
proof (induction xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by (induction ys) auto
qed

lemma idem_map2: assumes "(⋀x. f x x = x)" shows "map2 f l l = l"
proof-
  have "length l = length l" by simp
  then show "map2 f l l = l" by (induction l l rule: list_induct2) (use assms in auto)
qed

lemma rev_induct2[consumes 1, case_names Nil snoc]:
  assumes "length xs = length ys"
  assumes "P [] []"
  assumes "(⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs @ [x]) (ys @ [y]))"
  shows "P xs ys"
proof-
  have "length (rev xs) = length (rev ys)" using assms(1) by simp
  hence "P (rev (rev xs)) (rev (rev ys))" 
    using assms(2-3) by (induction rule: list_induct2[of "rev xs" "rev ys"]) simp_all
  thus ?thesis by simp
qed

lemma alist_map_corr: "distinct (map fst al) ⟹ (k,v) ∈ set al ⟷ map_of al k = Some v"
  by simp

lemma distinct_fst_imp_distinct: "distinct (map fst l) ⟹ distinct l"
  by (induction l) auto

lemma length_alist:
  assumes "distinct (map fst al)" and "distinct (map fst al')" and "set al = set al'"
  shows "length al = length al'"
  using assms by (metis distinct_card length_map set_map)

lemma same_map_of_imp_same_length: 
  "distinct (map fst ars1) ⟹ distinct (map fst ars2) ⟹ map_of ars1 = map_of ars2
  ⟹ length ars1 = length ars2"
  (* Name is a bit to specific*)
  using length_alist map_of_inject_set by blast

lemma in_range_if_ex_key: "v ∈ ran m ⟷ (∃k. m k = Some v)" 
  by (auto simp add: ranI ran_def)

lemma set_AList_delete_bound: "set (AList.delete a l) ⊆ set l"
  by (induction l) auto

lemma list_all_clearjunk_cons: 
  "list_all P (x#(AList.clearjunk l)) ⟹ list_all P (AList.clearjunk (x#l))"
  by (induction l rule: AList.clearjunk.induct) (auto simp add: delete_twist)

lemma lookup_AList_delete: "k'≠k ⟹ lookup (λx. x = k) al = lookup (λx. x = k) (AList.delete k' al)" 
  by (induction al) auto

lemma lookup_AList_clearjunk: "lookup (λx. x = k) al = lookup (λx. x = k) (AList.clearjunk al)"
proof (induction al)
  case Nil
  then show ?case
    by simp
next
  case (Cons a al)
  then show ?case 
  proof(cases "fst a=k")
    case True
    then show ?thesis
      by (metis (full_types) clearjunk.simps(2) lookup.simps(2) prod.collapse)
  next
    case False
    have "lookup (λx. x = k) (AList.clearjunk (a # al)) 
      = lookup (λx. x = k) (a # AList.clearjunk (AList.delete (fst a) al))"
      by simp
    also have "… = lookup (λx. x = k) (AList.clearjunk (AList.delete (fst a) al))"
      by (metis (full_types) False lookup.simps(2) surjective_pairing)
    also have "… = lookup (λx. x = k) (AList.clearjunk al)"
      by (metis False clearjunk_delete lookup_AList_delete)
    also have "… = lookup (λx. x = k) al"
      using Cons.IH by auto
    also have "… = lookup (λx. x = k) (a # al)"
      by (metis (full_types) False lookup.simps(2) surjective_pairing)
    finally show ?thesis 
      by simp
  qed
qed

definition "diff_list xs ys ≡ fold removeAll ys xs"

lemma diff_list_set[simp]: "set (diff_list xs ys) = set xs - set ys"
  unfolding diff_list_def by (induction ys arbitrary: xs) auto

lemma diff_list_set_from_Nil[simp]: "diff_list [] ys = []"
  using last_in_set by fastforce

lemma diff_list_set_remove_Nil[simp]: "diff_list xs [] = xs"
  unfolding diff_list_def by (induction xs) auto

lemma diff_list_rec: "diff_list (x # xs) ys = (if x∈set ys then diff_list xs ys else x#diff_list xs ys)"
  unfolding diff_list_def by (induction ys arbitrary: x xs) auto
lemma diff_list_order_irr: "set ys = set ys' ⟹ diff_list xs ys = diff_list xs ys'"
proof (induction ys arbitrary: ys' xs)
  case Nil
  then show ?case by simp
next
  case (Cons y ys)
  then show ?case
    by (induction xs arbitrary: y ys ys') (simp_all add: diff_list_rec)
qed

(* Folding lists with option return typs. probably no longer relevant, was for implementing sorts by lists *)
lemma fold_Option_bind_eq_Some_start_not_None:
  "fold (λnew option . Option.bind option (f new)) list start = Some res
  ⟹ start ≠ None"
  by (induction list arbitrary: start res)
    (fastforce split: option.splits if_splits simp add: bind_eq_Some_conv)+

lemma fold_Option_bind_eq_Some_at_point_not_None:
  "fold (λnew option . Option.bind option (f new)) (l1@l2) start = Some res
  ⟹ fold (λnew option . Option.bind option (f new)) (l1) start ≠ None"
  by (induction l1 arbitrary: start res l2) (use fold_Option_bind_eq_Some_start_not_None in 
      ‹fastforce split: option.splits if_splits simp add: bind_eq_Some_conv›)+

lemma fold_Option_bind_eq_Some_start_not_None':
  "fold (λ(x,y) option . Option.bind option (f x y)) list start = Some res
  ⟹ start ≠ None"
proof (induction list arbitrary: start res)
  case Nil
  then show ?case 
    by simp
next
  case (Cons a list)
  then show ?case 
    by (fastforce split: option.splits if_splits prod.splits simp add: bind_eq_Some_conv)
qed

lemma fold_Option_bind_eq_None_start_None:
  "fold (λ(x,y) option . Option.bind option (f x y)) list None = None"
  by (induction list) (auto split: option.splits if_splits prod.splits)

lemma fold_Option_bind_at_some_point_None_eq_None:
  "fold (λ(x,y) option . Option.bind option (f x y)) l1 start = None ⟹
  fold (λ(x,y) option . Option.bind option (f x y)) (l1@l2) start = None"
proof (induction l1 arbitrary: start  l2)
  case Nil
  then show ?case using fold_Option_bind_eq_Some_start_not_None' by fastforce
next
  case (Cons a l1)
  then show ?case by simp
qed

lemma fold_Option_bind_eq_Some_at_each_point_Some:
  "fold (λ(x,y) option . Option.bind option (f x y)) (l1@l2) start = Some res
  ⟹ (∃point . fold (λ(x,y) option . Option.bind option (f x y)) l1 start = Some point
    ∧ fold (λ(x,y) option . Option.bind option (f x y)) l2 (Some point) = Some res)"
proof (induction l1 arbitrary: start res l2)
  case Nil
  then show ?case 
    using fold_Option_bind_eq_Some_start_not_None' by fastforce
next
  case (Cons a l1)
  then show ?case by simp
qed

lemma fold_Option_bind_eq_Some_at_each_point_Some':
  assumes "fold (λ(x,y) option . Option.bind option (f x y)) (xs@ys) start = Some res"
  obtains point where 
    "fold (λ(x,y) option . Option.bind option (f x y)) xs start = Some point" and
    "fold (λ(x,y) option . Option.bind option (f x y)) ys (Some point) = Some res"
  using assms fold_Option_bind_eq_Some_at_each_point_Some by fast

(* Legacy *)
corollary fold_Option_bind_eq_Some_at_point_not_None':
  "fold (λ(x,y) option . Option.bind option (f x y)) (l1@l2) start = Some res
  ⟹ fold (λ(x,y) option . Option.bind option (f x y)) (l1) start ≠ None"
  using fold_Option_bind_eq_Some_at_each_point_Some by fast

(* Interestingly no longer need helper... *)
lemma fold_matches_first_step_not_None:
  assumes
    "fold (λ(T, U) subs . Option.bind subs (f T U)) (zip (x#xs) (y#ys)) (Some subs) = Some subs'" 
  obtains point where
    "f x y subs = Some point"
    "fold (λ(T, U) subs . Option.bind subs (f T U)) (zip (xs) (ys)) (Some point) = Some subs'"
  using assms fold_Option_bind_eq_Some_start_not_None' not_None_eq by fastforce

lemma fold_matches_last_step_not_None:
  assumes
    "length xs = length ys"
    "fold (λ(T, U) subs . Option.bind subs (f T U)) (zip (xs@[x]) (ys@[y])) (Some subs) = Some subs'" 
  obtains point where
    "fold (λ(T, U) subs . Option.bind subs (f T U)) (zip (xs) (ys)) (Some subs) = Some point"
    "f x y point = Some subs'"
  using assms fold_Option_bind_eq_Some_at_each_point_Some'[where xs="zip xs ys" and ys="[(x,y)]" 
      and start="Some subs" and res="subs'" and f="f"] by auto

end