Theory Auxiliary

section "Some Auxiliary Results"

theory Auxiliary imports Main
begin

lemma disjE3: "P ∨ Q ∨ R ⟹ (P ⟹ S) ⟹ (Q ⟹ S) ⟹ (R ⟹ S) ⟹ S" by auto

lemma ge_induct[consumes 1, case_names step]:
  fixes i::nat and j::nat and P::"nat ⇒ bool"
  shows "i ≤ j ⟹ (⋀n. i ≤ n ⟹ ((∀m ≥ i.  m<n ⟶ P m) ⟹ P n)) ⟹ P j"
proof -
  assume a0: "i ≤ j" and a1: "(⋀n. i ≤ n ⟹ ((∀m ≥ i.  m<n ⟶ P m) ⟹ P n))"
  have "(⋀n. ∀m<n. i ≤ m ⟶ P m ⟹ i ≤ n ⟶ P n)"
  proof
    fix n
    assume a2: "∀m<n. i ≤ m ⟶ P m"
    show "i ≤ n ⟹ P n"
    proof -
      assume "i ≤ n"
      with a1 have "(∀m ≥ i.  m<n ⟶ P m) ⟹ P n" by simp
      moreover from a2 have "∀m ≥ i.  m<n ⟶ P m" by simp
      ultimately show "P n" by simp
    qed
  qed
  with nat_less_induct[of "λj. i ≤ j ⟶ P j" j] have "i ≤ j ⟶ P j" .
  with a0 show ?thesis by simp
qed

lemma my_induct[consumes 1, case_names base step]:
  fixes P::"nat⇒bool"
assumes less: "i ≤ j"
    and base: "P j"
    and step: "⋀n. i ≤ n ⟹ n < j ⟹ (∀n'>n. n'≤j ⟶ P n') ⟹ P n"
  shows "P i"
proof cases
  assume "j=0"
  thus ?thesis using less base by simp
next
  assume "¬ j=0"
  have "j - (j - i) ≥ i ⟶ P (j - (j - i))"
  proof (rule less_induct[of "λn::nat. j-n ≥ i ⟶ P (j-n)" "j-i"])
    fix x assume asmp: "⋀y. y < x ⟹ i ≤ j - y ⟶ P (j - y)"
    show "i ≤ j - x ⟶ P (j - x)"
    proof cases
      assume "x=0"
      with base show ?thesis by simp
    next
      assume "¬ x=0"
      with ‹j ≠ 0› have "j - x < j" by simp
      show ?thesis
      proof
        assume "i ≤ j - x"
        moreover have "∀n'>j-x. n'≤j ⟶ P n'"
        proof
          fix n'
          show "n'>j-x ⟶ n'≤j ⟶ P n'"
          proof (rule HOL.impI[OF HOL.impI])
            assume "j - x < n'" and "n' ≤ j"
            hence "j - n' < x" by simp
            moreover from ‹i ≤ j - x› ‹j - x < n'› have "i ≤ n'" using le_less_trans less_imp_le_nat by blast
            with ‹n' ≤ j› have "i ≤ j - (j - n')" by simp
            ultimately have  "P (j - (j - n'))" using asmp by simp
            moreover from ‹n' ≤ j› have "j - (j - n') = n'" by simp
            ultimately show "P n'" by simp
          qed
        qed
        ultimately show "P (j - x)" using ‹j-x<j› step[of "j-x"] by simp
      qed
    qed
  qed
  moreover from less have "j - (j - i) = i" by simp
  ultimately show ?thesis by simp
qed

lemma Greatest_ex_le_nat: assumes "∃k. P k ∧ (∀k'. P k' ⟶ k' ≤ k)" shows "¬(∃n'>Greatest P. P n')"
  by (metis Greatest_equality assms less_le_not_le)

lemma cardEx: assumes "finite A" and "finite B" and "card A > card B" shows "∃x∈A. ¬ x∈B"
proof cases
  assume "A ⊆ B"
  with assms have "card A≤card B" using card_mono by blast
  with assms have False by simp
  thus ?thesis by simp
next
  assume "¬ A ⊆ B" 
  thus ?thesis by auto
qed

lemma cardshift: "card {i::nat. i>n ∧ i ≤ n' ∧ p (n'' + i)} = card {i. i>(n + n'') ∧ i ≤ (n' + n'') ∧ p i}"
proof -
  let ?f="λi. i+n''"
  have "bij_betw ?f {i::nat. i>n ∧ i ≤ n' ∧ p (n'' + i)} {i. i>(n + n'') ∧ i ≤ (n' + n'') ∧ p i}"
  proof (rule bij_betwI')
    fix x y assume "x ∈ {i. n < i ∧ i ≤ n' ∧ p (n'' + i)}" and "y ∈ {i. n < i ∧ i ≤ n' ∧ p (n'' + i)}"
    show "(x + n'' = y + n'') = (x = y)" by simp
  next
    fix x::nat assume "x ∈ {i. n < i ∧ i ≤ n' ∧ p (n'' + i)}"
    hence "n<x" and "x ≤ n'" and "p(n''+x)" by auto
    moreover have "n''+x=x+n''" by simp
    ultimately have "n + n'' < x + n''" and "x + n'' ≤ n' + n''" and "p (x + n'')" by auto
    thus "x + n'' ∈ {i. n + n'' < i ∧ i ≤ n' + n'' ∧ p i}" by auto
  next
    fix y::nat assume "y ∈ {i. n + n'' < i ∧ i ≤ n' + n'' ∧ p i}"
    hence "n+n''<y" and "y≤n'+n''" and "p y" by auto
    then obtain x where "x=y-n''" by simp
    with ‹n+n''<y› have "y=x+n''" by simp
    moreover from ‹x=y-n''› ‹n+n''<y› have "x>n" by simp
    moreover from ‹x=y-n''› ‹y≤n'+n''› have "x≤n'" by simp
    moreover from ‹y=x+n''› have "y=n''+x" by simp
    with ‹p y› have "p (n'' + x)" by simp
    ultimately show "∃x∈{i. n < i ∧ i ≤ n' ∧ p (n'' + i)}. y = x + n''" by auto
  qed
  thus ?thesis using bij_betw_same_card by auto
qed

end