Theory Ordered_Resolution_Prover.Lazy_List_Chain
section ‹Relational Chains over Lazy Lists›
theory Lazy_List_Chain
imports
"HOL-Library.BNF_Corec"
Lazy_List_Liminf
begin
text ‹
A chain is a lazy list of elements such that all pairs of consecutive elements are related by a
given relation. A full chain is either an infinite chain or a finite chain that cannot be extended.
The inspiration for this theory is Section 4.1 (``Theorem Proving Processes'') of Bachmair and
Ganzinger's chapter.
›
subsection ‹Chains›
coinductive chain :: "('a ⇒ 'a ⇒ bool) ⇒ 'a llist ⇒ bool" for R :: "'a ⇒ 'a ⇒ bool" where
chain_singleton: "chain R (LCons x LNil)"
| chain_cons: "chain R xs ⟹ R x (lhd xs) ⟹ chain R (LCons x xs)"
lemma
chain_LNil[simp]: "¬ chain R LNil" and
chain_not_lnull: "chain R xs ⟹ ¬ lnull xs"
by (auto elim: chain.cases)
lemma chain_lappend:
assumes
r_xs: "chain R xs" and
r_ys: "chain R ys" and
mid: "R (llast xs) (lhd ys)"
shows "chain R (lappend xs ys)"
proof (cases "lfinite xs")
case True
then show ?thesis
using r_xs mid
proof (induct rule: lfinite.induct)
case (lfinite_LConsI xs x)
note fin = this(1) and ih = this(2) and r_xxs = this(3) and mid = this(4)
show ?case
proof (cases "xs = LNil")
case True
then show ?thesis
using r_ys mid by simp (rule chain_cons)
next
case xs_nnil: False
have r_xs: "chain R xs"
by (metis chain.simps ltl_simps(2) r_xxs xs_nnil)
have mid': "R (llast xs) (lhd ys)"
by (metis llast_LCons lnull_def mid xs_nnil)
have start: "R x (lhd (lappend xs ys))"
by (metis (no_types) chain.simps lhd_LCons lhd_lappend chain_not_lnull ltl_simps(2) r_xxs
xs_nnil)
show ?thesis
unfolding lappend_code(2) using ih[OF r_xs mid'] start by (rule chain_cons)
qed
qed simp
qed (simp add: r_xs lappend_inf)
lemma chain_length_pos: "chain R xs ⟹ llength xs > 0"
by (cases xs) simp+
lemma chain_ldropn:
assumes "chain R xs" and "enat n < llength xs"
shows "chain R (ldropn n xs)"
using assms
by (induct n arbitrary: xs, simp,
metis chain.cases ldrop_eSuc_ltl ldropn_LNil ldropn_eq_LNil ltl_simps(2) not_less)
lemma inf_chain_ldropn_chain: "chain R xs ⟹ ¬ lfinite xs ⟹ chain R (ldropn n xs)"
using chain.simps[of R xs] by (simp add: chain_ldropn not_lfinite_llength)
lemma inf_chain_ltl_chain: "chain R xs ⟹ ¬ lfinite xs ⟹ chain R (ltl xs)"
by (metis inf_chain_ldropn_chain ldropn_0 ldropn_ltl)
lemma chain_lnth_rel:
assumes
chain: "chain R xs" and
len: "enat (Suc j) < llength xs"
shows "R (lnth xs j) (lnth xs (Suc j))"
proof -
define ys where "ys = ldropn j xs"
have "llength ys > 1"
unfolding ys_def using len
by (metis One_nat_def funpow_swap1 ldropn_0 ldropn_def ldropn_eq_LNil ldropn_ltl not_less
one_enat_def)
obtain y0 y1 ys' where
ys: "ys = LCons y0 (LCons y1 ys')"
unfolding ys_def by (metis Suc_ile_eq ldropn_Suc_conv_ldropn len less_imp_not_less not_less)
have "chain R ys"
unfolding ys_def using Suc_ile_eq chain chain_ldropn len less_imp_le by blast
then have "R y0 y1"
unfolding ys by (auto elim: chain.cases)
then show ?thesis
using ys_def unfolding ys by (metis ldropn_Suc_conv_ldropn ldropn_eq_LConsD llist.inject)
qed
lemma infinite_chain_lnth_rel:
assumes "¬ lfinite c" and "chain r c"
shows "r (lnth c i) (lnth c (Suc i))"
using assms chain_lnth_rel lfinite_conv_llength_enat by force
lemma lnth_rel_chain:
assumes
"¬ lnull xs" and
"∀j. enat (j + 1) < llength xs ⟶ R (lnth xs j) (lnth xs (j + 1))"
shows "chain R xs"
using assms
proof (coinduction arbitrary: xs rule: chain.coinduct)
case chain
note nnul = this(1) and nth_chain = this(2)
show ?case
proof (cases "lnull (ltl xs)")
case True
have "xs = LCons (lhd xs) LNil"
using nnul True by (simp add: llist.expand)
then show ?thesis
by blast
next
case nnul': False
moreover have "xs = LCons (lhd xs) (ltl xs)"
using nnul by simp
moreover have
"∀j. enat (j + 1) < llength (ltl xs) ⟶ R (lnth (ltl xs) j) (lnth (ltl xs) (j + 1))"
using nnul nth_chain
by (metis Suc_eq_plus1 ldrop_eSuc_ltl ldropn_Suc_conv_ldropn ldropn_eq_LConsD lnth_ltl)
moreover have "R (lhd xs) (lhd (ltl xs))"
using nnul' nnul nth_chain[rule_format, of 0, simplified]
by (metis ldropn_0 ldropn_Suc_conv_ldropn ldropn_eq_LConsD lhd_LCons_ltl lhd_conv_lnth
lnth_Suc_LCons ltl_simps(2))
ultimately show ?thesis
by blast
qed
qed
lemma chain_lmap:
assumes "∀x y. R x y ⟶ R' (f x) (f y)" and "chain R xs"
shows "chain R' (lmap f xs)"
using assms
proof (coinduction arbitrary: xs)
case chain
then have "(∃y. xs = LCons y LNil) ∨ (∃ys x. xs = LCons x ys ∧ chain R ys ∧ R x (lhd ys))"
using chain.simps[of R xs] by auto
then show ?case
proof
assume "∃ys x. xs = LCons x ys ∧ chain R ys ∧ R x (lhd ys)"
then have "∃ys x. lmap f xs = LCons x ys ∧
(∃xs. ys = lmap f xs ∧ (∀x y. R x y ⟶ R' (f x) (f y)) ∧ chain R xs) ∧ R' x (lhd ys)"
using chain
by (metis (no_types) lhd_LCons llist.distinct(1) llist.exhaust_sel llist.map_sel(1)
lmap_eq_LNil chain_not_lnull ltl_lmap ltl_simps(2))
then show ?thesis
by auto
qed auto
qed
lemma chain_mono:
assumes "∀x y. R x y ⟶ R' x y" and "chain R xs"
shows "chain R' xs"
using assms by (rule chain_lmap[of _ _ "λx. x", unfolded llist.map_ident])
lemma chain_ldropnI:
assumes
rel: "∀j. j ≥ i ⟶ enat (Suc j) < llength xs ⟶ R (lnth xs j) (lnth xs (Suc j))" and
si_lt: "enat (Suc i) < llength xs"
shows "chain R (ldropn i xs)"
proof (rule lnth_rel_chain)
show "¬ lnull (ldropn i xs)"
using si_lt by (simp add: Suc_ile_eq less_le_not_le)
next
show "∀j. enat (j + 1) < llength (ldropn i xs) ⟶
R (lnth (ldropn i xs) j) (lnth (ldropn i xs) (j + 1))"
using rel
by (smt (verit, best) Suc_ile_eq add.commute ldropn_eq_LNil ldropn_ldropn leD
le_add1 linorder_le_less_linear lnth_ldropn order_less_imp_le plus_1_eq_Suc)
qed
lemma chain_ldropn_lmapI:
assumes
rel: "∀j. j ≥ i ⟶ enat (Suc j) < llength xs ⟶ R (f (lnth xs j)) (f (lnth xs (Suc j)))" and
si_lt: "enat (Suc i) < llength xs"
shows "chain R (ldropn i (lmap f xs))"
proof -
have "chain R (lmap f (ldropn i xs))"
using chain_lmap[of "λx y. R (f x) (f y)" R f, of "ldropn i xs"] chain_ldropnI[OF rel si_lt]
by auto
thus ?thesis
by auto
qed
lemma lfinite_chain_imp_rtranclp_lhd_llast: "lfinite xs ⟹ chain R xs ⟹ R⇧*⇧* (lhd xs) (llast xs)"
proof (induct rule: lfinite.induct)
case (lfinite_LConsI xs x)
note fin_xs = this(1) and ih = this(2) and r_x_xs = this(3)
show ?case
proof (cases "xs = LNil")
case xs_nnil: False
then have r_xs: "chain R xs"
using r_x_xs by (blast elim: chain.cases)
then show ?thesis
using ih[OF r_xs] xs_nnil r_x_xs
by (metis chain.cases converse_rtranclp_into_rtranclp lhd_LCons llast_LCons chain_not_lnull
ltl_simps(2))
qed simp
qed simp
lemma tranclp_imp_exists_finite_chain_list:
"R⇧+⇧+ x y ⟹ ∃xs. chain R (llist_of (x # xs @ [y]))"
proof (induct rule: tranclp.induct)
case (r_into_trancl x y)
then have "chain R (llist_of (x # [] @ [y]))"
by (auto intro: chain.intros)
then show ?case
by blast
next
case (trancl_into_trancl x y z)
note rstar_xy = this(1) and ih = this(2) and r_yz = this(3)
obtain xs where
xs: "chain R (llist_of (x # xs @ [y]))"
using ih by blast
define ys where
"ys = xs @ [y]"
have "chain R (llist_of (x # ys @ [z]))"
unfolding ys_def using r_yz chain_lappend[OF xs chain_singleton, of z]
by (auto simp: lappend_llist_of_LCons llast_LCons)
then show ?case
by blast
qed
inductive_cases chain_consE: "chain R (LCons x xs)"
inductive_cases chain_nontrivE: "chain R (LCons x (LCons y xs))"
subsection ‹A Coinductive Puzzle›
primrec prepend where
"prepend [] ys = ys"
| "prepend (x # xs) ys = LCons x (prepend xs ys)"
lemma lnull_prepend[simp]: "lnull (prepend xs ys) = (xs = [] ∧ lnull ys)"
by (induct xs) auto
lemma lhd_prepend[simp]: "lhd (prepend xs ys) = (if xs ≠ [] then hd xs else lhd ys)"
by (induct xs) auto
lemma prepend_LNil[simp]: "prepend xs LNil = llist_of xs"
by (induct xs) auto
lemma lfinite_prepend[simp]: "lfinite (prepend xs ys) ⟷ lfinite ys"
by (induct xs) auto
lemma llength_prepend[simp]: "llength (prepend xs ys) = length xs + llength ys"
by (induct xs) (auto simp: enat_0 iadd_Suc eSuc_enat[symmetric])
lemma llast_prepend[simp]: "¬ lnull ys ⟹ llast (prepend xs ys) = llast ys"
by (induct xs) (auto simp: llast_LCons)
lemma prepend_prepend: "prepend xs (prepend ys zs) = prepend (xs @ ys) zs"
by (induct xs) auto
lemma chain_prepend:
"chain R (llist_of zs) ⟹ last zs = lhd xs ⟹ chain R xs ⟹ chain R (prepend zs (ltl xs))"
by (induct zs; cases xs)
(auto split: if_splits simp: lnull_def[symmetric] intro!: chain_cons elim!: chain_consE)
lemma lmap_prepend[simp]: "lmap f (prepend xs ys) = prepend (map f xs) (lmap f ys)"
by (induct xs) auto
lemma lset_prepend[simp]: "lset (prepend xs ys) = set xs ∪ lset ys"
by (induct xs) auto
lemma prepend_LCons: "prepend xs (LCons y ys) = prepend (xs @ [y]) ys"
by (induct xs) auto
lemma lnth_prepend:
"lnth (prepend xs ys) i = (if i < length xs then nth xs i else lnth ys (i - length xs))"
by (induct xs arbitrary: i) (auto simp: lnth_LCons' nth_Cons')
theorem lfinite_less_induct[consumes 1, case_names less]:
assumes fin: "lfinite xs"
and step: "⋀xs. lfinite xs ⟹ (⋀zs. llength zs < llength xs ⟹ P zs) ⟹ P xs"
shows "P xs"
using fin proof (induct "the_enat (llength xs)" arbitrary: xs rule: less_induct)
case (less xs)
show ?case
using less(2) by (intro step[OF less(2)] less(1))
(auto dest!: lfinite_llength_enat simp: eSuc_enat elim!: less_enatE llength_eq_enat_lfiniteD)
qed
theorem lfinite_prepend_induct[consumes 1, case_names LNil prepend]:
assumes "lfinite xs"
and LNil: "P LNil"
and prepend: "⋀xs. lfinite xs ⟹ (⋀zs. (∃ys. xs = prepend ys zs ∧ ys ≠ []) ⟹ P zs) ⟹ P xs"
shows "P xs"
using assms(1) proof (induct xs rule: lfinite_less_induct)
case (less xs)
from less(1) show ?case
by (cases xs)
(force simp: LNil neq_Nil_conv dest: lfinite_llength_enat intro!: prepend[of "LCons _ _"] intro: less)+
qed
coinductive emb :: "'a llist ⇒ 'a llist ⇒ bool" where
"lfinite xs ⟹ emb LNil xs"
| "emb xs ys ⟹ emb (LCons x xs) (prepend zs (LCons x ys))"
inductive_cases emb_LConsE: "emb (LCons z zs) ys"
inductive_cases emb_LNil1E: "emb LNil ys"
inductive_cases emb_LNil2E: "emb xs LNil"
lemma emb_lfinite:
assumes "emb xs ys"
shows "lfinite ys ⟷ lfinite xs"
proof
assume "lfinite xs"
then show "lfinite ys" using assms
by (induct xs arbitrary: ys rule: lfinite_induct)
(auto simp: lnull_def neq_LNil_conv elim!: emb_LNil1E emb_LConsE)
next
assume "lfinite ys"
then show "lfinite xs" using assms
proof (induction ys arbitrary: xs rule: lfinite_less_induct)
case (less ys)
from less.prems ‹lfinite ys› show ?case
by (cases xs)
(auto simp: eSuc_enat elim!: emb_LNil1E emb_LConsE less.IH[rotated]
dest!: lfinite_llength_enat)
qed
qed
inductive prepend_cong1 for X where
prepend_cong1_base: "X xs ⟹ prepend_cong1 X xs"
| prepend_cong1_prepend: "prepend_cong1 X ys ⟹ prepend_cong1 X (prepend xs ys)"
lemma prepend_cong1_alt: "prepend_cong1 X xs ⟷ (∃ys zs. xs = prepend ys zs ∧ X zs)"
by (rule iffI, induct xs rule: prepend_cong1.induct)
(force simp: prepend_prepend intro: prepend_cong1.intros exI[of _ "[]"])+
lemma emb_prepend_coinduct_cong[rotated, case_names emb]:
assumes "(⋀x1 x2. X x1 x2 ⟹
(∃xs. x1 = LNil ∧ x2 = xs ∧ lfinite xs)
∨ (∃xs ys x zs. x1 = LCons x xs ∧ x2 = prepend zs (LCons x ys)
∧ (prepend_cong1 (X xs) ys ∨ emb xs ys)))" (is "⋀x1 x2. X x1 x2 ⟹ ?bisim x1 x2")
shows "X x1 x2 ⟹ emb x1 x2"
proof (erule emb.coinduct[OF prepend_cong1_base])
fix xs zs
assume "prepend_cong1 (X xs) zs"
then show "?bisim xs zs"
by (induct zs rule: prepend_cong1.induct) (erule assms, force simp: prepend_prepend)
qed
lemma emb_prepend: "emb xs ys ⟹ emb xs (prepend zs ys)"
by (coinduction arbitrary: xs zs ys rule: emb_prepend_coinduct_cong)
(force elim: emb.cases simp: prepend_prepend)
lemma prepend_cong1_emb: "prepend_cong1 (emb xs) ys = emb xs ys"
by (rule iffI, induct ys rule: prepend_cong1.induct)
(simp_all add: emb_prepend prepend_cong1_base)
lemma prepend_cong_distrib:
"prepend_cong1 (P ⊔ Q) xs ⟷ prepend_cong1 P xs ∨ prepend_cong1 Q xs"
unfolding prepend_cong1_alt by auto
lemma emb_prepend_coinduct_aux[case_names emb]:
assumes "X x1 x2 " "(⋀x1 x2. X x1 x2 ⟹
(∃xs. x1 = LNil ∧ x2 = xs ∧ lfinite xs)
∨ (∃xs ys x zs. x1 = LCons x xs ∧ x2 = prepend zs (LCons x ys)
∧ (prepend_cong1 (X xs ⊔ emb xs) ys)))"
shows "emb x1 x2"
using assms unfolding prepend_cong_distrib prepend_cong1_emb
by (rule emb_prepend_coinduct_cong)
lemma emb_prepend_coinduct[rotated, case_names emb]:
assumes "(⋀x1 x2. X x1 x2 ⟹
(∃xs. x1 = LNil ∧ x2 = xs ∧ lfinite xs)
∨ (∃xs ys x zs zs'. x1 = LCons x xs ∧ x2 = prepend zs (LCons x (prepend zs' ys))
∧ (X xs ys ∨ emb xs ys)))"
shows "X x1 x2 ⟹ emb x1 x2"
by (erule emb_prepend_coinduct_aux[of X]) (force simp: prepend_cong1_alt dest: assms)
context
begin
private coinductive chain' for R where
"chain' R (LCons x LNil)"
| "chain R (llist_of (x # zs @ [lhd xs])) ⟹
chain' R xs ⟹ chain' R (LCons x (prepend zs xs))"
private lemma chain_imp_chain': "chain R xs ⟹ chain' R xs"
proof (coinduction arbitrary: xs rule: chain'.coinduct)
case chain'
then show ?case
proof (cases rule: chain.cases)
case (chain_cons zs z)
then show ?thesis
by (intro disjI2 exI[of _ z] exI[of _ "[]"] exI[of _ "zs"])
(auto intro: chain.intros)
qed simp
qed
private lemma chain'_imp_chain: "chain' R xs ⟹ chain R xs"
proof (coinduction arbitrary: xs rule: chain.coinduct)
case chain
then show ?case
proof (cases rule: chain'.cases)
case (2 y zs ys)
then show ?thesis
by (intro disjI2 exI[of _ "prepend zs ys"] exI[of _ y])
(force dest!: neq_Nil_conv[THEN iffD1] elim: chain.cases chain_nontrivE
intro: chain'.intros)
qed simp
qed
private lemma chain_chain': "chain = chain'"
unfolding fun_eq_iff by (metis chain_imp_chain' chain'_imp_chain)
lemma chain_prepend_coinduct[case_names chain]:
"X x ⟹ (⋀x. X x ⟹
(∃z. x = LCons z LNil) ∨
(∃y xs zs. x = LCons y (prepend zs xs) ∧
(X xs ∨ chain R xs) ∧ chain R (llist_of (y # zs @ [lhd xs])))) ⟹ chain R x"
by (subst chain_chain', erule chain'.coinduct) (force simp: chain_chain')
end
context
fixes R :: "'a ⇒ 'a ⇒ bool"
begin
private definition pick where
"pick x y = (SOME xs. chain R (llist_of (x # xs @ [y])))"
private lemma pick[simp]:
assumes "R⇧+⇧+ x y"
shows "chain R (llist_of (x # pick x y @ [y]))"
unfolding pick_def using tranclp_imp_exists_finite_chain_list[THEN someI_ex, OF assms] by auto
private