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

lemma star_n_add:
  "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