Quelle  HOL_Base.thy

(*
  File: HOL_Base.thy
  Author: Bohua Zhan

  Extra theorems in logic used by auto2.
*)

theory HOL_Base
  imports Main
begin

theorem to_contra_form: "Trueprop A ≡ (¬A ==> False)" by (rule equal_intr_rule) auto
theorem to_contra_form': "Trueprop (¬A) ≡ (A ==> False)" by (rule equal_intr_rule) auto

theorem contra_triv: "¬A ==> A ==> False" by simp
theorem or_intro1: "¬ (P ∨ Q) ==> ¬ P" by simp
theorem or_intro2: "¬ (P ∨ Q) ==> ¬ Q" by simp
theorem or_cancel1: "¬Q ==> (P ∨ Q) = P" by auto
theorem or_cancel2: "¬P ==> (P ∨ Q) = Q" by auto
theorem exE': "(∧x. P x ==> Q) ==> ∃x. P x ==> Q" by auto
theorem nn_create: "A ==> ¬¬A" by auto
theorem iffD: "A ⟷ B ==> (A ⟶ B) ∧ (B ⟶ A)" by auto

theorem obj_sym: "Trueprop (t = s) ≡ Trueprop (s = t)" by (rule equal_intr_rule) auto
theorem to_meta_eq: "Trueprop (t = s) ≡ (t ≡ s)" by (rule equal_intr_rule) auto

theorem inv_backward: "A ⟷ B ==> ¬A ==> ¬B" by auto
theorem backward_conv: "(A ==> B) ≡ (¬B ==> ¬A)" by (rule equal_intr_rule) auto
theorem backward1_conv: "(A ==> B ==> C) ≡ (¬C ==> B ==> ¬A)" by (rule equal_intr_rule) auto
theorem backward2_conv: "(A ==> B ==> C) ≡ (¬C ==> A ==> ¬B)" by (rule equal_intr_rule) auto
theorem resolve_conv: "(A ==> B) ≡ (¬B ==> A ==> False)" by (rule equal_intr_rule) auto

(* Quantifiers: swapping out of ALL or EX *)
theorem swap_ex_conj: "(P ∧ (∃x. Q x)) ⟷ (∃x. P ∧ Q x)" by auto
theorem swap_all_disj: "(P ∨ (∀x. Q x)) ⟷ (∀x. P ∨ Q x)" by auto

(* Use these instead of original versions to keep names in abstractions. *)
theorem Bex_def': "(∃x∈S. P x) ⟷ (∃x. x ∈ S ∧ P x)" by auto
theorem Ball_def': "(∀x∈S. P x) ⟷ (∀x. x ∈ S ⟶ P x)" by auto

(* Taking conjunction of assumptions *)
lemma atomize_conjL: "(A ==> B ==> PROP C) ≡ (A ∧ B ==> PROP C)" by (rule equal_intr_rule) auto

end