Theory Gen_Comp

header {* \isaheader{Generic Compare Algorithms} *}
theory Gen_Comp
imports 
  "../Intf/Intf_Comp" 
  "../../../Automatic_Refinement/Automatic_Refinement"
begin

subsection {* Order for Product *}
(* TODO: Optimization? Or only go via prod_cmp? *)
lemma autoref_prod_cmp_dflt_id[autoref_rules_raw]: 
  "(dflt_cmp op ≤ op <, dflt_cmp op ≤ op <) ∈
    ⟨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 op ≤ op <) (R1 -> R1 -> Id)"
  assumes "GEN_OP cmp2 (dflt_cmp op ≤ op <) (R2 -> R2 -> Id)"
  shows "(cmp_prod cmp1 cmp2, dflt_cmp op ≤ op <) ∈
    ⟨R1,R2⟩prod_rel -> ⟨R1,R2⟩prod_rel -> Id"
proof -
  have E: "dflt_cmp op ≤ op < 
    = cmp_prod (dflt_cmp op ≤ op <) (dflt_cmp op ≤ op <)"
    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