Theory InductRules

theory InductRules
imports Main
begin

lemma disjCases2[consumes 1, case_names 1 2]:
  assumes AB: "A ∨ B"
  and AP: "A ⟹ P"
  and BP: "B ⟹ P"
  shows "P"
proof -
  from AB AP BP show ?thesis by blast
qed

lemma disjCases3[consumes 1, case_names 1 2 3]:
  assumes AB: "A ∨ B ∨ C"
  and AP: "A ⟹ P"
  and BP: "B ⟹ P"
  and CP: "C ⟹ P"
  shows "P"
proof -
  from AB AP BP CP show ?thesis by blast
qed

lemma disjCases4[consumes 1, case_names 1 2 3 4]:
  assumes AB: "A ∨ B ∨ C ∨ D"
  and AP: "A ⟹ P"
  and BP: "B ⟹ P"
  and CP: "C ⟹ P"
  and DP: "D ⟹ P"
  shows "P"
proof -
  from AB AP BP CP DP show ?thesis by blast
qed

lemma disjCases5[consumes 1, case_names 1 2 3 4 5]:
  assumes AB: "A ∨ B ∨ C ∨ D ∨ E"
  and AP: "A ⟹ P"
  and BP: "B ⟹ P"
  and CP: "C ⟹ P"
  and DP: "D ⟹ P"
  and EP: "E ⟹ P"
  shows "P"
proof -
  from AB AP BP CP DP EP show ?thesis by blast
qed

lemma minimal_witness_ex:
  assumes k: "P (k::nat)"
  shows "∃ k0. k0 ≤ k ∧ P k0 ∧ (∀ k. k < k0 ⟶ ¬ (P k))" 
proof -
  let ?K = "{ h. h ≤ k ∧ P h }" 
  have finite_K: "finite ?K" by auto
  have "k ∈ ?K" by (simp add: k)
  then have nonempty_K: "?K ≠ {}" by auto
  let ?k = "Min ?K"
  have witness: "?k ≤ k ∧ P ?k"
    by (metis (mono_tags, lifting) Min_in finite_K mem_Collect_eq nonempty_K)
  have minimal: "∀ h. h < ?k ⟶ ¬ (P h)" 
    by (metis Min_le witness dual_order.strict_implies_order 
        dual_order.trans finite_K leD mem_Collect_eq)
  from witness minimal show ?thesis by metis 
qed

lemma minimal_witness[consumes 1, case_names Minimal]:
  assumes "P (k::nat)"
  and "⋀ K. K ≤ k ⟹ P K ⟹ (⋀ k. k < K ⟹ ¬ (P k)) ⟹ Q"
  shows "Q"
proof -
  from assms minimal_witness_ex show ?thesis by metis
qed

lemma ex_minimal_witness[consumes 1, case_names Minimal]:
  assumes "∃ k. P (k::nat)"
  and "⋀ K. P K ⟹ (⋀ k. k < K ⟹ ¬ (P k)) ⟹ Q"
  shows "Q"
proof -
  from assms minimal_witness_ex show ?thesis by metis
qed

end