Theory Intf_Comp

section ‹\isaheader{Orderings By Comparison Operator}›
theory Intf_Comp
imports 
  Automatic_Refinement.Automatic_Refinement
begin

subsection ‹Basic Definitions›

datatype comp_res = LESS | EQUAL | GREATER

consts i_comp_res :: interface
abbreviation "comp_res_rel ≡ Id :: (comp_res × _) set"
lemmas [autoref_rel_intf] = REL_INTFI[of comp_res_rel i_comp_res]

definition "comp2le cmp a b ≡ 
  case cmp a b of LESS ⇒ True | EQUAL ⇒ True | GREATER ⇒ False"

definition "comp2lt cmp a b ≡ 
  case cmp a b of LESS ⇒ True | EQUAL ⇒ False | GREATER ⇒ False"

definition "comp2eq cmp a b ≡ 
  case cmp a b of LESS ⇒ False | EQUAL ⇒ True | GREATER ⇒ False"

locale linorder_on =
  fixes D :: "'a set"
  fixes cmp :: "'a ⇒ 'a ⇒ comp_res"
  assumes lt_eq: "⟦x∈D; y∈D⟧ ⟹ cmp x y = LESS ⟷ (cmp y x = GREATER)"
  assumes refl[simp, intro!]: "x∈D ⟹ cmp x x = EQUAL"
  assumes trans[trans]: 
    "⟦ x∈D; y∈D; z∈D; cmp x y = LESS; cmp y z = LESS⟧ ⟹ cmp x z = LESS"
    "⟦ x∈D; y∈D; z∈D; cmp x y = LESS; cmp y z = EQUAL⟧ ⟹ cmp x z = LESS"
    "⟦ x∈D; y∈D; z∈D; cmp x y = EQUAL; cmp y z = LESS⟧ ⟹ cmp x z = LESS"
    "⟦ x∈D; y∈D; z∈D; cmp x y = EQUAL; cmp y z = EQUAL⟧ ⟹ cmp x z = EQUAL"
begin
  abbreviation "le ≡ comp2le cmp"
  abbreviation "lt ≡ comp2lt cmp"

  lemma eq_sym: "⟦x∈D; y∈D⟧ ⟹ cmp x y = EQUAL ⟹ cmp y x = EQUAL"
    apply (cases "cmp y x")
    using lt_eq lt_eq[symmetric]
    by auto
end

abbreviation "linorder ≡ linorder_on UNIV"

lemma linorder_to_class:
  assumes "linorder cmp" 
  assumes [simp]: "⋀x y. cmp x y = EQUAL ⟹ x=y"
  shows "class.linorder (comp2le cmp) (comp2lt cmp)"
proof -
  interpret linorder_on UNIV cmp by fact
  show ?thesis
    apply (unfold_locales)
    unfolding comp2le_def comp2lt_def
    apply (auto split: comp_res.split comp_res.split_asm)
    using lt_eq apply simp
    using lt_eq apply simp
    using lt_eq[symmetric] apply simp
    apply (drule (1) trans[rotated 3], simp_all) []
    apply (drule (1) trans[rotated 3], simp_all) []
    apply (drule (1) trans[rotated 3], simp_all) []
    apply (drule (1) trans[rotated 3], simp_all) []
    using lt_eq apply simp
    using lt_eq apply simp
    using lt_eq[symmetric] apply simp
    done
qed

definition "dflt_cmp le lt a b ≡ 
  if lt a b then LESS 
  else if le a b then EQUAL 
  else GREATER"

lemma (in linorder) class_to_linorder:
  "linorder (dflt_cmp (≤) (<))"
  apply (unfold_locales)
  unfolding dflt_cmp_def
  by (auto split: if_split_asm)

lemma restrict_linorder: "⟦linorder_on D cmp ; D'⊆D⟧ ⟹ linorder_on D' cmp"
  apply (rule linorder_on.intro)
  apply (drule (1) rev_subsetD)+
  apply (erule (2) linorder_on.lt_eq)
  apply (drule (1) rev_subsetD)+
  apply (erule (1) linorder_on.refl)
  apply (drule (1) rev_subsetD)+
  apply (erule (5) linorder_on.trans)
  apply (drule (1) rev_subsetD)+
  apply (erule (5) linorder_on.trans)
  apply (drule (1) rev_subsetD)+
  apply (erule (5) linorder_on.trans)
  apply (drule (1) rev_subsetD)+
  apply (erule (5) linorder_on.trans)
  done

subsection ‹Operations on Linear Orderings›

text ‹Map with injective function›
definition cmp_img where "cmp_img f cmp a b ≡ cmp (f a) (f b)"

lemma img_linorder[intro?]: 
  assumes LO: "linorder_on (f`D) cmp"
  shows "linorder_on D (cmp_img f cmp)"
  apply unfold_locales
  unfolding cmp_img_def
  apply (rule linorder_on.lt_eq[OF LO], auto) []
  apply (rule linorder_on.refl[OF LO], auto) []
  apply (erule (1) linorder_on.trans[OF LO, rotated -2], auto) []
  apply (erule (1) linorder_on.trans[OF LO, rotated -2], auto) []
  apply (erule (1) linorder_on.trans[OF LO, rotated -2], auto) []
  apply (erule (1) linorder_on.trans[OF LO, rotated -2], auto) []
  done

text ‹Combine›
definition "cmp_combine D1 cmp1 D2 cmp2 a b ≡ 
  if a∈D1 ∧ b∈D1 then cmp1 a b
  else if a∈D1 ∧ b∈D2 then LESS
  else if a∈D2 ∧ b∈D1 then GREATER
  else cmp2 a b
"

(* TODO: Move *)
lemma UnE': 
  assumes "x∈A∪B"
  obtains "x∈A" | "x∉A" "x∈B"
  using assms by blast

lemma combine_linorder[intro?]:
  assumes "linorder_on D1 cmp1"
  assumes "linorder_on D2 cmp2"
  assumes "D = D1∪D2"
  shows "linorder_on D (cmp_combine D1 cmp1 D2 cmp2)"
  apply unfold_locales
  unfolding cmp_combine_def
  using assms apply -
  apply (simp only:)
  apply (elim UnE)
  apply (auto dest: linorder_on.lt_eq) [4]

  apply (simp only:)
  apply (elim UnE)
  apply (auto dest: linorder_on.refl) [2]

  apply (simp only:)
  apply (elim UnE')
  apply simp_all [8]
  apply (erule (5) linorder_on.trans)
  apply (erule (5) linorder_on.trans)

  apply (simp only:)
  apply (elim UnE')
  apply simp_all [8]
  apply (erule (5) linorder_on.trans)
  apply (erule (5) linorder_on.trans)

  apply (simp only:)
  apply (elim UnE')
  apply simp_all [8]
  apply (erule (5) linorder_on.trans)
  apply (erule (5) linorder_on.trans)

  apply (simp only:)
  apply (elim UnE')
  apply simp_all [8]
  apply (erule (5) linorder_on.trans)
  apply (erule (5) linorder_on.trans)
  done

subsection ‹Universal Linear Ordering›
text ‹With Zorn's Lemma, we get a universal linear (even wf) ordering›

definition "univ_order_rel ≡ (SOME r. well_order_on UNIV r)"
definition "univ_cmp x y ≡ 
  if x=y then EQUAL 
  else if (x,y)∈univ_order_rel then LESS
  else GREATER"

lemma univ_wo: "well_order_on UNIV univ_order_rel"
  unfolding univ_order_rel_def
  using well_order_on[of UNIV]
  ..

lemma univ_linorder[intro?]: "linorder univ_cmp"
  apply unfold_locales
  unfolding univ_cmp_def 
  apply (auto split: if_split_asm)
  using univ_wo
  apply -
  unfolding well_order_on_def linear_order_on_def partial_order_on_def
    preorder_on_def
  apply (auto simp add: antisym_def) []
  apply (unfold total_on_def, fast) []
  apply (unfold trans_def, fast) []
  apply (auto simp add: antisym_def) []
  done

text ‹Extend any linear order to a universal order›
definition "cmp_extend D cmp ≡ 
  cmp_combine D cmp UNIV univ_cmp"

lemma extend_linorder[intro?]: 
  "linorder_on D cmp ⟹ linorder (cmp_extend D cmp)"
  unfolding cmp_extend_def
  apply rule
  apply assumption
  apply rule
  by simp

subsubsection ‹Lexicographic Order on Lists›  

fun cmp_lex where
  "cmp_lex cmp [] [] = EQUAL"
| "cmp_lex cmp [] _ = LESS"
| "cmp_lex cmp _ [] = GREATER"
| "cmp_lex cmp (a#l) (b#m) = (
    case cmp a b of
      LESS ⇒ LESS
    | EQUAL ⇒ cmp_lex cmp l m
    | GREATER ⇒ GREATER)"

primrec cmp_lex' where
  "cmp_lex' cmp [] m = (case m of [] ⇒ EQUAL | _ ⇒ LESS)"
| "cmp_lex' cmp (a#l) m = (case m of [] ⇒ GREATER | (b#m) ⇒ 
    (case cmp a b of
      LESS ⇒ LESS
    | EQUAL ⇒ cmp_lex' cmp l m
    | GREATER ⇒ GREATER
  ))"

lemma cmp_lex_alt: "cmp_lex cmp l m = cmp_lex' cmp l m"
  apply (induct l arbitrary: m)
  apply (auto split: comp_res.split list.split)
  done

lemma (in linorder_on) lex_linorder[intro?]:
  "linorder_on (lists D) (cmp_lex cmp)"
proof
  fix l m
  assume "l∈lists D" "m∈lists D"
  thus "(cmp_lex cmp l m = LESS) = (cmp_lex cmp m l = GREATER)"
    apply (induct cmp≡cmp l m rule: cmp_lex.induct)
    apply (auto split: comp_res.split simp: lt_eq)
    apply (auto simp: lt_eq[symmetric])
    done
next
  fix x
  assume "x∈lists D"
  thus "cmp_lex cmp x x = EQUAL"
    by (induct x) auto
next
  fix x y z
  assume M: "x∈lists D" "y∈lists D" "z∈lists D"

  {
    assume "cmp_lex cmp x y = LESS" "cmp_lex cmp y z = LESS"
    thus "cmp_lex cmp x z = LESS"
      using M
      apply (induct cmp≡cmp x y arbitrary: z rule: cmp_lex.induct)
      apply (auto split: comp_res.split_asm comp_res.split)
      apply (case_tac z, auto) []
      apply (case_tac z,
        auto split: comp_res.split_asm comp_res.split,
        (drule (4) trans, simp)+
      ) []
      apply (case_tac z,
        auto split: comp_res.split_asm comp_res.split,
        (drule (4) trans, simp)+
      ) []
      done
  }

  {
    assume "cmp_lex cmp x y = LESS" "cmp_lex cmp y z = EQUAL"
    thus "cmp_lex cmp x z = LESS"
      using M
      apply (induct cmp≡cmp x y arbitrary: z rule: cmp_lex.induct)
      apply (auto split: comp_res.split_asm comp_res.split)
      apply (case_tac z, auto) []
      apply (case_tac z,
        auto split: comp_res.split_asm comp_res.split,
        (drule (4) trans, simp)+
      ) []
      apply (case_tac z,
        auto split: comp_res.split_asm comp_res.split,
        (drule (4) trans, simp)+
      ) []
      done
  }

  {
    assume "cmp_lex cmp x y = EQUAL" "cmp_lex cmp y z = LESS"
    thus "cmp_lex cmp x z = LESS"
      using M
      apply (induct cmp≡cmp x y arbitrary: z rule: cmp_lex.induct)
      apply (auto split: comp_res.split_asm comp_res.split)
      apply (case_tac z,
        auto split: comp_res.split_asm comp_res.split,
        (drule (4) trans, simp)+
      ) []
      done
  }

  {
    assume "cmp_lex cmp x y = EQUAL" "cmp_lex cmp y z = EQUAL"
    thus "cmp_lex cmp x z = EQUAL"
      using M
      apply (induct cmp≡cmp x y arbitrary: z rule: cmp_lex.induct)
      apply (auto split: comp_res.split_asm comp_res.split)
      apply (case_tac z)
      apply (auto split: comp_res.split_asm comp_res.split)
      apply (drule (4) trans, simp)+
      done
  }
qed

subsubsection ‹Lexicographic Order on Pairs›  

fun cmp_prod where 
  "cmp_prod cmp1 cmp2 (a1,a2) (b1,b2) 
  = (
    case cmp1 a1 b1 of
      LESS ⇒ LESS
    | EQUAL ⇒ cmp2 a2 b2
    | GREATER ⇒ GREATER)"

lemma cmp_prod_alt: "cmp_prod = (λcmp1 cmp2 (a1,a2) (b1,b2). (
    case cmp1 a1 b1 of
      LESS ⇒ LESS
    | EQUAL ⇒ cmp2 a2 b2
    | GREATER ⇒ GREATER))"
  by (auto intro!: ext)

lemma prod_linorder[intro?]: 
  assumes A: "linorder_on A cmp1" 
  assumes B: "linorder_on B cmp2" 
  shows "linorder_on (A×B) (cmp_prod cmp1 cmp2)"
proof -
  interpret A: linorder_on A cmp1
    + B: linorder_on B cmp2 by fact+

  show ?thesis
    apply unfold_locales
    apply (auto split: comp_res.split comp_res.split_asm,
      simp_all add: A.lt_eq B.lt_eq,
      simp_all add: A.lt_eq[symmetric]
      ) []

    apply (auto split: comp_res.split comp_res.split_asm) []

    apply (auto split: comp_res.split comp_res.split_asm) []
    apply (drule (4) A.trans B.trans, simp)+

    apply (auto split: comp_res.split comp_res.split_asm) []
    apply (drule (4) A.trans B.trans, simp)+

    apply (auto split: comp_res.split comp_res.split_asm) []
    apply (drule (4) A.trans B.trans, simp)+

    apply (auto split: comp_res.split comp_res.split_asm) []
    apply (drule (4) A.trans B.trans, simp)+
    done
qed

subsection ‹Universal Ordering for Sets that is Effective for Finite Sets›

subsubsection ‹Sorted Lists of Sets›
text ‹Some more results about sorted lists of finite sets›

lemma set_to_map_set_is_map_of: 
  "distinct (map fst l) ⟹ set_to_map (set l) = map_of l"
  apply (induct l)
  apply (auto simp: set_to_map_insert)
  done

context linorder begin

  lemma sorted_list_of_set_eq_nil2[simp]:
    assumes "finite A" 
    shows "[] = sorted_list_of_set A ⟷ A={}"
    using assms
    by (auto dest: sym)

  lemma set_insort[simp]: "set (insort x l) = insert x (set l)"
    by (induct l) auto

  lemma sorted_list_of_set_inj_aux:
    fixes A B :: "'a set"
    assumes "finite A" 
    assumes "finite B" 
    assumes "sorted_list_of_set A = sorted_list_of_set B"
    shows "A=B"
    using assms
  proof -
    from ‹finite B› have "B = set (sorted_list_of_set B)" by simp
    also from assms have "… = set (sorted_list_of_set (A))"
      by simp
    also from ‹finite A› 
    have "set (sorted_list_of_set (A)) = A"
      by simp
    finally show ?thesis by simp
  qed

  lemma sorted_list_of_set_inj: "inj_on sorted_list_of_set (Collect finite)"
    apply (rule inj_onI)
    using sorted_list_of_set_inj_aux
    by blast
 
  definition "sorted_list_of_map m ≡ 
    map (λk. (k, the (m k))) (sorted_list_of_set (dom m))"

  lemma the_sorted_list_of_map:
    assumes "distinct (map fst l)"
    assumes "sorted (map fst l)"
    shows "sorted_list_of_map (map_of l) = l"
  proof -
    have "dom (map_of l) = set (map fst l)" by (induct l) force+
    hence "sorted_list_of_set (dom (map_of l)) = map fst l"
      using sorted_list_of_set.idem_if_sorted_distinct[OF assms(2,1)] by simp
    hence "sorted_list_of_map (map_of l) 
      = map (λk. (k, the (map_of l k))) (map fst l)"
      unfolding sorted_list_of_map_def by simp
    also have "… = l" using ‹distinct (map fst l)›
    proof (induct l)
      case Nil thus ?case by simp
    next
      case (Cons a l) 
      hence 
        1: "distinct (map fst l)" 
        and 2: "fst a∉fst`set l" 
        and 3: "map (λk. (k, the (map_of l k))) (map fst l) = l" 
        by simp_all

      from 2 have [simp]: "¬(∃x∈set l. fst x = fst a)"
        by (auto simp: image_iff)

      show ?case
        apply simp
        apply (subst (3) 3[symmetric])
        apply simp
        done
    qed
    finally show ?thesis .
  qed

  lemma map_of_sorted_list_of_map[simp]:
    assumes FIN: "finite (dom m)" 
    shows "map_of (sorted_list_of_map m) = m"
    unfolding sorted_list_of_map_def
  proof -
    have "set (sorted_list_of_set (dom m)) = dom m"
      and DIST: "distinct (sorted_list_of_set (dom m))"
      by (simp_all add: FIN) 

    have [simp]: "(fst ∘ (λk. (k, the (m k)))) = id" by auto

    have [simp]: "(λk. (k, the (m k))) ` dom m = map_to_set m"
      by (auto simp: map_to_set_def)

    show "map_of (map (λk. (k, the (m k))) (sorted_list_of_set (dom m))) = m"
      apply (subst set_to_map_set_is_map_of[symmetric])
      apply (simp add: DIST)
      apply (subst set_map)
      apply (simp add: FIN map_to_set_inverse)
      done
  qed

  lemma sorted_list_of_map_inj_aux:
    fixes A B :: "'a⇀'b"
    assumes [simp]: "finite (dom A)" 
    assumes [simp]: "finite (dom B)" 
    assumes E: "sorted_list_of_map A = sorted_list_of_map B"
    shows "A=B"
    using assms
  proof -
    have "A = map_of (sorted_list_of_map A)" by simp
    also note E
    also have "map_of (sorted_list_of_map B) = B" by simp
    finally show ?thesis .
  qed

  lemma sorted_list_of_map_inj: 
    "inj_on sorted_list_of_map (Collect (finite o dom))"
    apply (rule inj_onI)
    using sorted_list_of_map_inj_aux
    by auto
end

definition "cmp_set cmp ≡ 
  cmp_extend (Collect finite) (
    cmp_img
      (linorder.sorted_list_of_set (comp2le cmp)) 
      (cmp_lex cmp)
  )"

thm img_linorder

lemma set_ord_linear[intro?]: 
  "linorder cmp ⟹ linorder (cmp_set cmp)"
  unfolding cmp_set_def
  apply rule
  apply rule
  apply (rule restrict_linorder)
  apply (erule linorder_on.lex_linorder)
  apply simp
  done

definition "cmp_map cmpk cmpv ≡
  cmp_extend (Collect (finite o dom)) (
    cmp_img
      (linorder.sorted_list_of_map (comp2le cmpk))
      (cmp_lex (cmp_prod cmpk cmpv))
  )
"

lemma map_to_set_inj[intro!]: "inj map_to_set"
  apply (rule inj_onI)
  unfolding map_to_set_def
  apply (rule ext)
  apply (case_tac "x xa")
  apply (case_tac [!] "y xa")
  apply force+
  done

corollary map_to_set_inj'[intro!]: "inj_on map_to_set S"
  by (metis map_to_set_inj subset_UNIV subset_inj_on)
  
lemma map_ord_linear[intro?]: 
  assumes A: "linorder cmpk" 
  assumes B: "linorder cmpv" 
  shows "linorder (cmp_map cmpk cmpv)"
proof -
  interpret lk: linorder_on UNIV cmpk by fact
  interpret lv: linorder_on UNIV cmpv by fact
  
  show ?thesis
    unfolding cmp_map_def
    apply rule
    apply rule
    apply (rule restrict_linorder)
    apply (rule linorder_on.lex_linorder)
    apply (rule)
    apply fact
    apply fact
    apply simp
    done
qed
  
  
locale eq_linorder_on = linorder_on +
  assumes cmp_imp_equal: "⟦x∈D; y∈D⟧ ⟹ cmp x y = EQUAL ⟹ x = y"
begin
  lemma cmp_eq[simp]: "⟦x∈D; y∈D⟧ ⟹ cmp x y = EQUAL ⟷ x = y"
    by (auto simp: cmp_imp_equal)
end
  
abbreviation "eq_linorder ≡ eq_linorder_on UNIV"

lemma dflt_cmp_2inv[simp]: 
  "dflt_cmp (comp2le cmp) (comp2lt cmp) = cmp"
  unfolding dflt_cmp_def[abs_def] comp2le_def[abs_def] comp2lt_def[abs_def]
  apply (auto split: comp_res.splits intro!: ext)
  done

lemma (in linorder) dflt_cmp_inv2[simp]:
  shows 
  "(comp2le (dflt_cmp (≤) (<)))= (≤)"
  "(comp2lt (dflt_cmp (≤) (<)))= (<)"
proof -
  show "(comp2lt (dflt_cmp (≤) (<)))= (<)"
    unfolding dflt_cmp_def[abs_def] comp2le_def[abs_def] comp2lt_def[abs_def]
    apply (auto split: comp_res.splits intro!: ext)
    done

  show "(comp2le (dflt_cmp (≤) (<))) = (≤)"
    unfolding dflt_cmp_def[abs_def] comp2le_def[abs_def] comp2lt_def[abs_def]
    apply (auto split: comp_res.splits intro!: ext)
    done

qed
    
lemma eq_linorder_class_conv:
  "eq_linorder cmp ⟷ class.linorder (comp2le cmp) (comp2lt cmp)"
proof
  assume "eq_linorder cmp"
  then interpret eq_linorder_on UNIV cmp .
  have "linorder cmp" by unfold_locales
  show "class.linorder (comp2le cmp) (comp2lt cmp)"
    apply (rule linorder_to_class)
    apply fact
    by simp
next
  assume "class.linorder (comp2le cmp) (comp2lt cmp)"
  then interpret linorder "comp2le cmp" "comp2lt cmp" .
  
  from class_to_linorder interpret linorder_on UNIV cmp
    by simp
  show "eq_linorder cmp"
  proof
    fix x y
    assume "cmp x y = EQUAL"
    hence "comp2le cmp x y" "¬comp2lt cmp x y"
      by (auto simp: comp2le_def comp2lt_def)
    thus "x=y" by simp
  qed
qed
  
lemma (in linorder) class_to_eq_linorder:
  "eq_linorder (dflt_cmp (≤) (<))"
proof -
  interpret linorder_on UNIV "dflt_cmp (≤) (<)"
    by (rule class_to_linorder)

  show ?thesis
    apply unfold_locales
    apply (auto simp: dflt_cmp_def split: if_split_asm)
    done
qed

lemma eq_linorder_comp2eq_eq: 
  assumes "eq_linorder cmp"
  shows "comp2eq cmp = (=)"
proof -
  interpret eq_linorder_on UNIV cmp by fact
  show ?thesis
    apply (intro ext)
    unfolding comp2eq_def
    apply (auto split: comp_res.split dest: refl)
    done
qed
    
lemma restrict_eq_linorder: 
  assumes "eq_linorder_on D cmp" 
  assumes S: "D'⊆D" 
  shows "eq_linorder_on D' cmp"
proof -
  interpret eq_linorder_on D cmp by fact
  
  show ?thesis
    apply (rule eq_linorder_on.intro)
    apply (rule restrict_linorder[where D=D])
    apply unfold_locales []
    apply fact
    apply unfold_locales
    using S
    apply -
    apply (drule (1) rev_subsetD)+
    apply auto
    done
qed
  
lemma combine_eq_linorder[intro?]:
  assumes A: "eq_linorder_on D1 cmp1"
  assumes B: "eq_linorder_on D2 cmp2"
  assumes EQ: "D=D1∪D2"
  shows "eq_linorder_on D (cmp_combine D1 cmp1 D2 cmp2)"
proof -
  interpret A: eq_linorder_on D1 cmp1 by fact
  interpret B: eq_linorder_on D2 cmp2 by fact
  interpret linorder_on "(D1 ∪ D2)" "(cmp_combine D1 cmp1 D2 cmp2)"
    apply rule
    apply unfold_locales
    by simp
  
  show ?thesis
    apply (simp only: EQ)
    apply unfold_locales
    unfolding cmp_combine_def
    by (auto split: if_split_asm)
qed

lemma img_eq_linorder[intro?]:
  assumes A: "eq_linorder_on (f`D) cmp"
  assumes INJ: "inj_on f D"
  shows "eq_linorder_on D (cmp_img f cmp)"
proof -
  interpret eq_linorder_on "f`D" cmp by fact
  interpret L: linorder_on "(D)" "(cmp_img f cmp)"
    apply rule
    apply unfold_locales
    done
  
  show ?thesis
    apply unfold_locales
    unfolding cmp_img_def
    using INJ
    apply (auto dest: inj_onD)
    done
qed

lemma univ_eq_linorder[intro?]:
  shows "eq_linorder univ_cmp"
  apply (rule eq_linorder_on.intro)
  apply rule
  apply unfold_locales
  unfolding univ_cmp_def
  apply (auto split: if_split_asm)
  done
  
lemma extend_eq_linorder[intro?]:
  assumes "eq_linorder_on D cmp"
  shows "eq_linorder (cmp_extend D cmp)"
proof -
  interpret eq_linorder_on D cmp by fact
  show ?thesis
    unfolding cmp_extend_def
    apply (rule)
    apply fact
    apply rule
    by simp
qed
  
lemma lex_eq_linorder[intro?]:
  assumes "eq_linorder_on D cmp"
  shows "eq_linorder_on (lists D) (cmp_lex cmp)"
proof -
  interpret eq_linorder_on D cmp by fact
  show ?thesis
    apply (rule eq_linorder_on.intro)
    apply rule
    apply unfold_locales
    subgoal for l m
      apply (induct cmp≡cmp l m rule: cmp_lex.induct)
      apply (auto split: comp_res.splits)
      done
    done
qed

lemma prod_eq_linorder[intro?]:
  assumes "eq_linorder_on D1 cmp1"
  assumes "eq_linorder_on D2 cmp2"
  shows "eq_linorder_on (D1×D2) (cmp_prod cmp1 cmp2)"
proof -
  interpret A: eq_linorder_on D1 cmp1 by fact
  interpret B: eq_linorder_on D2 cmp2 by fact
  show ?thesis
    apply (rule eq_linorder_on.intro)
    apply rule
    apply unfold_locales
    apply (auto split: comp_res.splits)
    done
qed

lemma set_ord_eq_linorder[intro?]: 
  "eq_linorder cmp ⟹ eq_linorder (cmp_set cmp)"
  unfolding cmp_set_def
  apply rule
  apply rule
  apply (rule restrict_eq_linorder)
  apply rule
  apply assumption
  apply simp

  apply (rule linorder.sorted_list_of_set_inj)
  apply (subst (asm) eq_linorder_class_conv)
  .

lemma map_ord_eq_linorder[intro?]: 
  "⟦eq_linorder cmpk; eq_linorder cmpv⟧ ⟹ eq_linorder (cmp_map cmpk cmpv)"
  unfolding cmp_map_def
  apply rule
  apply rule
  apply (rule restrict_eq_linorder)
  apply rule
  apply rule
  apply assumption
  apply assumption
  apply simp

  apply (rule linorder.sorted_list_of_map_inj)
  apply (subst (asm) eq_linorder_class_conv)
  .

definition cmp_unit :: "unit ⇒ unit ⇒ comp_res" 
  where [simp]: "cmp_unit u v ≡ EQUAL"

lemma cmp_unit_eq_linorder:
  "eq_linorder cmp_unit"
  by unfold_locales simp_all
  
subsection ‹Parametricity›  
  
lemma param_cmp_extend[param]:
  assumes "(cmp,cmp')∈R → R → Id"
  assumes "Range R ⊆ D"
  shows "(cmp,cmp_extend D cmp') ∈ R → R → Id"
  unfolding cmp_extend_def cmp_combine_def[abs_def]
  using assms
  apply clarsimp
  by (blast dest!: fun_relD)

lemma param_cmp_img[param]: 
  "(cmp_img,cmp_img) ∈ (Ra→Rb) → (Rb→Rb→Rc) → Ra → Ra → Rc"
  unfolding cmp_img_def[abs_def]
  by parametricity

lemma param_comp_res[param]:
  "(LESS,LESS)∈Id"
  "(EQUAL,EQUAL)∈Id"
  "(GREATER,GREATER)∈Id"
  "(case_comp_res,case_comp_res)∈Ra→Ra→Ra→Id→Ra"
  by (auto split: comp_res.split)

term cmp_lex
lemma param_cmp_lex[param]:
  "(cmp_lex,cmp_lex)∈(Ra→Rb→Id)→⟨Ra⟩list_rel→⟨Rb⟩list_rel→Id"
  unfolding cmp_lex_alt[abs_def] cmp_lex'_def
  by (parametricity)

term cmp_prod
lemma param_cmp_prod[param]:
  "(cmp_prod,cmp_prod)∈
  (Ra→Rb→Id)→(Rc→Rd→Id)→⟨Ra,Rc⟩prod_rel→⟨Rb,Rd⟩prod_rel→Id"
  unfolding cmp_prod_alt
  by (parametricity)

lemma param_cmp_unit[param]: 
  "(cmp_unit,cmp_unit)∈Id→Id→Id" 
  by auto

lemma param_comp2eq[param]: "(comp2eq,comp2eq)∈(R→R→Id)→R→R→Id"
  unfolding comp2eq_def[abs_def]
  by (parametricity)


  
lemma cmp_combine_paramD:
  assumes "(cmp,cmp_combine D1 cmp1 D2 cmp2)∈R→R→Id"
  assumes "Range R ⊆ D1"
  shows "(cmp,cmp1)∈R→R→Id"
  using assms
  unfolding cmp_combine_def[abs_def]
  apply (intro fun_relI)
  apply (drule_tac x=a in fun_relD, assumption)
  apply (drule_tac x=aa in fun_relD, assumption)
  apply (drule RangeI, drule (1) rev_subsetD)
  apply (drule RangeI, drule (1) rev_subsetD)
  apply simp
  done

lemma cmp_extend_paramD:
  assumes "(cmp,cmp_extend D cmp')∈R→R→Id"
  assumes "Range R ⊆ D"
  shows "(cmp,cmp')∈R→R→Id"
  using assms
  unfolding cmp_extend_def
  apply (rule cmp_combine_paramD)
  done
  

subsection ‹Tuning of Generated Implementation›
lemma [autoref_post_simps]: "comp2eq (dflt_cmp (≤) ((<)::_::linorder⇒_)) = (=)"
  by (simp add: class_to_eq_linorder eq_linorder_comp2eq_eq)



end