src/ZF/OrderType.ML

 (*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord
   The smaller ordinal is an initial segment of the larger *)
 goalw OrderType.thy [pred_def, lt_def]
     "!!i j. j<i ==> pred(i, j, Memrel(i)) = j";
 by (asm_simp_tac (!simpset addsimps [Memrel_iff]) 1);
-by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+by (fast_tac (!claset addEs [Ord_trans]) 1);
 qed "lt_pred_Memrel";
 
 goalw OrderType.thy [pred_def,Memrel_def] 
       "!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "pred_Memrel";
 
 goal OrderType.thy
     "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
 by (forward_tac [lt_pred_Memrel] 1);

 (*combining these two simplifications LOOPS! *)
 by (asm_simp_tac (!simpset addsimps [pred_pred_eq]) 1);
 by (asm_full_simp_tac (!simpset addsimps [pred_def]) 1);
 by (rtac (refl RSN (2,RepFun_cong)) 1);
 by (dtac well_ord_is_trans_on 1);
-by (fast_tac (eq_cs addSEs [trans_onD]) 1);
+by (fast_tac (!claset addSEs [trans_onD]) 1);
 qed "ordermap_pred_eq_ordermap";
 
 goalw OrderType.thy [ordertype_def]
     "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
 by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);

 (*May rewrite with this -- provided no rules are supplied for proving that
         well_ord(pred(A,x,r), r) *)
 goal OrderType.thy
     "!!A r. well_ord(A,r) ==>  \
 \           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
-by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD]));
+by (rtac equalityI 1);
+by (safe_tac (!claset addSIs [ordertype_pred_lt RS ltD]));
 by (fast_tac
     (!claset addss
      (!simpset addsimps [ordertype_def, 
                       well_ord_is_wf RS ordermap_eq_image, 
                       ordermap_type RS image_fun, 

 (*proof by Krzysztof Grabczewski*)
 goalw OrderType.thy [Ord_alt_def] "!!i. Ord(i) ==> Ord_alt(i)";
 by (rtac conjI 1);
 by (etac well_ord_Memrel 1);
 by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Ord_is_Ord_alt";
 
 (*proof by lcp*)
 goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, 
                      tot_ord_def, part_ord_def, trans_on_def] 

 
 (** Addition with 0 **)
 
 goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
 by (res_inst_tac [("d", "Inl")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (Asm_simp_tac));
 qed "bij_sum_0";
 
 goal OrderType.thy
  "!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
 by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
 by (assume_tac 2);
-by (fast_tac (sum_cs addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
 qed "ordertype_sum_0_eq";
 
 goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
 by (res_inst_tac [("d", "Inr")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (Asm_simp_tac));
 qed "bij_0_sum";
 
 goal OrderType.thy
  "!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
 by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
 by (assume_tac 2);
-by (fast_tac (sum_cs addss (!simpset addsimps [radd_Inr_iff, Memrel_iff])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [radd_Inr_iff, Memrel_iff])) 1);
 qed "ordertype_0_sum_eq";
 
 (** Initial segments of radd.  Statements by Grabczewski **)
 
 (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
 goalw OrderType.thy [pred_def]
  "!!A B. a:A ==>  \
 \        (lam x:pred(A,a,r). Inl(x))    \
 \        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS
     (asm_full_simp_tac 
      (!simpset addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
 qed "pred_Inl_bij";
 

 goalw OrderType.thy [pred_def, id_def]
  "!!A B. b:B ==>  \
 \        id(A+pred(B,b,s))      \
 \        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
 by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (Asm_full_simp_tac));
 qed "pred_Inr_bij";
 
 goal OrderType.thy
  "!!A B. [| b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
 \        ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
 \        ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
 by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (fast_tac (sum_cs addss (!simpset addsimps [pred_def, id_def])) 2);
+by (fast_tac (!claset addss (!simpset addsimps [pred_def, id_def])) 2);
 by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset]));
 qed "ordertype_pred_Inr_eq";
 
 (*** Basic laws for ordinal addition ***)
 

 by (rtac ltE 1 THEN assume_tac 1);
 by (rtac ltI 1);
 by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
 by (asm_simp_tac 
     (!simpset addsimps [ordertype_pred_unfold, 
-			well_ord_radd, well_ord_Memrel,
-			ordertype_pred_Inl_eq, 
-			lt_pred_Memrel, leI RS le_ordertype_Memrel]
+                        well_ord_radd, well_ord_Memrel,
+                        ordertype_pred_Inl_eq, 
+                        lt_pred_Memrel, leI RS le_ordertype_Memrel]
            setloop rtac (InlI RSN (2,bexI))) 1);
 qed "lt_oadd1";
 
 (*Thus also we obtain the rule  i++j = k ==> i le k *)
 goal OrderType.thy "!!i j. [| Ord(i);  Ord(j) |] ==> i le i++j";

 by (etac revcut_rl 1);
 by (asm_full_simp_tac 
     (!simpset addsimps [ordertype_pred_unfold, well_ord_radd,
                      well_ord_Memrel]) 1);
 by (eresolve_tac [ltD RS RepFunE] 1);
-by (fast_tac (sum_cs addss 
+by (fast_tac (!claset addss 
               (!simpset addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
                                ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
                                ordertype_pred_Inr_eq, 
                                ordertype_sum_Memrel])) 1);
 qed "lt_oadd_disj";

 by (fast_tac (!claset addSEs [ltE]) 1);
 qed "oadd_unfold";
 
 goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
 by (asm_simp_tac (!simpset addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "oadd_1";
 
 goal OrderType.thy
     "!!i. [| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
-		(*ZF_ss prevents looping*)
+                (*ZF_ss prevents looping*)
 by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
 by (asm_simp_tac (!simpset addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
 qed "oadd_succ";
 
 
 (** Ordinal addition with limit ordinals **)
 
 val prems = goal OrderType.thy
     "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
 \    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
+by (fast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
                                     lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
                      addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
 qed "oadd_UN";
 
 goal OrderType.thy 

 by (asm_simp_tac (!simpset addsimps [oadd_Limit]) 1);
 by (rtac le_trans 1);
 by (rtac le_implies_UN_le_UN 2);
 by (Fast_tac 2);
 by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
-				     le_refl, Limit_is_Ord]) 1);
+                                     le_refl, Limit_is_Ord]) 1);
 qed "oadd_le_self2";
 
 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k++i le j++i";
 by (forward_tac [lt_Ord] 1);
 by (forward_tac [le_Ord2] 1);

 **)
 
 goal OrderType.thy
     "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (fast_tac (sum_cs addSIs [if_type]) 1);
+by (fast_tac (!claset addSIs [if_type]) 1);
 by (fast_tac (!claset addSIs [case_type]) 1);
 by (etac sumE 2);
 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
 qed "bij_sum_Diff";
 

 
 goalw OrderType.thy [pred_def]
  "!!A B. [| a:A;  b:B |] ==>  \
 \        pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
 \        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
-by (safe_tac eq_cs);
+by (rtac equalityI 1);
+by (safe_tac (!claset));
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [rmult_iff])));
 by (ALLGOALS (Fast_tac));
 qed "pred_Pair_eq";
 
 goal OrderType.thy

 goalw OrderType.thy [omult_def]
  "!!i j. [| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i";
 by (rtac ltI 1);
 by (asm_simp_tac
     (!simpset addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
-			lt_Ord2]) 2);
+                        lt_Ord2]) 2);
 by (asm_simp_tac 
     (!simpset addsimps [ordertype_pred_unfold, 
                      well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
 by (rtac bexI 1);
 by (fast_tac (!claset addSEs [ltE]) 2);
 by (asm_simp_tac 
     (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
-			symmetric omult_def]) 1);
+                        symmetric omult_def]) 1);
 qed "omult_oadd_lt";
 
 goal OrderType.thy
  "!!i j. [| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
 by (rtac (subsetI RS equalityI) 1);

 by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
                       Ord_ordertype] 1));
 qed "oadd_omult_distrib";
 
 goal OrderType.thy "!!i. [| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
-		(*ZF_ss prevents looping*)
+                (*ZF_ss prevents looping*)
 by (asm_simp_tac (ZF_ss addsimps [oadd_1 RS sym]) 1);
 by (asm_simp_tac 
     (!simpset addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
 qed "omult_succ";
 

 
 val prems = goal OrderType.thy
     "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
 \    i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
 by (asm_simp_tac (!simpset addsimps (prems@[Ord_UN, omult_unfold])) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "omult_UN";
 
 goal OrderType.thy 
     "!!i j. [| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
 by (asm_simp_tac 

 by (asm_simp_tac (!simpset addsimps [omult_Limit]) 1);
 by (rtac le_trans 1);
 by (rtac le_implies_UN_le_UN 2);
 by (Fast_tac 2);
 by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
-				     Limit_is_Ord RS le_refl]) 1);
+                                     Limit_is_Ord RS le_refl]) 1);
 qed "omult_le_self2";
 
 
 (** Further properties of ordinal multiplication **)