Theory Deriving.Comparator_Generator

(*  Title:       Deriving class instances for datatypes
    Author:      Christian Sternagel and René Thiemann  <christian.sternagel|rene.thiemann@uibk.ac.at>
    Maintainer:  Christian Sternagel and René Thiemann 
    License:     LGPL
*)
section ‹Generating Comparators›

theory Comparator_Generator
imports
  "../Generator_Aux"
  "../Derive_Manager"
  Comparator
begin

typedecl ('a,'b,'c,'z)type

text ‹In the following, we define a generator which for a given datatype @{typ "('a,'b,'c,'z)type"}
  constructs a comparator of type 
  @{typ "'a comparator ⇒ 'b comparator ⇒ 'c comparator ⇒ 'z comparator ⇒ ('a,'b,'c,'z)type"}.
  To this end, we first compare the index of the constructors, then for equal constructors, we
  compare the arguments recursively and combine the results lexicographically.›

hide_type "type"

subsection ‹Lexicographic combination of @{typ order}›

fun comp_lex :: "order list ⇒ order"
where
  "comp_lex (c # cs) = (case c of Eq ⇒ comp_lex cs | _ ⇒ c)" |
  "comp_lex [] = Eq"

subsection ‹Improved code for non-lazy languages›

text ‹The following equations will eliminate all occurrences of @{term comp_lex}
  in the generated code of the comparators.›

lemma comp_lex_unfolds: 
  "comp_lex [] = Eq"
  "comp_lex [c] = c"
  "comp_lex (c # d # cs) = (case c of Eq ⇒ comp_lex (d # cs) | z ⇒ z)"
  by (cases c, auto)+

subsection ‹Pointwise properties for equality, symmetry, and transitivity› 


text ‹The pointwise properties are important during inductive proofs of soundness of comparators.
  They are defined in a way that are combinable with @{const comp_lex}.›

lemma comp_lex_eq: "comp_lex os = Eq ⟷ (∀ ord ∈ set os. ord = Eq)" 
  by (induct os) (auto split: order.splits)
  
definition trans_order :: "order ⇒ order ⇒ order ⇒ bool" where
  "trans_order x y z ⟷ x ≠ Gt ⟶ y ≠ Gt ⟶ z ≠ Gt ∧ ((x = Lt ∨ y = Lt) ⟶ z = Lt)"

lemma trans_orderI:
  "(x ≠ Gt ⟹ y ≠ Gt ⟹ z ≠ Gt ∧ ((x = Lt ∨ y = Lt) ⟶ z = Lt)) ⟹ trans_order x y z"
  by (simp add: trans_order_def)

lemma trans_orderD:
  assumes "trans_order x y z" and "x ≠ Gt" and "y ≠ Gt"
  shows "z ≠ Gt" and "x = Lt ∨ y = Lt ⟹ z = Lt"
  using assms by (auto simp: trans_order_def)

lemma All_less_Suc:
  "(∀i < Suc x. P i) ⟷ P 0 ∧ (∀i < x. P (Suc i))"
  using less_Suc_eq_0_disj by force

lemma comp_lex_trans:
  assumes "length xs = length ys"
    and "length ys = length zs"
    and "∀ i < length zs. trans_order (xs ! i) (ys ! i) (zs ! i)"
  shows "trans_order (comp_lex xs) (comp_lex ys) (comp_lex zs)"
using assms
proof (induct xs ys zs rule: list_induct3)
  case (Cons x xs y ys z zs)
  then show ?case
    by (intro trans_orderI)
       (cases x y z rule: order.exhaust [case_product order.exhaust order.exhaust],
        auto simp: All_less_Suc dest: trans_orderD)
qed (simp add: trans_order_def)

lemma comp_lex_sym:
  assumes "length xs = length ys"
    and "∀ i < length ys. invert_order (xs ! i) = ys ! i"
  shows "invert_order (comp_lex xs) = comp_lex ys"
  using assms by (induct xs ys rule: list_induct2, simp, case_tac x) fastforce+

declare comp_lex.simps [simp del]

definition peq_comp :: "'a comparator ⇒ 'a ⇒ bool"
where
  "peq_comp acomp x ⟷ (∀ y. acomp x y = Eq ⟷ x = y)"

lemma peq_compD: "peq_comp acomp x ⟹ acomp x y = Eq ⟷ x = y"
  unfolding peq_comp_def by auto

lemma peq_compI: "(⋀ y. acomp x y = Eq ⟷ x = y) ⟹ peq_comp acomp x"
  unfolding peq_comp_def by auto

definition psym_comp :: "'a comparator ⇒ 'a ⇒ bool" where
  "psym_comp acomp x ⟷ (∀ y. invert_order (acomp x y) = (acomp y x))"

lemma psym_compD:
  assumes "psym_comp acomp x"
  shows "invert_order (acomp x y) = (acomp y x)"
  using assms unfolding psym_comp_def by blast+

lemma psym_compI:
  assumes "⋀ y. invert_order (acomp x y) = (acomp y x)"
  shows "psym_comp acomp x"
  using assms unfolding psym_comp_def by blast


definition ptrans_comp :: "'a comparator ⇒ 'a ⇒ bool" where
  "ptrans_comp acomp x ⟷ (∀ y z. trans_order (acomp x y) (acomp y z) (acomp x z))"

lemma ptrans_compD:
  assumes "ptrans_comp acomp x"
  shows "trans_order (acomp x y) (acomp y z) (acomp x z)"
  using assms unfolding ptrans_comp_def by blast+

lemma ptrans_compI:
  assumes "⋀ y z. trans_order (acomp x y) (acomp y z) (acomp x z)"
  shows "ptrans_comp acomp x"
  using assms unfolding ptrans_comp_def by blast

subsection ‹Separate properties of comparators›

definition eq_comp :: "'a comparator ⇒ bool" where
  "eq_comp acomp ⟷ (∀ x. peq_comp acomp x)"

lemma eq_compD2: "eq_comp acomp ⟹ peq_comp acomp x"
  unfolding eq_comp_def by blast

lemma eq_compI2: "(⋀ x. peq_comp acomp x) ⟹ eq_comp acomp" 
  unfolding eq_comp_def by blast
    
definition trans_comp :: "'a comparator ⇒ bool" where
  "trans_comp acomp ⟷ (∀ x. ptrans_comp acomp x)"
  
lemma trans_compD2: "trans_comp acomp ⟹ ptrans_comp acomp x"
  unfolding trans_comp_def by blast

lemma trans_compI2: "(⋀ x. ptrans_comp acomp x) ⟹ trans_comp acomp" 
  unfolding trans_comp_def by blast

  
definition sym_comp :: "'a comparator ⇒ bool" where
  "sym_comp acomp ⟷ (∀ x. psym_comp acomp x)"

lemma sym_compD2:
  "sym_comp acomp ⟹ psym_comp acomp x"
  unfolding sym_comp_def by blast

lemma sym_compI2: "(⋀ x. psym_comp acomp x) ⟹ sym_comp acomp" 
  unfolding sym_comp_def by blast

lemma eq_compD: "eq_comp acomp ⟹ acomp x y = Eq ⟷ x = y"
  by (rule peq_compD[OF eq_compD2])

lemma eq_compI: "(⋀ x y. acomp x y = Eq ⟷ x = y) ⟹ eq_comp acomp"
  by (intro eq_compI2 peq_compI)

lemma trans_compD: "trans_comp acomp ⟹ trans_order (acomp x y) (acomp y z) (acomp x z)"
  by (rule ptrans_compD[OF trans_compD2])

lemma trans_compI: "(⋀ x y z. trans_order (acomp x y) (acomp y z) (acomp x z)) ⟹ trans_comp acomp"
  by (intro trans_compI2 ptrans_compI)

lemma sym_compD:
  "sym_comp acomp ⟹ invert_order (acomp x y) = (acomp y x)" 
  by (rule psym_compD[OF sym_compD2])
  
lemma sym_compI: "(⋀ x y. invert_order (acomp x y) = (acomp y x)) ⟹ sym_comp acomp"
  by (intro sym_compI2 psym_compI)

lemma eq_sym_trans_imp_comparator:
  assumes "eq_comp acomp" and "sym_comp acomp" and "trans_comp acomp"
  shows "comparator acomp"
proof
  fix x y z
  show "invert_order (acomp x y) = acomp y x"
    using sym_compD [OF ‹sym_comp acomp›] .
  {
    assume "acomp x y = Eq"
    with eq_compD [OF ‹eq_comp acomp›]
    show "x = y" by blast
  }
  {
    assume "acomp x y = Lt" and "acomp y z = Lt"
    with trans_orderD [OF trans_compD [OF ‹trans_comp acomp›], of x y z]
    show "acomp x z = Lt" by auto
  }
qed

lemma comparator_imp_eq_sym_trans:
  assumes "comparator acomp"
  shows "eq_comp acomp" "sym_comp acomp" "trans_comp acomp" 
proof -
  interpret comparator acomp by fact
  show "eq_comp acomp" using eq by (intro eq_compI, auto)
  show "sym_comp acomp" using sym by (intro sym_compI, auto)
  show "trans_comp acomp"
  proof (intro trans_compI trans_orderI)
    fix x y z
    assume "acomp x y ≠ Gt" "acomp y z ≠ Gt"
    thus "acomp x z ≠ Gt ∧ (acomp x y = Lt ∨ acomp y z = Lt ⟶ acomp x z = Lt)"
      using comp_trans [of x y z] and eq [of x y] and eq [of y z]
      by (cases "acomp x y" "acomp y z" rule: order.exhaust [case_product order.exhaust]) auto
  qed
qed

context
  fixes acomp :: "'a comparator"
  assumes c: "comparator acomp"
begin
lemma comp_to_psym_comp: "psym_comp acomp x"
  using comparator_imp_eq_sym_trans[OF c]
  by (intro sym_compD2)

lemma comp_to_peq_comp: "peq_comp acomp x" 
  using comparator_imp_eq_sym_trans [OF c] 
  by (intro eq_compD2)
  
lemma comp_to_ptrans_comp: "ptrans_comp acomp x" 
  using comparator_imp_eq_sym_trans [OF c] 
  by (intro trans_compD2)
end

subsection ‹Auxiliary Lemmas for Comparator Generator›

lemma forall_finite: "(∀ i < (0 :: nat). P i) = True"
   "(∀ i < Suc 0. P i) = P 0"
   "(∀ i < Suc (Suc x). P i) = (P 0 ∧ (∀ i < Suc x. P (Suc i)))"
  by (auto, case_tac i, auto)
  
lemma trans_order_different:
  "trans_order a b Lt"
  "trans_order Gt b c"
  "trans_order a Gt c"
  by (intro trans_orderI, auto)+

lemma length_nth_simps: 
  "length [] = 0" "length (x # xs) = Suc (length xs)" 
  "(x # xs) ! 0 = x" "(x # xs) ! (Suc n) = xs ! n" by auto

subsection ‹The Comparator Generator›

ML_file ‹comparator_generator.ML›
                 
end