Theory Gen_Comp

section ‹\isaheader{Generic Compare Algorithms}›
theory Gen_Comp
imports 
  "../Intf/Intf_Comp"
  Automatic_Refinement.Automatic_Refinement
  "HOL-Library.Product_Lexorder"
begin

subsection ‹Order for Product›
(* TODO: Optimization? Or only go via prod_cmp? *)
lemma autoref_prod_cmp_dflt_id[autoref_rules_raw]: 
  "(dflt_cmp (≤) (<), dflt_cmp (≤) (<)) ∈
    ⟨Id,Id⟩prod_rel → ⟨Id,Id⟩prod_rel → Id"
  by auto

lemma gen_prod_cmp_dflt[autoref_rules_raw]:
  assumes PRIO_TAG_GEN_ALGO
  assumes "GEN_OP cmp1 (dflt_cmp (≤) (<)) (R1 → R1 → Id)"
  assumes "GEN_OP cmp2 (dflt_cmp (≤) (<)) (R2 → R2 → Id)"
  shows "(cmp_prod cmp1 cmp2, dflt_cmp (≤) (<)) ∈
    ⟨R1,R2⟩prod_rel → ⟨R1,R2⟩prod_rel → Id"
proof -
  have E: "dflt_cmp (≤) (<) 
    = cmp_prod (dflt_cmp (≤) (<)) (dflt_cmp (≤) (<))"
    by (auto simp: dflt_cmp_def prod_less_def prod_le_def intro!: ext)

  show ?thesis
    using assms
    unfolding autoref_tag_defs E
    by parametricity
qed


end