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