Theory Bounded_Quantifiers

✐‹creator "Kevin Kappelmann"›
subsection ‹Bounded Quantifiers›
theory Bounded_Quantifiers
  imports
    HOL_Basics_Base
    Predicates_Lattice
    ML_Unification.ML_Unification_HOL_Setup
begin

consts ball :: "'a ⇒ ('b ⇒ bool) ⇒ bool"

open_bundle ball_syntax
begin
notation ball (‹∀(⇘_⇙)›)
syntax
  "_ball"  :: ‹[pttrns, 'a, bool] ⇒ bool› (‹(2∀_ : _./ _)› 10)
syntax_consts
  "_ball" ⇌ ball
translations
  "∀x xs : P. Q" ⇀ "CONST ball P (λx. ∀xs : P. Q)"
  "∀x : P. Q" ⇌ "CONST ball P (λx. Q)"
end

consts bex :: "'a ⇒ ('b ⇒ bool) ⇒ bool"

open_bundle bex_syntax
begin
notation bex (‹∃(⇘_⇙)›)
syntax
  "_bex"  :: ‹[pttrns, 'a, bool] ⇒ bool› (‹(2∃_ : _./ _)› 10)
syntax_consts
  "_bex" ⇌ bex
translations
  "∃x xs : P. Q" ⇀ "CONST bex P (λx. ∃xs : P. Q)"
  "∃x : P. Q" ⇌ "CONST bex P (λx. Q)"
end

consts bex1 :: "'a ⇒ ('b ⇒ bool) ⇒ bool"

open_bundle bex1_syntax
begin
notation bex1 (‹∃!(⇘_⇙)›)
syntax
  "_bex1"  :: ‹[pttrns, 'a, bool] ⇒ bool› (‹(2∃!_ : _./ _)› 10)
syntax_consts
  "_bex1" ⇌ bex1
translations
  "∃!x xs : P. Q" ⇀ "CONST bex1 P (λx. ∃!xs : P. Q)"
  "∃!x : P. Q" ⇌ "CONST bex1 P (λx. Q)"
end

bundle bounded_quantifier_syntax
begin
unbundle ball_syntax and bex_syntax and bex1_syntax
end

definition "ball_pred P Q ≡ ∀x. P x ⟶ Q x"
adhoc_overloading ball ⇌ ball_pred

definition "bex_pred P Q ≡ ∃x. P x ∧ Q x"
adhoc_overloading bex ⇌ bex_pred

definition "bex1_pred P Q ≡ ∃!x. P x ∧ Q x"
adhoc_overloading bex1 ⇌ bex1_pred

(*copied from HOL.Set.thy*)
simproc_setup defined_ball ("∀x : P. Q x ⟶ U x") = ‹
  K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms ball_pred_def}))
›
simproc_setup defined_bex ("∃x : P. Q x ∧ U x") = ‹
  K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms bex_pred_def}))
›

lemma ballI [intro!]:
  assumes "⋀x. P x ⟹ Q x"
  shows "∀x : P. Q x"
  using assms unfolding ball_pred_def by blast

lemma ballE [elim]:
  assumes "∀x : P. Q x"
  obtains "⋀x. P x ⟹ Q x"
  using assms unfolding ball_pred_def by blast

lemma ballE':
  assumes "∀x : P. Q x"
  obtains "¬(P x)" | "P x" "Q x"
  using assms by blast

lemma ballD: "∀x : P. Q x ⟹ P x ⟹ Q x"
  by blast

lemma ball_cong: "⟦P = P'; ⋀x. P' x ⟹ Q x ⟷ Q' x⟧ ⟹ (∀x : P. Q x) ⟷ (∀x : P'. Q' x)"
  by auto

lemma ball_cong_simp [cong]:
  "⟦P = P'; ⋀x. P' x =simp=> Q x ⟷ Q' x⟧ ⟹ (∀x : P. Q x) ⟷ (∀x : P'. Q' x)"
  unfolding simp_implies_def by (rule ball_cong)

(*copied from HOL.Set.thy*)
ML ‹
structure Simpdata =
struct
  open Simpdata
  val mksimps_pairs = [(\<^const_name>‹ball_pred›, @{thms ballD})] @ mksimps_pairs
end
open Simpdata
›
declaration ‹K (Simplifier.map_simpset (Simplifier.set_mksimps (mksimps mksimps_pairs)))›

lemma atomize_ball: "(⋀x. P x ⟹ Q x) ≡ Trueprop (∀x : P. Q x)"
  by (simp only: ball_pred_def atomize_all atomize_imp)

declare atomize_ball[symmetric, rulify]
declare atomize_ball[symmetric, defn]

lemma bexI [intro!]:
  (*better argument order: Q often determines the choice for x*)
  assumes "∃x. Q x ∧ P x"
  shows "∃x : P. Q x"
  using assms unfolding bex_pred_def by blast

lemma bexE [elim!]:
  assumes "∃x : P. Q x"
  obtains x where "P x" "Q x"
  using assms unfolding bex_pred_def by blast

lemma bexD:
  assumes "∃x : P. Q x"
  shows "∃x. P x ∧ Q x"
  using assms by blast

lemma bex_cong:
  "⟦P = P'; ⋀x. P' x ⟹ Q x ⟷ Q' x⟧ ⟹ (∃x : P. Q x) ⟷ (∃x : P'. Q' x)"
  by blast

lemma bex_cong_simp [cong]:
  "⟦P = P'; ⋀x. P' x =simp=> Q x ⟷ Q' x⟧ ⟹ (∃x : P. Q x) ⟷ (∃x : P'. Q' x)"
  unfolding simp_implies_def by (rule bex_cong)

lemma bex1I [intro]:
  (*better argument order: Q often determines the choice for x*)
  assumes "∃!x. Q x ∧ P x"
  shows "∃!x : P. Q x"
  using assms unfolding bex1_pred_def by blast

lemma bex1D [dest!]:
  assumes "∃!x : P. Q x"
  shows "∃!x. P x ∧ Q x"
  using assms unfolding bex1_pred_def by blast

lemma bex1_cong: "⟦P = P'; ⋀x. P x ⟹ Q x ⟷ Q' x⟧ ⟹ (∃!x : P. Q x) ⟷ (∃!x : P'. Q' x)"
  by blast

lemma bex1_cong_simp [cong]:
  "⟦P = P'; ⋀x. P x =simp=> Q x ⟷ Q' x⟧ ⟹ (∃!x : P. Q x) ⟷ (∃!x : P'. Q' x)"
  unfolding simp_implies_def by (rule bex1_cong)

lemma ball_iff_ex_pred [iff]: "(∀x : P. Q) ⟷ ((∃x. P x) ⟶ Q)"
  by auto

lemma bex_iff_ex_and [iff]: "(∃x : P. Q) ⟷ ((∃x. P x) ∧ Q)"
  by blast

lemma ball_eq_imp_iff_imp [iff]: "(∀x : P. x = y ⟶ Q x) ⟷ (P y ⟶ Q y)"
  by blast

lemma ball_eq_imp_iff_imp' [iff]: "(∀x : P. y = x ⟶ Q x) ⟷ (P y ⟶ Q y)"
  by blast

lemma bex_eq_iff_pred [iff]: "(∃x : P. x = y) ⟷ P y"
  by blast

lemma bex_eq_iff_pred' [iff]: "(∃x : P. y = x) ⟷ P y"
  by blast

lemma bex_eq_and_iff_pred [iff]: "(∃x : P. x = y ∧ Q x) ⟷ P y ∧ Q y"
  by blast

lemma bex_eq_and_iff_pred' [iff]: "(∃x : P. y = x ∧ Q x) ⟷ P y ∧ Q y"
  by blast

lemma ball_and_iff_ball_and_ball: "(∀x : P. Q x ∧ U x) ⟷ (∀x : P. Q x) ∧ (∀x : P. U x)"
  by auto

lemma bex_or_iff_bex_or_bex: "(∃x : P. Q x ∨ U x) ⟷ (∃x : P. Q x) ∨ (∃x : P. U x)"
  by auto

lemma ball_or_iff_ball_or [iff]: "(∀x : P. Q x ∨ U) ⟷ ((∀x : P. Q x) ∨ U)"
  by auto

lemma ball_or_iff_or_ball [iff]: "(∀x : P. Q ∨ U x) ⟷ (Q ∨ (∀x : P. U x))"
  by auto

lemma ball_imp_iff_imp_ball [iff]: "(∀x : P. Q ⟶ U x) ⟷ (Q ⟶ (∀x : P. U x))"
  by auto

lemma bex_and_iff_bex_and [iff]: "(∃x : P. Q x ∧ U) ⟷ ((∃x : P. Q x) ∧ U)"
  by auto

lemma bex_and_iff_and_bex [iff]: "(∃x : P. Q ∧ U x) ⟷ (Q ∧ (∃x : P. U x))"
  by auto

lemma ball_imp_iff_bex_imp [iff]: "(∀x : P. Q x ⟶ U) ⟷ ((∃x : P. Q x) ⟶ U)"
  by auto

lemma not_ball_iff_bex_not [iff]: "(¬(∀x : P. Q x)) ⟷ (∃x : P. ¬(Q x))"
  by auto

lemma not_bex_iff_ball_not [iff]: "(¬(∃x : P. Q x)) ⟷ (∀x : P. ¬(Q x))"
  by auto

lemma bex1_iff_bex_and [iff]: "(∃!x : P. Q) ⟷ ((∃!x. P x) ∧ Q)"
  by auto

lemma ball_bottom_eq_top [simp]: "∀⇘⊥⇙ = ⊤" by auto
lemma bex_bottom_eq_bottom [simp]: "∃⇘⊥⇙ = ⊥" by fastforce
lemma bex1_bottom_eq_bottom [simp]: "∃!⇘⊥⇙ = ⊥" by fastforce

lemma ball_top_eq_all [simp]: "∀⇘⊤⇙ = All" by fastforce

lemma ball_top_eq_all_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "∀⇘P⇙ ≡ All"
  using assms by simp

lemma bex_top_eq_ex [simp]: "∃⇘⊤⇙ = Ex" by fastforce

lemma bex_top_eq_ex_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "∃⇘P⇙ ≡ Ex"
  using assms by simp

lemma bex1_top_eq_ex1 [simp]: "∃!⇘⊤⇙ = Ex1" by fastforce

lemma bex1_top_eq_ex1_uhint [uhint]:
  assumes "P ≡ (⊤ :: 'a ⇒ bool)"
  shows "∃!⇘P⇙ ≡ Ex1"
  using assms by simp

end