Theory Reflection

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

header {* 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 @{text M}.
To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
closed under ordered pairing provided @{text l} is limit.  Possibly this
could be avoided: the induction hypothesis @{term Cl_reflects}
(in locale @{text ex_reflection}) could be weakened to
@{term "∀y∈Mset(a). ∀z∈Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most
uses of @{term Pair_in_Mset}.  But there isn't much point in doing so, since
ultimately the @{text ex_reflection} proof is packaged up using the
predicate @{text 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 @{term y}*}
  fixes FF --{*sup over the whole level, @{term "y∈Mset(a)"}*}
  fixes ClEx --{*Reflecting ordinals for the formula @{term "∃z. P"}*}
  defines "F0(P,y) == μ b. (∃z. M(z) & P(<y,z>)) -->
                               (∃z∈Mset(b). P(<y,z>))"
      and "FF(P)   == λa. \<Union>y∈Mset(a). F0(P,y)"
      and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a"

lemma (in reflection) Mset_mono: "i≤j ==> Mset(i) ⊆ Mset(j)"
apply (insert Mset_mono_le)
apply (simp add: mono_le_subset_def leI)
done

text{*Awkward: we need a version of @{text ClEx_def} as an equality
      at the level of classes, which do not really exist*}
lemma (in reflection) 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 (in reflection) Triv_reflection [intro]:
     "Reflects(Ord, P, λa x. P(x))"
by (simp add: Reflects_def)

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

theorem (in reflection) 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 (in reflection) 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 (in reflection) 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 (in reflection) 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 (in reflection) F0_works:
     "[| y∈Mset(a); Ord(a); M(z); P(<y,z>) |] ==> ∃z∈Mset(F0(P,y)). P(<y,z>)"
apply (unfold F0_def M_def, clarify)
apply (rule LeastI2)
  apply (blast intro: Mset_mono [THEN subsetD])
 apply (blast intro: lt_Ord2, blast)
done

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

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

lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))"
apply (insert Mset_cont)
apply (simp add: cont_Ord_def FF_def, blast)
done

text{*Recall that @{term F0} depends upon @{term "y∈Mset(a)"},
while @{term FF} depends only upon @{term a}. *}
lemma (in reflection) 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 Ord_F0)
apply (blast intro: F0_works)
done

lemma (in reflection) 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


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)"

lemma (in ex_reflection) 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 (in ex_reflection) 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 @{text ClEx} indeed consists of reflecting ordinals...*}
lemma (in ex_reflection) 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 (in ex_reflection) 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

text{*The same two theorems, exported to locale @{text reflection}.*}

text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
lemma (in reflection) 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>))"
apply (unfold 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 (in reflection) Closed_Unbounded_ClEx:
     "(!!a. [| Cl(a); Ord(a) |] ==> ∀x∈Mset(a). P(x) <-> Q(a,x))
      ==> Closed_Unbounded(ClEx(P))"
apply (unfold 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 (in reflection) 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 (in reflection) 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 (in reflection) 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 (in reflection) 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 (in reflection) 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 (in reflection) 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 @{text ?Cl} and later retrieved from the final
proof state.*}
schematic_lemma (in reflection)
     "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 @{term "Ord(a)"} is redundant,
though harmless.*}
lemma (in reflection)
     "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_lemma (in reflection)
     "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 (in reflection)
  "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_lemma (in reflection)
  "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_lemma (in reflection)
     "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 @{term P} is quantifier-free, since it is not being relativized.*}
schematic_lemma (in reflection)
     "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_lemma (in reflection)
     "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_lemma (in reflection)
     "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 @{text Π} needs
to be relativized.*}
schematic_lemma (in reflection)
     "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