Theory HOL_Base

(*
  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