src/ZF/univ.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 14 1c0926788772
     1.1 --- a/src/ZF/univ.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/univ.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
     1.5  goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
     1.6  by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
     1.7 -by (SIMP_TAC ZF_ss 1);
     1.8 +by (simp_tac ZF_ss 1);
     1.9  val Vfrom = result();
    1.10  
    1.11  (** Monotonicity **)
    1.12 @@ -122,9 +122,8 @@
    1.13  
    1.14  goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
    1.15  by (rtac (Vfrom RS trans) 1);
    1.16 -brs ([refl] RL ZF_congs) 1;
    1.17 -by (rtac equalityI 1);
    1.18 -by (rtac (succI1 RS RepFunI RS Union_upper) 2);
    1.19 +by (rtac (succI1 RS RepFunI RS Union_upper RSN
    1.20 +	      (2, equalityI RS subst_context)) 1);
    1.21  by (rtac UN_least 1);
    1.22  by (rtac (subset_refl RS Vfrom_mono RS Pow_mono) 1);
    1.23  by (etac member_succD 1);
    1.24 @@ -473,16 +472,16 @@
    1.25  val rank_trans_rls = rank_rls @ (rank_rls RLN (2, [rank_trans]));
    1.26  
    1.27  val rank_ss = ZF_ss 
    1.28 -    addrews [split, case_Inl, case_Inr, Vset_rankI]
    1.29 -    addrews rank_trans_rls;
    1.30 +    addsimps [case_Inl, case_Inr, Vset_rankI]
    1.31 +    addsimps rank_trans_rls;
    1.32  
    1.33  (** Recursion over Vset levels! **)
    1.34  
    1.35  (*NOT SUITABLE FOR REWRITING: recursive!*)
    1.36  goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
    1.37  by (rtac (transrec RS ssubst) 1);
    1.38 -by (SIMP_TAC (wf_ss addrews [Ord_rank, Ord_succ, Vset_D RS beta, 
    1.39 -			     VsetI RS beta]) 1);
    1.40 +by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, Vset_D RS beta, 
    1.41 +			      VsetI RS beta]) 1);
    1.42  val Vrec = result();
    1.43  
    1.44  (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
    1.45 @@ -493,13 +492,6 @@
    1.46  by (rtac Vrec 1);
    1.47  val def_Vrec = result();
    1.48  
    1.49 -val prems = goalw Univ.thy [Vrec_def]
    1.50 -    "[| a=a';  !!x u. H(x,u)=H'(x,u) |]  ==> Vrec(a,H)=Vrec(a',H')";
    1.51 -val Vrec_ss = ZF_ss addcongs ([transrec_cong] @ mk_congs Univ.thy ["rank"])
    1.52 -		      addrews (prems RL [sym]);
    1.53 -by (SIMP_TAC Vrec_ss 1);
    1.54 -val Vrec_cong = result();
    1.55 -
    1.56  
    1.57  (*** univ(A) ***)
    1.58