src/ZF/Constructible/Reflection.thy
 changeset 36319 8feb2c4bef1a parent 32960 69916a850301 child 46823 57bf0cecb366
```     1.1 --- a/src/ZF/Constructible/Reflection.thy	Fri Apr 23 23:33:48 2010 +0200
1.2 +++ b/src/ZF/Constructible/Reflection.thy	Fri Apr 23 23:35:43 2010 +0200
1.3 @@ -268,7 +268,7 @@
1.4  text{*Example 1: reflecting a simple formula.  The reflecting class is first
1.5  given as the variable @{text ?Cl} and later retrieved from the final
1.6  proof state.*}
1.7 -lemma (in reflection)
1.8 +schematic_lemma (in reflection)
1.9       "Reflects(?Cl,
1.10                 \<lambda>x. \<exists>y. M(y) & x \<in> y,
1.11                 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
1.12 @@ -285,7 +285,7 @@
1.13
1.14
1.15  text{*Example 2*}
1.16 -lemma (in reflection)
1.17 +schematic_lemma (in reflection)
1.18       "Reflects(?Cl,
1.19                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
1.20                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
1.21 @@ -302,14 +302,14 @@
1.22  by fast
1.23
1.24  text{*Example 2''.  We expand the subset relation.*}
1.25 -lemma (in reflection)
1.26 +schematic_lemma (in reflection)
1.27    "Reflects(?Cl,
1.28          \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
1.29          \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z --> w\<in>x) --> z\<in>y)"
1.30  by fast
1.31
1.32  text{*Example 2'''.  Single-step version, to reveal the reflecting class.*}
1.33 -lemma (in reflection)
1.34 +schematic_lemma (in reflection)
1.35       "Reflects(?Cl,
1.36                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
1.37                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
1.38 @@ -329,21 +329,21 @@
1.39
1.40  text{*Example 3.  Warning: the following examples make sense only
1.41  if @{term P} is quantifier-free, since it is not being relativized.*}
1.42 -lemma (in reflection)
1.43 +schematic_lemma (in reflection)
1.44       "Reflects(?Cl,
1.45                 \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<in> y <-> z \<in> x & P(z)),
1.46                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x & P(z))"
1.47  by fast
1.48
1.49  text{*Example 3'*}
1.50 -lemma (in reflection)
1.51 +schematic_lemma (in reflection)
1.52       "Reflects(?Cl,
1.53                 \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
1.54                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
1.55  by fast
1.56
1.57  text{*Example 3''*}
1.58 -lemma (in reflection)
1.59 +schematic_lemma (in reflection)
1.60       "Reflects(?Cl,
1.61                 \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
1.62                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
1.63 @@ -351,7 +351,7 @@
1.64
1.65  text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
1.66  to be relativized.*}
1.67 -lemma (in reflection)
1.68 +schematic_lemma (in reflection)
1.69       "Reflects(?Cl,
1.70                 \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
1.71                 \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"
```