Theory Common

section ‹Commonly used Lemmas›
theory Common
imports 
  Main
  "HOL-Library.Extended_Nat" 
  "HOL-Eisbach.Eisbach"
begin

declare [[coercion_enabled = false]]

subsection ‹Miscellaneous›

lemma split_sym_rel: 
  fixes G :: "'a rel"
  assumes "sym G" "irrefl G"
  obtains E where "E∩E¯ = {}" "G = E ∪ E¯"  
proof -
  obtain R :: "'a rel" 
  where WO: "well_order_on UNIV R" using Zorn.well_order_on ..

  let ?E = "G ∩ R"
  
  from ‹irrefl G› have [simp, intro!]: "(x,x)∉G" for x 
    by (auto simp: irrefl_def)
  
  have "?E ∩ ?E¯ = {}"
    using WO 
    unfolding well_order_on_def linear_order_on_def 
      partial_order_on_def antisym_def
    by fastforce 
  moreover  
  have "G = ?E ∪ ?E¯" 
    apply safe
    apply (simp_all add: symD[OF ‹sym G›])
    using WO unfolding well_order_on_def linear_order_on_def total_on_def
    by force
  ultimately show ?thesis by (rule that)  
qed


lemma least_antimono: "X≠{} ⟹ X⊆Y ⟹ (LEAST y::_::wellorder. y∈Y) ≤ (LEAST x. x∈X)"
  by (metis LeastI_ex Least_le equals0I rev_subsetD)
  
lemma distinct_map_snd_inj: "distinct (map snd l) ⟹ (a,b)∈set l ⟹ (a',b)∈set l ⟹ a=a'"
  by (metis distinct_map inj_onD prod.sel(2) prod.simps(1))
  
lemma map_add_apply: "(m⇩1 ++ m⇩2) k = (case m⇩2 k of None ⇒ m⇩1 k | Some x ⇒ Some x)"
  by (auto simp: map_add_def)

lemma map_eq_append_conv: "map f xs = ys⇩1@ys⇩2 
  ⟷ (∃xs⇩1 xs⇩2. xs = xs⇩1@xs⇩2 ∧ map f xs⇩1 = ys⇩1 ∧ map f xs⇩2 = ys⇩2)"
  apply rule
  subgoal
    apply (rule exI[where x="take (length ys⇩1) xs"])
    apply (rule exI[where x="drop (length ys⇩1) xs"])
    apply (drule sym)
    by (auto simp: append_eq_conv_conj take_map drop_map)
  subgoal by auto
  done
  
  
lemma prod_case_const[simp]: "case_prod (λ_ _. c) = (λ_. c)" by auto

lemma card2_eq: "card e = 2 ⟷ (∃u v. u≠v ∧ e={u,v})"
  by (auto simp: eval_nat_numeral card_Suc_eq)

lemma in_ranE:
  assumes "v ∈ ran m"  
  obtains k where "m k = Some v"
  using assms unfolding ran_def by auto
  
  
lemma Inf_in:
  fixes A :: "'a::{linorder,complete_lattice} set"
  assumes "finite A" "A≠{}" 
  shows "Inf A ∈ A" 
  using assms 
  proof (induction A rule: finite_induct)
    case empty
    then show ?case by simp
  next
    have [simp]: "inf a b = (if a≤b then a else b)" for a b :: 'a
      by (meson inf_absorb2 le_iff_inf linear)
  
    case (insert x F)
    show ?case proof cases
      assume "F={}" thus ?thesis by auto
    next
      assume "F≠{}"
      with insert.IH have "Inf F ∈ F" .
      then show ?thesis
        using le_less_linear[of x "Inf F"]
        by auto 
    
  qed
qed  

lemma INF_of_enat_infty_iff1: "(INF x ∈ A. enat (f x)) = ∞ ⟷ A={}"
  apply (cases "A={}")
  subgoal by (simp add: top_enat_def)
  subgoal by safe (metis INF_top_conv(2) enat.distinct(1) top_enat_def)+
  done

lemma INF_of_enat_infty_iff2: 
  "∞ = (INF x ∈ A. enat (f x)) ⟷ A={}"  
  by (metis INF_of_enat_infty_iff1)

lemmas INF_of_enat_infty_iff[simp] = INF_of_enat_infty_iff1 INF_of_enat_infty_iff2
    
lemma INF_of_enat_nat_conv1: 
  assumes "finite A"  
  shows "(INF x ∈ A. enat (f x)) = enat d ⟷ (∃x∈A. d = f x ∧ (∀y∈A. f x ≤ f y))"  
proof -
  from assms have F: "finite (enat`f`A)" by auto

  show ?thesis proof (cases "A={}")
    case True thus ?thesis by (auto simp: top_enat_def)
  next
    case [simp]: False  
    note * = Inf_in[OF F, simplified]
    show ?thesis
      apply (rule iffI)
      subgoal by (smt False Inf_in assms enat.inject enat_ord_simps(1) finite_imageI imageE image_is_empty le_INF_iff order_refl)
      subgoal by clarsimp (meson INF_greatest INF_lower antisym enat_ord_simps(1))
      done
  qed
qed      
      
lemma INF_of_enat_nat_conv2: 
  assumes "finite A"  
  shows "enat d = (INF x ∈ A. enat (f x)) ⟷ (∃x∈A. d = f x ∧ (∀y∈A. f x ≤ f y))"  
  using INF_of_enat_nat_conv1[OF assms] by metis

lemmas INF_of_enat_nat_conv = INF_of_enat_nat_conv1 INF_of_enat_nat_conv2
  
lemma finite_inf_linorder_ne_ex:
  fixes f :: "_ ⇒ _::{complete_lattice,linorder}"
  assumes "finite S"
  assumes "S≠{}"
  shows "∃x∈S. (INF x ∈ S. f x) = f x"
  using assms
  by (meson Inf_in finite_imageI imageE image_is_empty)
  
  

lemma finite_linorder_eq_INF_conv: "finite S 
  ⟹ a = (INF x ∈ S. f x) ⟷ (if S={} then a=top else ∃x∈S. a=f x ∧ (∀y∈S. a ≤ f y))"
  for a :: "_::{complete_lattice,linorder}"
  by (auto 
    simp: INF_greatest INF_lower  
    intro: finite_inf_linorder_ne_ex antisym)
  
lemma sym_inv_eq[simp]: "sym E ⟹ E¯ = E" unfolding sym_def by auto 

lemma insert_inv[simp]: "(insert e E)¯ = insert (prod.swap e) (E¯)"
  by (cases e) auto
  
lemma inter_compl_eq_diff[simp]: "x ∩ - s = x - s"  
  by auto

lemma inter_same_diff[simp]: "A∩(A-S) = A-S" by blast  
  
lemma minus_inv_sym_aux[simp]: "(- {(a, b), (b, a)})¯ = -{(a,b),(b,a)}" 
  by auto
    

subsection ‹The-Default›
fun the_default :: "'a ⇒ 'a option ⇒ 'a" where
  "the_default d None = d"
| "the_default _ (Some x) = x"

lemma the_default_alt: "the_default d x = (case x of None ⇒ d | Some v ⇒ v)" by (auto split: option.split)


subsection ‹Implementing ‹enat› by Option›

text ‹Our maps are functions to ‹nat option›,which are interpreted as ‹enat›,
  ‹None› being ‹∞››

fun enat_of_option :: "nat option ⇒ enat" where
  "enat_of_option None = ∞" 
| "enat_of_option (Some n) = enat n"  
  
lemma enat_of_option_inj[simp]: "enat_of_option x = enat_of_option y ⟷ x=y"
  by (cases x; cases y; simp)

lemma enat_of_option_simps[simp]:
  "enat_of_option x = enat n ⟷ x = Some n"
  "enat_of_option x = ∞ ⟷ x = None"
  "enat n = enat_of_option x ⟷ x = Some n"
  "∞ = enat_of_option x ⟷ x = None"
  by (cases x; auto; fail)+
  
lemma enat_of_option_le_conv: "enat_of_option m ≤ enat_of_option n ⟷ (case (m,n) of 
    (_,None) ⇒ True
  | (Some a, Some b) ⇒ a≤b
  | (_, _) ⇒ False
)"
  by (auto split: option.split)

  
subsection ‹Foldr-Refine›
lemma foldr_refine:
  assumes "I s"
  assumes "⋀s x. I s ⟹ x∈set l ⟹ I (f x s) ∧ α (f x s) = f' x (α s)"
  shows "I (foldr f l s) ∧ α (foldr f l s) = foldr f' l (α s)"
  using assms
  by (induction l arbitrary: s) auto
  
end