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 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