Quelle  Reflection.thy

(*  Title:      ZF/Constructible/Reflection.thy
  Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section ‹The Reflection Theorem›

theory Reflection imports Normal begin

lemma all_iff_not_ex_not: "(∀x. P(x)) ⟷ (¬ (∃x. ¬ P(x)))"
  by blast

lemma ball_iff_not_bex_not: "(∀x∈A. P(x)) ⟷ (¬ (∃x∈A. ¬ P(x)))"
  by blast

text‹From the notes of A. S. Kechris, page 6, and from
  Andrzej Mostowski, \emph{Constructible Sets with Applications},
  North-Holland, 1969, page 23.›


subsection‹Basic Definitions›

text‹First part: the cumulative hierarchy defining the class ‹M›.
 To avoid handling multiple arguments, we assume that ‹Mset(l)› is
 closed under ordered pairing provided ‹l› is limit. Possibly this
 could be avoided: the induction hypothesis 🍋‹Cl_reflects›
 (in locale ‹ex_reflection›) could be weakened to
 🍋‹∀y∈Mset(a). ∀z∈Mset(a). P(⟨y,z⟩) ⟷ Q(a,⟨y,z⟩)›, removing most
 uses of 🍋‹Pair_in_Mset›. But there isn't much point in doing so, since
 ultimately the ‹ex_reflection› proof is packaged up using the
 predicate ‹Reflects›.
 ›
locale reflection =
  fixes Mset and M and Reflects
  assumes Mset_mono_le : "mono_le_subset(Mset)"
      and Mset_cont    : "cont_Ord(Mset)"
      and Pair_in_Mset : "[x ∈ Mset(a); y ∈ Mset(a); Limit(a)]
                          ==> ⟨x,y⟩ ∈ Mset(a)"
  defines "M(x) ≡ ∃a. Ord(a) ∧ x ∈ Mset(a)"
      and "Reflects(Cl,P,Q) ≡ Closed_Unbounded(Cl) ∧
                              (∀a. Cl(a) ⟶ (∀x∈Mset(a). P(x) ⟷ Q(a,x)))"
  fixes F0 🍋 ‹ordinal for a specific value 🍋‹y›\›
  fixes FF 🍋 ‹sup over the whole level, 🍋‹y∈Mset(a)›\›
  fixes ClEx 🍋 ‹Reflecting ordinals for the formula 🍋‹∃z. P›\›
  defines "F0(P,y) ≡ μ b. (∃z. M(z) ∧ P(⟨y,z⟩)) ⟶
                               (∃z∈Mset(b). P(⟨y,z⟩))"
      and "FF(P) ≡ λa. ∪y∈Mset(a). F0(P,y)"
      and "ClEx(P,a) ≡ Limit(a) ∧ normalize(FF(P),a) = a"

begin 

lemma Mset_mono: "i≤j ==> Mset(i) ⊆ Mset(j)"
  using Mset_mono_le by (simp add: mono_le_subset_def leI)

text‹Awkward: we need a version of ‹ClEx_def› as an equality
  at the level of classes, which do not really exist›
lemma ClEx_eq:
     "ClEx(P) ≡ λa. Limit(a) ∧ normalize(FF(P),a) = a"
by (simp add: ClEx_def [symmetric])


subsection‹Easy Cases of the Reflection Theorem›

theorem Triv_reflection [intro]:
  "Reflects(Ord, P, λa x. P(x))"
  by (simp add: Reflects_def)

theorem Not_reflection [intro]:
  "Reflects(Cl,P,Q) ==> Reflects(Cl, λx. ¬P(x), λa x. ¬Q(a,x))"
  by (simp add: Reflects_def)

theorem And_reflection [intro]:
  "[Reflects(Cl,P,Q); Reflects(C',P',Q')]
      ==> Reflects(λa. Cl(a) ∧ C'(a), λx. P(x) ∧ P'(x),
                                      λa x. Q(a,x) ∧ Q'(a,x))"
  by (simp add: Reflects_def Closed_Unbounded_Int, blast)

theorem Or_reflection [intro]:
     "[Reflects(Cl,P,Q); Reflects(C',P',Q')]
      ==> Reflects(λa. Cl(a) ∧ C'(a), λx. P(x) ∨ P'(x),
                                      λa x. Q(a,x) ∨ Q'(a,x))"
by (simp add: Reflects_def Closed_Unbounded_Int, blast)

theorem Imp_reflection [intro]:
     "[Reflects(Cl,P,Q); Reflects(C',P',Q')]
      ==> Reflects(λa. Cl(a) ∧ C'(a),
                   λx. P(x) ⟶ P'(x),
                   λa x. Q(a,x) ⟶ Q'(a,x))"
by (simp add: Reflects_def Closed_Unbounded_Int, blast)

theorem Iff_reflection [intro]:
     "[Reflects(Cl,P,Q); Reflects(C',P',Q')]
      ==> Reflects(λa. Cl(a) ∧ C'(a),
                   λx. P(x) ⟷ P'(x),
                   λa x. Q(a,x) ⟷ Q'(a,x))"
by (simp add: Reflects_def Closed_Unbounded_Int, blast)

subsection‹Reflection for Existential Quantifiers›

lemma F0_works:
  "[y∈Mset(a); Ord(a); M(z); P(⟨y,z⟩)] ==> ∃z∈Mset(F0(P,y)). P(⟨y,z⟩)"
  unfolding F0_def M_def
  apply clarify
  apply (rule LeastI2)
    apply (blast intro: Mset_mono [THEN subsetD])
   apply (blast intro: lt_Ord2, blast)
  done

lemma Ord_F0 [intro,simp]: "Ord(F0(P,y))"
  by (simp add: F0_def)

lemma Ord_FF [intro,simp]: "Ord(FF(P,y))"
  by (simp add: FF_def)

lemma cont_Ord_FF: "cont_Ord(FF(P))"
  using Mset_cont by (simp add: cont_Ord_def FF_def, blast)

text‹Recall that 🍋‹F0› depends upon 🍋‹y∈Mset(a)›,
 while 🍋‹FF› depends only upon 🍋‹a›.›
lemma FF_works:
  "[M(z); y∈Mset(a); P(⟨y,z⟩); Ord(a)] ==> ∃z∈Mset(FF(P,a)). P(⟨y,z⟩)"
  apply (simp add: FF_def)
  apply (simp_all add: cont_Ord_Union [of concl: Mset]
      Mset_cont Mset_mono_le not_emptyI)
  apply (blast intro: F0_works)
  done

lemma FFN_works:
     "[M(z); y∈Mset(a); P(⟨y,z⟩); Ord(a)]
      ==> ∃z∈Mset(normalize(FF(P),a)). P(⟨y,z⟩)"
apply (drule FF_works [of concl: P], assumption+)
apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD])
done

end

text‹Locale for the induction hypothesis›

locale ex_reflection = reflection +
  fixes P  🍋 ‹the original formula›
  fixes Q  🍋 ‹the reflected formula›
  fixes Cl 🍋 ‹the class of reflecting ordinals›
  assumes Cl_reflects: "[Cl(a); Ord(a)] ==> ∀x∈Mset(a). P(x) ⟷ Q(a,x)"

begin

lemma ClEx_downward:
     "[M(z); y∈Mset(a); P(⟨y,z⟩); Cl(a); ClEx(P,a)]
      ==> ∃z∈Mset(a). Q(a,⟨y,z⟩)"
apply (simp add: ClEx_def, clarify)
apply (frule Limit_is_Ord)
apply (frule FFN_works [of concl: P], assumption+)
apply (drule Cl_reflects, assumption+)
apply (auto simp add: Limit_is_Ord Pair_in_Mset)
done

lemma ClEx_upward:
     "[z∈Mset(a); y∈Mset(a); Q(a,⟨y,z⟩); Cl(a); ClEx(P,a)]
      ==> ∃z. M(z) ∧ P(⟨y,z⟩)"
apply (simp add: ClEx_def M_def)
apply (blast dest: Cl_reflects
             intro: Limit_is_Ord Pair_in_Mset)
done

text‹Class ‹ClEx› indeed consists of reflecting ordinals...›
lemma ZF_ClEx_iff:
     "[y∈Mset(a); Cl(a); ClEx(P,a)]
      ==> (∃z. M(z) ∧ P(⟨y,z⟩)) ⟷ (∃z∈Mset(a). Q(a,⟨y,z⟩))"
by (blast intro: dest: ClEx_downward ClEx_upward)

text‹...and it is closed and unbounded›
lemma ZF_Closed_Unbounded_ClEx:
     "Closed_Unbounded(ClEx(P))"
apply (simp add: ClEx_eq)
apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded
                   Closed_Unbounded_Limit Normal_normalize)
done

end

text‹The same two theorems, exported to locale ‹reflection›.›

context reflection
begin

text‹Class ‹ClEx› indeed consists of reflecting ordinals...›
lemma ClEx_iff:
     "[y∈Mset(a); Cl(a); ClEx(P,a);
        ∧a. [Cl(a); Ord(a)] ==> ∀x∈Mset(a). P(x) ⟷ Q(a,x)]
      ==> (∃z. M(z) ∧ P(⟨y,z⟩)) ⟷ (∃z∈Mset(a). Q(a,⟨y,z⟩))"
  unfolding ClEx_def FF_def F0_def M_def
apply (rule ex_reflection.ZF_ClEx_iff
  [OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro,
    of Mset Cl])
apply (simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
done

(*Alternative proof, less unfolding:
 apply (rule Reflection.ZF_ClEx_iff [of Mset _ _ Cl, folded M_def])
 apply (fold ClEx_def FF_def F0_def)
 apply (rule ex_reflection.intro, assumption)
 apply (simp add: ex_reflection_axioms.intro, assumption+)
*)

lemma Closed_Unbounded_ClEx:
     "(∧a. [Cl(a); Ord(a)] ==> ∀x∈Mset(a). P(x) ⟷ Q(a,x))
      ==> Closed_Unbounded(ClEx(P))"
  unfolding ClEx_eq FF_def F0_def M_def
apply (rule ex_reflection.ZF_Closed_Unbounded_ClEx [of Mset _ _ Cl])
apply (rule ex_reflection.intro, rule reflection_axioms)
apply (blast intro: ex_reflection_axioms.intro)
done

subsection‹Packaging the Quantifier Reflection Rules›

lemma Ex_reflection_0:
     "Reflects(Cl,P0,Q0)
      ==> Reflects(λa. Cl(a) ∧ ClEx(P0,a),
                   λx. ∃z. M(z) ∧ P0(⟨x,z⟩),
                   λa x. ∃z∈Mset(a). Q0(a,⟨x,z⟩))"
apply (simp add: Reflects_def)
apply (intro conjI Closed_Unbounded_Int)
  apply blast
 apply (rule Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify)
apply (rule_tac Cl=Cl in  ClEx_iff, assumption+, blast)
done

lemma All_reflection_0:
     "Reflects(Cl,P0,Q0)
      ==> Reflects(λa. Cl(a) ∧ ClEx(λx.¬P0(x), a),
                   λx. ∀z. M(z) ⟶ P0(⟨x,z⟩),
                   λa x. ∀z∈Mset(a). Q0(a,⟨x,z⟩))"
apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not)
apply (rule Not_reflection, drule Not_reflection, simp)
apply (erule Ex_reflection_0)
done

theorem Ex_reflection [intro]:
     "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x)))
      ==> Reflects(λa. Cl(a) ∧ ClEx(λx. P(fst(x),snd(x)), a),
                   λx. ∃z. M(z) ∧ P(x,z),
                   λa x. ∃z∈Mset(a). Q(a,x,z))"
by (rule Ex_reflection_0 [of _ " λx. P(fst(x),snd(x))"
                               "λa x. Q(a,fst(x),snd(x))", simplified])

theorem All_reflection [intro]:
     "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x)))
      ==> Reflects(λa. Cl(a) ∧ ClEx(λx. ¬P(fst(x),snd(x)), a),
                   λx. ∀z. M(z) ⟶ P(x,z),
                   λa x. ∀z∈Mset(a). Q(a,x,z))"
by (rule All_reflection_0 [of _ "λx. P(fst(x),snd(x))"
                                "λa x. Q(a,fst(x),snd(x))", simplified])

text‹And again, this time using class-bounded quantifiers›

theorem Rex_reflection [intro]:
     "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x)))
      ==> Reflects(λa. Cl(a) ∧ ClEx(λx. P(fst(x),snd(x)), a),
                   λx. ∃z[M]. P(x,z),
                   λa x. ∃z∈Mset(a). Q(a,x,z))"
by (unfold rex_def, blast)

theorem Rall_reflection [intro]:
     "Reflects(Cl, λx. P(fst(x),snd(x)), λa x. Q(a,fst(x),snd(x)))
      ==> Reflects(λa. Cl(a) ∧ ClEx(λx. ¬P(fst(x),snd(x)), a),
                   λx. ∀z[M]. P(x,z),
                   λa x. ∀z∈Mset(a). Q(a,x,z))"
by (unfold rall_def, blast)


text‹No point considering bounded quantifiers, where reflection is trivial.›


subsection‹Simple Examples of Reflection›

text‹Example 1: reflecting a simple formula. The reflecting class is first
 given as the variable ‹?Cl› and later retrieved from the final
 proof state.›
schematic_goal
     "Reflects(?Cl,
               λx. ∃y. M(y) ∧ x ∈ y,
               λa x. ∃y∈Mset(a). x ∈ y)"
by fast

text‹Problem here: there needs to be a conjunction (class intersection)
 in the class of reflecting ordinals. The 🍋‹Ord(a)› is redundant,
 though harmless.›
lemma
     "Reflects(λa. Ord(a) ∧ ClEx(λx. fst(x) ∈ snd(x), a),
               λx. ∃y. M(y) ∧ x ∈ y,
               λa x. ∃y∈Mset(a). x ∈ y)"
by fast


text‹Example 2›
schematic_goal
     "Reflects(?Cl,
               λx. ∃y. M(y) ∧ (∀z. M(z) ⟶ z ⊆ x ⟶ z ∈ y),
               λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x ⟶ z ∈ y)"
by fast

text‹Example 2'. We give the reflecting class explicitly.›
lemma
  "Reflects
    (λa. (Ord(a) ∧
          ClEx(λx. ¬ (snd(x) ⊆ fst(fst(x)) ⟶ snd(x) ∈ snd(fst(x))), a)) ∧
          ClEx(λx. ∀z. M(z) ⟶ z ⊆ fst(x) ⟶ z ∈ snd(x), a),
            λx. ∃y. M(y) ∧ (∀z. M(z) ⟶ z ⊆ x ⟶ z ∈ y),
            λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x ⟶ z ∈ y)"
by fast

text‹Example 2''. We expand the subset relation.›
schematic_goal
  "Reflects(?Cl,
        λx. ∃y. M(y) ∧ (∀z. M(z) ⟶ (∀w. M(w) ⟶ w∈z ⟶ w∈x) ⟶ z∈y),
        λa x. ∃y∈Mset(a). ∀z∈Mset(a). (∀w∈Mset(a). w∈z ⟶ w∈x) ⟶ z∈y)"
by fast

text‹Example 2'''. Single-step version, to reveal the reflecting class.›
schematic_goal
     "Reflects(?Cl,
               λx. ∃y. M(y) ∧ (∀z. M(z) ⟶ z ⊆ x ⟶ z ∈ y),
               λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ⊆ x ⟶ z ∈ y)"
apply (rule Ex_reflection)
txt‹
 @{goals[display,indent=0,margin=60]}
 ›
apply (rule All_reflection)
txt‹
 @{goals[display,indent=0,margin=60]}
 ›
apply (rule Triv_reflection)
txt‹
 @{goals[display,indent=0,margin=60]}
 ›
done

text‹Example 3. Warning: the following examples make sense only
 if 🍋‹P› is quantifier-free, since it is not being relativized.›
schematic_goal
     "Reflects(?Cl,
               λx. ∃y. M(y) ∧ (∀z. M(z) ⟶ z ∈ y ⟷ z ∈ x ∧ P(z)),
               λa x. ∃y∈Mset(a). ∀z∈Mset(a). z ∈ y ⟷ z ∈ x ∧ P(z))"
by fast

text‹Example 3'›
schematic_goal
     "Reflects(?Cl,
               λx. ∃y. M(y) ∧ y = Collect(x,P),
               λa x. ∃y∈Mset(a). y = Collect(x,P))"
by fast

text‹Example 3''›
schematic_goal
     "Reflects(?Cl,
               λx. ∃y. M(y) ∧ y = Replace(x,P),
               λa x. ∃y∈Mset(a). y = Replace(x,P))"
by fast

text‹Example 4: Axiom of Choice. Possibly wrong, since ‹Π› needs
 to be relativized.›
schematic_goal
     "Reflects(?Cl,
               λA. 0∉A ⟶ (∃f. M(f) ∧ f ∈ (∏X ∈ A. X)),
               λa A. 0∉A ⟶ (∃f∈Mset(a). f ∈ (∏X ∈ A. X)))"
by fast

end

end