Quelle OrdQuant.thy
Sprache: Isabelle
(* Title: ZF/OrdQuant.thy
Authors: Krzysztof Grabczewski and L C Paulson
*)
section ‹ Special quantifiers›
theory OrdQuant
imports Ordinal
begin
subsection ‹ Quantifiers and union operator for ordinals›
definition
(* Ordinal Quantifiers *)
oall ::
"[i, i ==> ==> where
"oall(A, P) ≡ ∀ x. x⟶ P(x)"
definition
oex ::
"[i, i ==> ==> where
"oex(A, P) ≡ ∃ x. x∧ P(x)"
definition
(* Ordinal Union *)
OUnion ::
"[i, i ==> ==> where
"OUnion(i,B) ≡ {z: ∪ ∈ i. B(x). Ord(i)}"
syntax
"_oall" ::
"[idt, i, o] ==> (
‹ (‹ indent=3 notation=‹ binder ∀ 🚫 close>› \› 10)"_oex" :: "[idt, i, o] ==> (‹ (‹ indent=3 notation=‹ binder ∃ 🚫 close>› \∃ _🚫 / _)› 10)"_OUNION" :: "[idt, i, i] ==> (‹ (‹ indent=3 notation=‹ binder ∪ 🚫 close>› \∪ 🚫 / _) › 10)
syntax_consts
"_oall" ⇌ oall and
"_oex" ⇌ oex and
"_OUNION" ⇌ OUnion
translations
"∀ x🚫 P" ⇌ "CONST oall(a, λx. P)"
"∃ x🚫 P" ⇌ "CONST oex(a, λx. P)"
"∪ 🚫 B" ⇌ "CONST OUnion(a, λx. B)"
subsubsection ‹ simplification of the new quantifiers›
(*MOST IMPORTANT that this is added to the simpset BEFORE Ord_atomize
is proved. Ord_atomize would convert this rule to
x < 0 \<Longrightarrow> P(x) \<equiv> True, which causes dire effects!*)
lemma [simp]:
"(∀ x<0. P(x))"
by (simp add: oall_def)
lemma [simp]:
"¬ (∃ x<0. P(x))"
by (simp add: oex_def)
lemma [simp]:
"(∀ x (Ord(i) ⟶ P(i) ∧ (∀ xapply (simp add: oall_def le_iff)apply (blast intro: lt_Ord2)done lemma [simp]: "(∃ x (Ord(i) ∧ (P(i) | (∃ xapply (simp add: oex_def le_iff)apply (blast intro: lt_Ord2)done ‹ Union over ordinals› lemma Ord_OUN [intro,simp]:"[ ∧ ==> Ord(B(x))] ==> Ord(∪ by (simp add: OUnion_def ltI Ord_UN)lemma OUN_upper_lt:"[ a∪ x] ==> i < (∪ by (unfold OUnion_def lt_def, blast )lemma OUN_upper_le:"[ a≤ b(a); Ord(∪ ] ==> i
≤ (
∪ x
apply (unfold OUnion_def, auto)apply (rule UN_upper_le )apply (auto simp add: lt_def)done lemma Limit_OUN_eq: "Limit(i) ==> (∪ by (simp add: OUnion_def Limit_Union_eq Limit_is_Ord)(* No < version of this theorem: consider that @{term"(\<Union>i\<in>nat.i)=nat"}! *) lemma OUN_least:"(∧ ==> B(x) ⊆ C) ==> (∪ ⊆ C"by (simp add: OUnion_def UN_least ltI)lemma OUN_least_le:"[ Ord(i); ∧ ==> b(x) ≤ i] ==> (∪ ≤ i"by (simp add: OUnion_def UN_least_le ltI Ord_0_le)lemma le_implies_OUN_le_OUN:"[ ∧ ==> c(x) ≤ d(x)] ==> (∪ ≤ (∪ by (blast intro: OUN_least_le OUN_upper_le le_Ord2 Ord_OUN)lemma OUN_UN_eq:"(∧ ∈ A ==> Ord(B(x))) ==> (∪ ∪ ∈ A. B(x)). C(z)) = (∪ ∈ A. ∪ by (simp add: OUnion_def)lemma OUN_Union_eq:"(∧ ∈ X ==> Ord(x)) ==> (∪ ∪ ∪ ∈ X. ∪ by (simp add: OUnion_def)(*So that rule_format will get rid of this quantifier...*) lemma atomize_oall [symmetric, rulify]:"(∧ ==> P(x)) ≡ Trueprop (∀ xby (simp add: oall_def atomize_all atomize_imp)‹ universal quantifier for ordinals› lemma oallI [intro!]:"[ ∧ ==> P(x)] ==> ∀ xby (simp add: oall_def)lemma ospec: "[ ∀ x] ==> P(x)"by (simp add: oall_def)lemma oallE:"[ ∀ x==> Q; ¬ x==> Q] ==> Q"by (simp add: oall_def, blast)lemma rev_oallE [elim]:"[ ∀ x¬ x ==> Q; P(x) ==> Q] ==> Q"by (simp add: oall_def, blast)(*Trival rewrite rule. @{term"(\<forall>x<a.P)<->P"} holds only if a is not 0!*) lemma oall_simp [simp]: "(∀ x True" by blast(*Congruence rule for rewriting*) lemma oall_cong [cong]:"[ a=a'; ∧ ==> P(x) <-> P'(x)] ==> oall(a, λx. P(x)) <-> oall(a', λx. P'(x))" by (simp add: oall_def)‹ existential quantifier for ordinals› lemma oexI [intro]:"[ P(x); x] ==> ∃ xapply (simp add: oex_def, blast)done (*Not of the general form for such rules... *) lemma oexCI:"[ ∀ x¬ P(x) ==> P(a); a] ==> ∃ xapply (simp add: oex_def, blast)done lemma oexE [elim!]:"[ ∃ x∧ x. [ x] ==> Q] ==> Q"apply (simp add: oex_def, blast)done lemma oex_cong [cong]:"[ a=a'; ∧ ==> P(x) <-> P'(x)] ==> oex(a, λx. P(x)) <-> oex(a', λx. P'(x))" apply (simp add: oex_def cong add: conj_cong)done ‹ Rules for Ordinal-Indexed Unions› lemma OUN_I [intro]: "[ a∈ B(a)] ==> b: (∪ by (unfold OUnion_def lt_def, blast)lemma OUN_E [elim!]:"[ b ∈ (∪ ∧ a.[ b ∈ B(a); a] ==> R] ==> R"apply (unfold OUnion_def lt_def, blast)done lemma OUN_iff: "b ∈ (∪ (∃ x∈ B(x))"by (unfold OUnion_def oex_def lt_def, blast)lemma OUN_cong [cong]:"[ i=j; ∧ ==> C(x)=D(x)] ==> (∪ ∪ xby (simp add: OUnion_def lt_def OUN_iff)lemma lt_induct:"[ i∧ x.[ x∀y] ==> P(x)] ==> P(i)"apply (simp add: lt_def oall_def)apply (erule conjE)apply (erule Ord_induct, assumption, blast)done subsection ‹ Quantification over a class› definition "rall" :: "[i==> ==> ==> where "rall(M, P) ≡ ∀ x. M(x) ⟶ P(x)" definition "rex" :: "[i==> ==> ==> where "rex(M, P) ≡ ∃ x. M(x) ∧ P(x)" syntax "_rall" :: "[pttrn, i==> ==> (‹ (‹ indent=3 notation=‹ binder ∀ []› \∀ › 10)"_rex" :: "[pttrn, i==> ==> (‹ (‹ indent=3 notation=‹ binder ∃ []› \∃ › 10)"_rall" ⇌ rall and "_rex" ⇌ rextranslations "∀ x[M]. P" ⇌ "CONST rall(M, λx. P)" "∃ x[M]. P" ⇌ "CONST rex(M, λx. P)" ‹ Relativized universal quantifier› lemma rallI [intro!]: "[ ∧ ==> P(x)] ==> ∀ x[M]. P(x)" by (simp add: rall_def)lemma rspec: "[ ∀ x[M]. P(x); M(x)] ==> P(x)" by (simp add: rall_def)(*Instantiates x first: better for automatic theorem proving?*) lemma rev_rallE [elim]:"[ ∀ x[M]. P(x); ¬ M(x) ==> Q; P(x) ==> Q] ==> Q" by (simp add: rall_def, blast)lemma rallE: "[ ∀ x[M]. P(x); P(x) ==> Q; ¬ M(x) ==> Q] ==> Q" by blast(*Trival rewrite rule; (\<forall>x[M].P)<->P holds only if A is nonempty!*) lemma rall_triv [simp]: "(∀ x[M]. P) ⟷ ((∃ x. M(x)) ⟶ P)" by (simp add: rall_def)(*Congruence rule for rewriting*) lemma rall_cong [cong]:"(∧ ==> P(x) <-> P'(x)) ==> (∀ x[M]. P(x)) <-> (∀ x[M]. P'(x))" by (simp add: rall_def)‹ Relativized existential quantifier› lemma rexI [intro]: "[ P(x); M(x)] ==> ∃ x[M]. P(x)" by (simp add: rex_def, blast)(*The best argument order when there is only one M(x)*) lemma rev_rexI: "[ M(x); P(x)] ==> ∃ x[M]. P(x)" by blast(*Not of the general form for such rules... *) lemma rexCI: "[ ∀ x[M]. ¬ P(x) ==> P(a); M(a)] ==> ∃ x[M]. P(x)" by blastlemma rexE [elim!]: "[ ∃ x[M]. P(x); ∧ [ M(x); P(x)] ==> Q] ==> Q" by (simp add: rex_def, blast)(*We do not even have (\<exists>x[M]. True) <-> True unless A is nonempty\<And>*) lemma rex_triv [simp]: "(∃ x[M]. P) ⟷ ((∃ x. M(x)) ∧ P)" by (simp add: rex_def)lemma rex_cong [cong]:"(∧ ==> P(x) <-> P'(x)) ==> (∃ x[M]. P(x)) <-> (∃ x[M]. P'(x))" by (simp add: rex_def cong: conj_cong)lemma rall_is_ball [simp]: "(∀ x[λz. z∈ A]. P(x)) <-> (∀ x∈ A. P(x))" by blastlemma rex_is_bex [simp]: "(∃ x[λz. z∈ A]. P(x)) <-> (∃ x∈ A. P(x))" by blastlemma atomize_rall: "(∧ ==> P(x)) ≡ Trueprop (∀ x[M]. P(x))" by (simp add: rall_def atomize_all atomize_imp)declare atomize_rall [symmetric, rulify]lemma rall_simps1:"(∀ x[M]. P(x) ∧ Q) <-> (∀ x[M]. P(x)) ∧ ((∀ x[M]. False) | Q)" "(∀ x[M]. P(x) | Q) <-> ((∀ x[M]. P(x)) | Q)" "(∀ x[M]. P(x) ⟶ Q) <-> ((∃ x[M]. P(x)) ⟶ Q)" "(¬ (∀ x[M]. P(x))) <-> (∃ x[M]. ¬ P(x))" by blast+lemma rall_simps2:"(∀ x[M]. P ∧ Q(x)) <-> ((∀ x[M]. False) | P) ∧ (∀ x[M]. Q(x))" "(∀ x[M]. P | Q(x)) <-> (P | (∀ x[M]. Q(x)))" "(∀ x[M]. P ⟶ Q(x)) <-> (P ⟶ (∀ x[M]. Q(x)))" by blast+lemmas rall_simps [simp] = rall_simps1 rall_simps2lemma rall_conj_distrib:"(∀ x[M]. P(x) ∧ Q(x)) <-> ((∀ x[M]. P(x)) ∧ (∀ x[M]. Q(x)))" by blastlemma rex_simps1:"(∃ x[M]. P(x) ∧ Q) <-> ((∃ x[M]. P(x)) ∧ Q)" "(∃ x[M]. P(x) | Q) <-> (∃ x[M]. P(x)) | ((∃ x[M]. True) ∧ Q)" "(∃ x[M]. P(x) ⟶ Q) <-> ((∀ x[M]. P(x)) ⟶ ((∃ x[M]. True) ∧ Q))" "(¬ (∃ x[M]. P(x))) <-> (∀ x[M]. ¬ P(x))" by blast+lemma rex_simps2:"(∃ x[M]. P ∧ Q(x)) <-> (P ∧ (∃ x[M]. Q(x)))" "(∃ x[M]. P | Q(x)) <-> ((∃ x[M]. True) ∧ P) | (∃ x[M]. Q(x))" "(∃ x[M]. P ⟶ Q(x)) <-> (((∀ x[M]. False) | P) ⟶ (∃ x[M]. Q(x)))" by blast+lemmas rex_simps [simp] = rex_simps1 rex_simps2lemma rex_disj_distrib:"(∃ x[M]. P(x) | Q(x)) <-> ((∃ x[M]. P(x)) | (∃ x[M]. Q(x)))" by blast‹ One-point rule for bounded quantifiers› lemma rex_triv_one_point1 [simp]: "(∃ x[M]. x=a) <-> ( M(a))" by blastlemma rex_triv_one_point2 [simp]: "(∃ x[M]. a=x) <-> ( M(a))" by blastlemma rex_one_point1 [simp]: "(∃ x[M]. x=a ∧ P(x)) <-> ( M(a) ∧ P(a))" by blastlemma rex_one_point2 [simp]: "(∃ x[M]. a=x ∧ P(x)) <-> ( M(a) ∧ P(a))" by blastlemma rall_one_point1 [simp]: "(∀ x[M]. x=a ⟶ P(x)) <-> ( M(a) ⟶ P(a))" by blastlemma rall_one_point2 [simp]: "(∀ x[M]. a=x ⟶ P(x)) <-> ( M(a) ⟶ P(a))" by blast‹ Sets as Classes› definition "[i,i] ==> (‹ (‹ open_block notation=‹ prefix setclass› \› [40] 40) where "setclass(A) ≡ λx. x ∈ A" lemma setclass_iff [simp]: "setclass(A,x) <-> x ∈ A" by (simp add: setclass_def)lemma rall_setclass_is_ball [simp]: "(∀ x[##A]. P(x)) <-> (∀ x∈ A. P(x))" by autolemma rex_setclass_is_bex [simp]: "(∃ x[##A]. P(x)) <-> (∃ x∈ A. P(x))" by auto‹ val Ord_atomize = atomize ([(🍋 ‹ oall› , › declaration ‹ fn _ => Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => map mk_eq o Ord_atomize o Variable.gen_all ctxt)) › text ‹ Setting up the one-point-rule simproc› simproc_setup defined_rex ("∃ x[M]. P(x) ∧ Q(x)" ) = ‹ K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms rex_def})) › simproc_setup defined_rall ("∀ x[M]. P(x) ⟶ Q(x)" ) = ‹ K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms rall_def})) › end Messung V0.5 in Prozent C=80 H=81 G=80
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet am 2026-04-25)
¤ *© Formatika GbR, Deutschland
2026-05-26
