src/ZF/Constructible/Formula.thy
changeset 15481 fc075ae929e4
parent 14171 0cab06e3bbd0
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/Constructible/Formula.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -633,21 +633,26 @@
     1.4  text{*Kunen's VI 1.6 (b)*}
     1.5  lemma Lset_mono [rule_format]:
     1.6       "ALL j. i<=j --> Lset(i) <= Lset(j)"
     1.7 -apply (rule_tac a=i in eps_induct)
     1.8 -apply (rule impI [THEN allI])
     1.9 -apply (subst Lset)
    1.10 -apply (subst Lset, blast) 
    1.11 -done
    1.12 +proof (induct i rule: eps_induct, intro allI impI)
    1.13 +  fix x j
    1.14 +  assume "\<forall>y\<in>x. \<forall>j. y \<subseteq> j \<longrightarrow> Lset(y) \<subseteq> Lset(j)"
    1.15 +     and "x \<subseteq> j"
    1.16 +  thus "Lset(x) \<subseteq> Lset(j)"
    1.17 +    by (force simp add: Lset [of x] Lset [of j]) 
    1.18 +qed
    1.19  
    1.20  text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}
    1.21  lemma Lset_mono_mem [rule_format]:
    1.22       "ALL j. i:j --> Lset(i) <= Lset(j)"
    1.23 -apply (rule_tac a=i in eps_induct)
    1.24 -apply (rule impI [THEN allI])
    1.25 -apply (subst Lset, auto) 
    1.26 -apply (rule rev_bexI, assumption)
    1.27 -apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD) 
    1.28 -done
    1.29 +proof (induct i rule: eps_induct, intro allI impI)
    1.30 +  fix x j
    1.31 +  assume "\<forall>y\<in>x. \<forall>j. y \<in> j \<longrightarrow> Lset(y) \<subseteq> Lset(j)"
    1.32 +     and "x \<in> j"
    1.33 +  thus "Lset(x) \<subseteq> Lset(j)"
    1.34 +    by (force simp add: Lset [of j] 
    1.35 +              intro!: bexI intro: elem_subset_in_DPow dest: LsetD DPowD) 
    1.36 +qed
    1.37 +
    1.38  
    1.39  text{*Useful with Reflection to bump up the ordinal*}
    1.40  lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"