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