Theory Containers.Lexicographic_Order
theory Lexicographic_Order imports
List_Fusion
"HOL-Library.Char_ord"
begin
hide_const (open) List.lexordp
section ‹List fusion for lexicographic order›
context linorder begin
lemma lexordp_take_index_conv:
"lexordp xs ys ⟷
(length xs < length ys ∧ take (length xs) ys = xs) ∨
(∃i < min (length xs) (length ys). take i xs = take i ys ∧ xs ! i < ys ! i)"
(is "?lhs = ?rhs")
proof
assume ?lhs thus ?rhs
by induct (auto 4 3 del: disjCI intro: disjI2 exI[where x="Suc i" for i])
next
assume ?rhs (is "?prefix ∨ ?less") thus ?lhs
proof
assume "?prefix"
hence "ys = xs @ hd (drop (length xs) ys) # tl (drop (length xs) ys)"
by (metis append_Nil2 append_take_drop_id less_not_refl list.collapse)
thus ?thesis unfolding lexordp_iff by blast
next
assume "?less"
then obtain i where "i < min (length xs) (length ys)"
and "take i xs = take i ys" and nth: "xs ! i < ys ! i" by blast
hence "xs = take i xs @ xs ! i # drop (Suc i) xs" "ys = take i xs @ ys ! i # drop (Suc i) ys"
by -(subst append_take_drop_id[symmetric, of _ i], simp_all add: Cons_nth_drop_Suc)
with nth show ?thesis unfolding lexordp_iff by blast
qed
qed
lemma lexordp_lex: "(xs, ys) ∈ lex {(xs, ys). xs < ys} ⟷ lexordp xs ys ∧ length xs = length ys"
proof(induct xs arbitrary: ys)
case Nil thus ?case by clarsimp
next
case Cons thus ?case by(cases ys)(simp_all, safe, simp)
qed
end
subsection ‹Setup for list fusion›
context ord begin
definition lexord_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where [code del]: "lexord_fusion g1 g2 s1 s2 = lexordp (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
definition lexord_eq_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where [code del]: "lexord_eq_fusion g1 g2 s1 s2 = lexordp_eq (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
lemma lexord_fusion_code:
"lexord_fusion g1 g2 s1 s2 ⟷
(if list.has_next g1 s1 then
if list.has_next g2 s2 then
let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in x < y ∨ ¬ y < x ∧ lexord_fusion g1 g2 s1' s2'
else False
else list.has_next g2 s2)"
unfolding lexord_fusion_def
by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm)
lemma lexord_eq_fusion_code:
"lexord_eq_fusion g1 g2 s1 s2 ⟷
(list.has_next g1 s1 ⟶
list.has_next g2 s2 ∧
(let (x, s1') = list.next g1 s1;
(y, s2') = list.next g2 s2
in x < y ∨ ¬ y < x ∧ lexord_eq_fusion g1 g2 s1' s2'))"
unfolding lexord_eq_fusion_def
by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm)
end
lemmas [code] =
lexord_fusion_code ord.lexord_fusion_code
lexord_eq_fusion_code ord.lexord_eq_fusion_code
lemmas [symmetric, code_unfold] =
lexord_fusion_def ord.lexord_fusion_def
lexord_eq_fusion_def ord.lexord_eq_fusion_def
end