section ‹Transitions›
text ‹This theory contains some facts about closure, the definition of full transformations, and
well-foundedness.›
theory Wellfounded_More
imports Main
begin
subsection ‹More theorems about Closures›
text ‹This is the equivalent of the theorem @{thm [source] rtranclp_mono} for @{term tranclp}›
lemma tranclp_mono_explicit:
‹r⇧+⇧+ a b ⟹ r ≤ s ⟹ s⇧+⇧+ a b›
using rtranclp_mono by (auto dest!: tranclpD intro: rtranclp_into_tranclp2)
lemma tranclp_mono:
assumes mono: ‹r ≤ s›
shows ‹r⇧+⇧+ ≤ s⇧+⇧+›
using rtranclp_mono[OF mono] mono by (auto dest!: tranclpD intro: rtranclp_into_tranclp2)
lemma tranclp_idemp_rel:
‹R⇧+⇧+⇧+⇧+ a b ⟷ R⇧+⇧+ a b›
apply (rule iffI)
prefer 2 apply blast
by (induction rule: tranclp_induct) auto
text ‹Equivalent of the theorem @{thm [source] rtranclp_idemp}›
lemma trancl_idemp: ‹(r⇧+)⇧+ = r⇧+›
by simp
lemmas tranclp_idemp[simp] = trancl_idemp[to_pred]
text ‹This theorem already exists as theroem @{thm [source] Nitpick.rtranclp_unfold} (and
sledgehammer uses it), but it makes sense to duplicate it, because it is unclear how stable the
lemmas in the @{file ‹~~/src/HOL/Nitpick.thy›} theory are.›
lemma rtranclp_unfold: ‹rtranclp r a b ⟷ (a = b ∨ tranclp r a b)›
by (meson rtranclp.simps rtranclpD tranclp_into_rtranclp)
lemma tranclp_unfold_end: ‹tranclp r a b ⟷ (∃a'. rtranclp r a a' ∧ r a' b)›
by (metis rtranclp.rtrancl_refl rtranclp_into_tranclp1 tranclp.cases tranclp_into_rtranclp)
text ‹Near duplicate of theorem @{thm [source] tranclpD}:›
lemma tranclp_unfold_begin: ‹tranclp r a b ⟷ (∃a'. r a a' ∧ rtranclp r a' b)›
by (meson rtranclp_into_tranclp2 tranclpD)
lemma trancl_set_tranclp: ‹(a, b) ∈ {(b,a). P a b}⇧+ ⟷ P⇧+⇧+ b a›
apply (rule iffI)
apply (induction rule: trancl_induct; simp)
apply (induction rule: tranclp_induct; auto simp: trancl_into_trancl2)
done
lemma tranclp_rtranclp_rtranclp_rel: ‹R⇧+⇧+⇧*⇧* a b ⟷ R⇧*⇧* a b›
by (simp add: rtranclp_unfold)
lemma tranclp_rtranclp_rtranclp[simp]: ‹R⇧+⇧+⇧*⇧* = R⇧*⇧*›
by (fastforce simp: rtranclp_unfold)
lemma rtranclp_exists_last_with_prop:
assumes ‹R x z› and ‹R⇧*⇧* z z'› and ‹P x z›
shows ‹∃y y'. R⇧*⇧* x y ∧ R y y' ∧ P y y' ∧ (λa b. R a b ∧ ¬P a b)⇧*⇧* y' z'›
using assms(2,1,3)
proof induction
case base
then show ?case by auto
next
case (step z' z'') note z = this(2) and IH = this(3)[OF this(4-5)]
show ?case
apply (cases ‹P z' z''›)
apply (rule exI[of _ z'], rule exI[of _ z''])
using z assms(1) step.hyps(1) step.prems(2) apply (auto; fail)[1]
using IH z by (fastforce intro: rtranclp.rtrancl_into_rtrancl)
qed
lemma rtranclp_and_rtranclp_left: ‹(λ a b. P a b ∧ Q a b)⇧*⇧* S T ⟹ P⇧*⇧* S T›
by (induction rule: rtranclp_induct) auto
subsection ‹Full Transitions›
paragraph ‹Definition›
text ‹We define here predicates to define properties after all possible transitions.›
abbreviation (input) no_step :: "('a ⇒ 'b ⇒ bool) ⇒ 'a ⇒ bool" where
"no_step step S ≡ ∀S'. ¬step S S'"
definition full1 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" where
"full1 transf = (λS S'. tranclp transf S S' ∧ no_step transf S')"
definition full:: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" where
"full transf = (λS S'. rtranclp transf S S' ∧ no_step transf S')"
text ‹We define output notations only for printing (to ease reading):›
notation (output) full1 ("_⇧+⇧↓")
notation (output) full ("_⇧↓")
paragraph ‹Some Properties›
lemma rtranclp_full1I:
‹R⇧*⇧* a b ⟹ full1 R b c ⟹ full1 R a c›
unfolding full1_def by auto
lemma tranclp_full1I:
‹R⇧+⇧+ a b ⟹ full1 R b c ⟹ full1 R a c›
unfolding full1_def by auto
lemma rtranclp_fullI:
‹R⇧*⇧* a b ⟹ full R b c ⟹ full R a c›
unfolding full_def by auto
lemma tranclp_full_full1I:
‹R⇧+⇧+ a b ⟹ full R b c ⟹ full1 R a c›
unfolding full_def full1_def by auto
lemma full_fullI:
‹R a b ⟹ full R b c ⟹ full1 R a c›
unfolding full_def full1_def by auto
lemma full_unfold:
‹full r S S' ⟷ ((S = S' ∧ no_step r S') ∨ full1 r S S')›
unfolding full_def full1_def by (auto simp add: rtranclp_unfold)
lemma full1_is_full[intro]: ‹full1 R S T ⟹ full R S T›
by (simp add: full_unfold)
lemma not_full1_rtranclp_relation: "¬full1 R⇧*⇧* a b"
by (auto simp: full1_def)
lemma not_full_rtranclp_relation: "¬full R⇧*⇧* a b"
by (auto simp: full_def)
lemma full1_tranclp_relation_full:
‹full1 R⇧+⇧+ a b ⟷ full1 R a b›
by (metis converse_tranclpE full1_def reflclp_tranclp rtranclpD rtranclp_idemp rtranclp_reflclp
tranclp.r_into_trancl tranclp_into_rtranclp)
lemma full_tranclp_relation_full:
‹full R⇧+⇧+ a b ⟷ full R a b›
by (metis full_unfold full1_tranclp_relation_full tranclp.r_into_trancl tranclpD)
lemma tranclp_full1_full1:
‹(full1 R)⇧+⇧+ a b ⟷ full1 R a b›
by (metis (mono_tags) full1_def predicate2I tranclp.r_into_trancl tranclp_idemp
tranclp_mono_explicit tranclp_unfold_end)
lemma rtranclp_full1_eq_or_full1:
‹(full1 R)⇧*⇧* a b ⟷ (a = b ∨ full1 R a b)›
unfolding rtranclp_unfold tranclp_full1_full1 by simp
lemma no_step_full_iff_eq:
‹no_step R S ⟹ full R S T ⟷ S = T›
unfolding full_def
by (meson rtranclp.rtrancl_refl rtranclpD tranclpD)
subsection ‹Well-Foundedness and Full Transitions›
lemma wf_exists_normal_form:
assumes wf: ‹wf {(x, y). R y x}›
shows ‹∃b. R⇧*⇧* a b ∧ no_step R b›
proof (rule ccontr)
assume ‹¬ ?thesis›
then have H: ‹⋀b. ¬ R⇧*⇧* a b ∨ ¬no_step R b›
by blast
define F where ‹F = rec_nat a (λi b. SOME c. R b c)›
have [simp]: ‹F 0 = a›
unfolding F_def by auto
have [simp]: ‹⋀i. F (Suc i) = (SOME b. R (F i) b)›
unfolding F_def by simp
{ fix i
have ‹∀j<i. R (F j) (F (Suc j))›
proof (induction i)
case 0
then show ?case by auto
next
case (Suc i)
then have ‹R⇧*⇧* a (F i)›
by (induction i) auto
then have ‹R (F i) (SOME b. R (F i) b)›
using H by (simp add: someI_ex)
then have ‹∀j < Suc i. R (F j) (F (Suc j))›
using H Suc by (simp add: less_Suc_eq)
then show ?case by fast
qed
}
then have ‹∀j. R (F j) (F (Suc j))› by blast
then show False
using wf unfolding wfP_def wf_iff_no_infinite_down_chain by blast
qed
lemma wf_exists_normal_form_full:
assumes wf: ‹wf {(x, y). R y x}›
shows ‹∃b. full R a b›
using wf_exists_normal_form[OF assms] unfolding full_def by blast
subsection ‹More Well-Foundedness›
text ‹A little list of theorems that could be useful, but are hidden:
▪ link between @{term wf} and infinite chains: theorems
@{thm [source] wf_iff_no_infinite_down_chain} and @{thm [source] wf_no_infinite_down_chainE}.›
lemma wf_if_measure_in_wf:
‹wf R ⟹ (⋀a b. (a, b) ∈ S ⟹ (ν a, ν b)∈R) ⟹ wf S›
by (metis in_inv_image wfE_min wfI_min wf_inv_image)
lemma wfP_if_measure: fixes f :: ‹'a ⇒ nat›
shows ‹(⋀x y. P x ⟹ g x y ⟹ f y < f x) ⟹ wf {(y,x). P x ∧ g x y}›
apply (insert wf_measure[of f])
apply (simp only: measure_def inv_image_def less_than_def less_eq)
apply (erule wf_subset)
apply auto
done
lemma wf_if_measure_f:
assumes ‹wf r›
shows ‹wf {(b, a). (f b, f a) ∈ r}›
using assms by (metis inv_image_def wf_inv_image)
lemma wf_wf_if_measure':
assumes ‹wf r› and H: ‹⋀x y. P x ⟹ g x y ⟹ (f y, f x) ∈ r›
shows ‹wf {(y,x). P x ∧ g x y}›
proof -
have ‹wf {(b, a). (f b, f a) ∈ r}› using assms(1) wf_if_measure_f by auto
then have ‹wf {(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r}›
using wf_subset[of _ ‹{(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r}›] by auto
moreover have ‹{(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r} ⊆ {(b, a). (f b, f a) ∈ r}› by auto
moreover have ‹{(b, a). P a ∧ g a b ∧ (f b, f a) ∈ r} = {(b, a). P a ∧ g a b}› using H by auto
ultimately show ?thesis using wf_subset by simp
qed
lemma wf_lex_less: ‹wf (lex less_than)›
by (auto simp: wf_less)
lemma wfP_if_measure2: fixes f :: ‹'a ⇒ nat›
shows ‹(⋀x y. P x y ⟹ g x y ⟹ f x < f y) ⟹ wf {(x,y). P x y ∧ g x y}›
apply (insert wf_measure[of f])
apply (simp only: measure_def inv_image_def less_than_def less_eq)
apply (erule wf_subset)
apply auto
done
lemma lexord_on_finite_set_is_wf:
assumes
P_finite: ‹⋀U. P U ⟶ U ∈ A› and
finite: ‹finite A› and
wf: ‹wf R› and
trans: ‹trans R›
shows ‹wf {(T, S). (P S ∧ P T) ∧ (T, S) ∈ lexord R}›
proof (rule wfP_if_measure2)
fix T S
assume P: ‹P S ∧ P T› and
s_le_t: ‹(T, S) ∈ lexord R›
let ?f = ‹λS. {U. (U, S) ∈ lexord R ∧ P U ∧ P S}›
have ‹?f T ⊆ ?f S›
using s_le_t P lexord_trans trans by auto
moreover have ‹T ∈ ?f S›
using s_le_t P by auto
moreover have ‹T ∉ ?f T›
using s_le_t by (auto simp add: lexord_irreflexive local.wf)
ultimately have ‹{U. (U, T) ∈ lexord R ∧ P U ∧ P T} ⊂ {U. (U, S) ∈ lexord R ∧ P U ∧ P S}›
by auto
moreover have ‹finite {U. (U, S) ∈ lexord R ∧ P U ∧ P S}›
using finite by (metis (no_types, lifting) P_finite finite_subset mem_Collect_eq subsetI)
ultimately show ‹card (?f T) < card (?f S)› by (simp add: psubset_card_mono)
qed
lemma wf_fst_wf_pair:
assumes ‹wf {(M', M). R M' M} ›
shows ‹wf {((M', N'), (M, N)). R M' M}›
proof -
have ‹wf ({(M', M). R M' M} <*lex*> {})›
using assms by auto
then show ?thesis
by (rule wf_subset) auto
qed
lemma wf_snd_wf_pair:
assumes ‹wf {(M', M). R M' M} ›
shows ‹wf {((M', N'), (M, N)). R N' N}›
proof -
have wf: ‹wf {((M', N'), (M, N)). R M' M}›
using assms wf_fst_wf_pair by auto
then have wf: ‹⋀P. (∀x. (∀y. (y, x) ∈ {((M', N'), M, N). R M' M} ⟶ P y) ⟶ P x) ⟹ All P›
unfolding wf_def by auto
show ?thesis
unfolding wf_def
proof (intro allI impI)
fix P :: ‹'c × 'a ⇒ bool› and x :: ‹'c × 'a›
assume H: ‹∀x. (∀y. (y, x) ∈ {((M', N'), M, y). R N' y} ⟶ P y) ⟶ P x›
obtain a b where x: ‹x = (a, b)› by (cases x)
have P: ‹P x = (P ∘ (λ(a, b). (b, a))) (b, a)›
unfolding x by auto
show ‹P x›
using wf[of ‹P o (λ(a, b). (b, a))›] apply rule
using H apply simp
unfolding P by blast
qed
qed
lemma wf_if_measure_f_notation2:
assumes ‹wf r›
shows ‹wf {(b, h a)|b a. (f b, f (h a)) ∈ r}›
apply (rule wf_subset)
using wf_if_measure_f[OF assms, of f] by auto
lemma wf_wf_if_measure'_notation2:
assumes ‹wf r› and H: ‹⋀x y. P x ⟹ g x y ⟹ (f y, f (h x)) ∈ r›
shows ‹wf {(y,h x)| y x. P x ∧ g x y}›
proof -
have ‹wf {(b, h a)|b a. (f b, f (h a)) ∈ r}› using assms(1) wf_if_measure_f_notation2 by auto
then have ‹wf {(b, h a)|b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r}›
using wf_subset[of _ ‹{(b, h a)| b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r}›] by auto
moreover have ‹{(b, h a)|b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r}
⊆ {(b, h a)|b a. (f b, f (h a)) ∈ r}› by auto
moreover have ‹{(b, h a)|b a. P a ∧ g a b ∧ (f b, f (h a)) ∈ r} = {(b, h a)|b a. P a ∧ g a b}›
using H by auto
ultimately show ?thesis using wf_subset by simp
qed
lemma power_ex_decomp:
assumes ‹(R^^n) S T›
shows
‹∃f. f 0 = S ∧ f n = T ∧ (∀i. i < n ⟶ R (f i) (f (Suc i)))›
using assms
proof (induction n arbitrary: T)
case 0
then show ‹?case› by auto
next
case (Suc n) note IH = this(1) and R = this(2)
from R obtain T' where
ST: ‹(R^^n) S T'› and
T'T: ‹R T' T›
by auto
obtain f where
[simp]: ‹f 0 = S› and
[simp]: ‹f n = T'› and
H: ‹⋀i. i < n ⟹ R (f i) (f (Suc i))›
using IH[OF ST] by fast
let ?f = ‹f(Suc n := T)›
show ?case
by (rule exI[of _ ?f])
(use H ST T'T in auto)
qed
text ‹The following lemma gives a bound on the maximal number of transitions of a sequence that is well-founded
under the lexicographic ordering \<^term>‹lexn› on natural numbers.
›
lemma lexn_number_of_transition:
assumes
le: ‹⋀i. i < n ⟹ ((f (Suc i)), (f i)) ∈ lexn less_than m› and
upper: ‹⋀i j. i ≤ n ⟹ j < m ⟹ (f i) ! j ∈ {0..<k}› and
‹finite A› and
k: ‹k > 1›
shows ‹n < k ^ Suc m›
proof -
define r where
‹r x = zip x (map (λi. k ^ (length x -i)) [0..<length x])› for x :: ‹nat list›
define s where
‹s x = foldr (λa b. a + b) (map (λ(a, b). a * b) x) 0› for x :: ‹(nat × nat) list›
have [simp]: ‹r [] = []› ‹s [] = 0›
by (auto simp: r_def s_def)
have upt': ‹m > 0 ⟹ [0..< m] = 0 # map Suc [0..< m - 1]› for m
by (auto simp: map_Suc_upt upt_conv_Cons)
have upt'': ‹m > 0 ⟹ [0..< m] = [0..< m - 1] @ [m-1]› for m
by (cases m) (auto simp: )
have Cons: ‹r (x # xs) = (x, k^(Suc (length xs))) # (r xs)› for x xs
unfolding r_def
apply (subst upt')
apply (clarsimp simp add: upt'' comp_def nth_append Suc_diff_le simp flip: zip_map2)
apply (clarsimp simp add: upt'' comp_def nth_append Suc_diff_le simp flip: zip_map2)
done
have [simp]: ‹s (ab # xs) = fst ab * snd ab + s xs› for ab xs
unfolding s_def by (cases ab) auto
have le2: ‹(∀a ∈ set b. a < k) ⟹ (k ^ (Suc (length b))) > s ((r b))› for b
apply (induction b arbitrary: f)
using k apply (auto simp: Cons)
apply (rule order.strict_trans1)
apply (rule_tac j = ‹(k - 1) * k *k ^ length b› in Nat.add_le_mono1)
subgoal for a b
by auto
apply (rule order.strict_trans2)
apply (rule_tac b = ‹(k - 1) * k * k ^ length b› and d = ‹(k * k ^ length b)› in add_le_less_mono)
apply (auto simp: mult.assoc comm_semiring_1_class.semiring_normalization_rules(2))
done
have ‹s (r (f (Suc i))) < s (r (f i))› if ‹i < n› for i
proof -
have i_n: ‹Suc i ≤ n› ‹i ≤ n›
using that by auto
have length: ‹length (f i) = m› ‹length (f (Suc i)) = m›
using le[OF that] by (auto dest: lexn_length)
define xs and ys where ‹xs = f i› and ‹ys = f (Suc i)›
show ?thesis
using le[OF that] upper[OF i_n(2)] upper[OF i_n(1)] length Cons
unfolding xs_def[symmetric] ys_def[symmetric]
proof (induction m arbitrary: xs ys)
case 0 then show ?case by auto
next
case (Suc m) note IH = this(1) and H = this(2) and p = this(3-)
have IH: ‹(tl ys, tl xs) ∈ lexn less_than m ⟹ s (r (tl ys)) < s (r (tl xs))›
apply (rule IH)
subgoal by auto
subgoal for i using p(1)[of ‹Suc i›] p by (cases xs; auto)
subgoal for i using p(2)[of ‹Suc i›] p by (cases ys; auto)
subgoal using p by (cases xs) auto
subgoal using p by auto
subgoal using p by auto
done
have ‹s (r (tl ys)) < k ^ (Suc (length (tl ys)))›
apply (rule le2)
unfolding all_set_conv_all_nth
using p by (simp add: nth_tl)
then have ‹ab * (k * k ^ length (tl ys)) + s (r (tl ys)) <
ab * (k * k ^ length (tl ys)) + (k * k ^ length (tl ys))› for ab
by auto
also have ‹… ab ≤ (ab + 1) * (k * k ^ length (tl ys))› for ab
by auto
finally have less: ‹ab < ac ⟹ ab * (k * k ^ length (tl ys)) + s (r (tl ys)) <
ac * (k * k ^ length (tl ys))› for ab ac
proof -
assume a1: "⋀ab. ab * (k * k ^ length (tl ys)) + s (r (tl ys)) <
(ab + 1) * (k * k ^ length (tl ys))"
assume "ab < ac"
then have "¬ ac * (k * k ^ length (tl ys)) < (ab + 1) * (k * k ^ length (tl ys))"
by (metis (no_types) One_nat_def Suc_leI add.right_neutral add_Suc_right
mult_less_cancel2 not_less)
then show ?thesis
using a1 by (meson le_less_trans not_less)
qed
have ‹ab < ac ⟹
ab * (k * k ^ length (tl ys)) + s (r (tl ys))
< ac * (k * k ^ length (tl xs)) + s (r (tl xs))› for ab ac
using less[of ab ac] p by auto
then show ?case
apply (cases xs; cases ys)
using IH H p(3-5) by auto
qed
qed
then have ‹i≤n ⟹ s (r (f i)) + i ≤ s (r (f 0))› for i
apply (induction i)
subgoal by auto
subgoal premises p for i
using p(3)[of ‹i-1›] p(1,2)
apply auto
by (meson Nat.le_diff_conv2 Suc_leI Suc_le_lessD add_leD2 less_diff_conv less_le_trans p(3))
done
from this[of n] show ‹n < k ^ Suc m›
using le2[of ‹f 0›] upper[of 0] k
using le[of 0] apply (cases ‹n = 0›)
by (auto dest!: lexn_length simp: all_set_conv_all_nth eq_commute[of _ m])
qed
end