# Theory MiscLemmas

```section "Miscellaneous lemmas"

theory MiscLemmas imports "HOL-Library.Sublist" begin

inductive star :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl[simp,intro]: "star r x x"
| step: "r x y ⟹ star r y z ⟹ star r x z"

inductive star_n :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl_n: "star_n r 0 x x"
| step_n: "r x y ⟹ star_n r n y z ⟹ star_n r (Suc n) x z"

declare star_n.intros[simp, intro]

lemma star_n_decompose:
"star_n r n x y ⟹ star_n r n' x z ⟹ n' < n
⟹ (⋀x y z. r x y ⟹ r x z ⟹ y = z)
⟹ (⋀n x y z. star_n r n x y ⟹ star_n r n x z ⟹ y = z)
⟹ star_n r (n - n') z y"
apply (induct arbitrary: n' z rule: star_n.induct, simp)
apply clarsimp
apply (rename_tac n z n' za)
apply (subgoal_tac "Suc n - n' = Suc (n - n')")
prefer 2
apply simp
apply simp
apply (case_tac "n' < n", simp)
apply (case_tac n')
apply clarsimp
apply (erule star_n.cases[of _ 0]; simp)
apply (rename_tac z' m)
apply simp
apply (drule_tac x=m and y=z' in meta_spec2)
apply (subgoal_tac "Suc (n - Suc m) = n - m")
prefer 2
apply arith
apply simp
apply (erule meta_mp)
apply (erule_tac ?a1.0="Suc m" in star_n.cases; simp)
apply clarsimp
apply (rename_tac y n z x y' n' z')
apply (drule_tac x=x and y=y in meta_spec2)
apply (drule_tac x=y' in meta_spec)
apply simp
apply (subgoal_tac "n' = n")
prefer 2
apply arith
apply simp
apply (case_tac n; simp)
apply clarsimp
apply (erule star_n.cases; simp)
apply (erule star_n.cases; simp)
apply (rename_tac za m)
apply (drule_tac x="n - (Suc 0)" and y=za in meta_spec2)
apply simp
apply (erule meta_mp)
apply (drule_tac x=m and y=y in meta_spec2)
apply (rotate_tac -1)
apply (drule_tac x=z and y=za in meta_spec2)
apply (erule star_n.cases; simp)
apply (erule star_n.cases; simp)
by fastforce

"star_n r n x z ⟷ (∃n1 n2 y. star_n r n1 x y ∧ star_n r n2 y z ∧ n = n1 + n2)"
proof (rule iffI)
assume "star_n r n x z"
from this show "∃n1 n2 y. star_n r n1 x y ∧ star_n r n2 y z ∧ n = n1 + n2"
by (induct rule: star_n.induct; fastforce)
next
assume H0: "∃n1 n2 y. star_n r n1 x y ∧ star_n r n2 y z ∧ n = n1 + n2"
have H: "star_n r n1 x y ⟹
star_n r n2 y z ⟹ star_n r (n1 + n2) x z" for y n1 n2
by (induct rule: star_n.induct; simp)
show "star_n r n x z " using H0 H by blast
qed

lemma star_star_n:
"star r x y ⟹ ∃n. star_n r n x y"
by (induct rule: star.induct; fastforce)

lemma star_n_star:
"star_n r n x y ⟹ star r x y"
by (induct rule: star_n.induct; fastforce elim!: step)

lemma star_eq_star_n:
"star r x y = (∃n. star_n r n x y)"
by (meson star_n_star star_star_n)

lemma star_trans:
"star r x y ⟹ star r y z ⟹ star r x z"
by (meson star_eq_star_n star_n_add)

lemma step_rev:
"star r x y ⟹ r y z ⟹ star r x z"
by (meson star.simps star_trans)

lemma star_n_trans:
"star_n r n x y ⟹ star_n r n' y z ⟹ star_n r (n + n') x z"
using star_n_add by force

lemma step_n_rev:
"star_n r n x y ⟹ r y z ⟹ star_n r (Suc n) x z"
by (induct rule: star_n.induct; clarsimp)

lemma star_n_lastE:
"star_n r (Suc n) x z ⟹
(⋀n' x' y' z'. n = n' ⟹ x = x' ⟹ z = z'
⟹ star_n r n' x' y' ⟹ r y' z' ⟹ P) ⟹ P"
proof (induct n arbitrary: x z)
case 0
then show ?case
by cases (erule star_n.cases; force)
next
case (Suc n)
then show ?case
by cases (erule star_n.cases; force)+
qed

lemma
star_n_conjunct1: "star_n (λx y. P x y ∧ Q x y) n s t ⟹ star_n P n s t" and
star_n_conjunct2: "star_n (λx y. P x y ∧ Q x y) n s t ⟹ star_n Q n s t" and
star_n_commute: "star_n (λx y. P x y ∧ Q x y) n s t ⟹ star_n (λx y. Q x y ∧ P x y) n s t"
by (induct rule: star_n.induct; clarsimp)+

lemma forall_swap4:
"(∀x y z w. P x y z w) ⟷ (∀z w y x. P x y z w)" by auto

lemma prefix_drop_append:
"prefix xs ys ⟹ xs @ drop (length xs) ys = ys"
by (metis append_eq_conv_conj prefix_def)

lemma min_prefix:
"∀i. prefix (f i) (f (Suc i)) ⟹ (∀i. prefix (f 0) (f i))"
apply clarsimp
using prefix_order.lift_Suc_mono_le by blast

definition wf_to_wfP where
"wf_to_wfP r ≡ λx y. (x, y) ∈ r"

end```