src/ZF/OrderArith.ML

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Towards ordinal arithmetic 
 *)
-
-open OrderArith;
-
 
 (**** Addition of relations -- disjoint sum ****)
 
 (** Rewrite rules.  Can be used to obtain introduction rules **)
 

 Addsimps [radd_Inl_iff, radd_Inr_iff, 
           radd_Inl_Inr_iff, radd_Inr_Inl_iff];
 
 Goalw [linear_def]
     "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
-by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE));
-by (ALLGOALS Asm_simp_tac);
+by (Force_tac 1);
 qed "linear_radd";
 
 
 (** Well-foundedness **)
 

 Goal "[| f: bij(A,C);  g: bij(B,D) |] ==> \
 \        (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)";
 by (res_inst_tac 
         [("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] 
     lam_bijective 1);
-by (safe_tac (claset() addSEs [sumE]));
+by Safe_tac;
 by (ALLGOALS (asm_simp_tac bij_inverse_ss));
 qed "sum_bij";
 
 Goalw [ord_iso_def]
     "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |] ==>     \

      ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
 Goal "A Int B = 0 ==>     \
 \           (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
 by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")] 
     lam_bijective 1);
-by (blast_tac (claset() addSIs [if_type]) 2);
-by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by Auto_tac;
 qed "sum_disjoint_bij";
 
 (** Associativity **)
 
 Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
 \ : bij((A+B)+C, A+(B+C))";
 by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] 
     lam_bijective 1);
-by (ALLGOALS (asm_simp_tac (simpset() setloop etac sumE)));
+by Auto_tac;
 qed "sum_assoc_bij";
 
 Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
 \ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),    \
 \           A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
 by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
-by (REPEAT_FIRST (etac sumE));
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
 qed "sum_assoc_ord_iso";
 
 
 (**** Multiplication of relations -- lexicographic product ****)
 

 by (blast_tac (claset() addIs [bij_is_inj RS inj_apply_equality]) 1);
 qed "prod_ord_iso_cong";
 
 Goal "(lam z:A. <x,z>) : bij(A, {x}*A)";
 by (res_inst_tac [("d", "snd")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
 qed "singleton_prod_bij";
 
 (*Used??*)
 Goal "well_ord({x},xr) ==>  \
 \         (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";

 by (rtac subst_elem 1);
 by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
 by (rtac singleton_prod_bij 1);
 by (rtac sum_disjoint_bij 1);
 by (Blast_tac 1);
-by (asm_simp_tac (simpset() addcongs [case_cong] addsimps [id_conv]) 1);
+by (asm_simp_tac (simpset() addcongs [case_cong]) 1);
 by (resolve_tac [comp_lam RS trans RS sym] 1);
 by (fast_tac (claset() addSEs [case_type]) 1);
 by (asm_simp_tac (simpset() addsimps [case_case]) 1);
 qed "prod_sum_singleton_bij";
 

 
 Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
 \ : bij((A+B)*C, (A*C)+(B*C))";
 by (res_inst_tac
     [("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
-by (safe_tac (claset() addSEs [sumE]));
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
 qed "sum_prod_distrib_bij";
 
 Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
 \ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
 \           (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
 by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
-by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE]));
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
 qed "sum_prod_distrib_ord_iso";
 
 (** Associativity **)
 
 Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
 by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
-by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE)));
+by Auto_tac;
 qed "prod_assoc_bij";
 
 Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                   \
 \ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),  \
 \           A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))";
 by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
-by (REPEAT_FIRST (eresolve_tac [SigmaE, ssubst]));
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
+by Auto_tac;
 qed "prod_assoc_ord_iso";
 
 (**** Inverse image of a relation ****)
 
 (** Rewrite rule **)
 
-Goalw [rvimage_def] 
-    "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
+Goalw [rvimage_def] "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
 by (Blast_tac 1);
 qed "rvimage_iff";
 
 (** Type checking **)
 

 by (rtac Collect_subset 1);
 qed "rvimage_type";
 
 bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
 
-Goalw [rvimage_def] 
-    "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
+Goalw [rvimage_def] "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
 by (Blast_tac 1);
 qed "rvimage_converse";
 
 
 (** Partial Ordering Properties **)

 by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
 by (Blast_tac 1);
 by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
 by (blast_tac (claset() addSIs [apply_funtype]) 1);
 by (blast_tac (claset() addSIs [apply_funtype] 
-                       addSDs [rvimage_iff RS iffD1]) 1);
+                        addSDs [rvimage_iff RS iffD1]) 1);
 qed "wf_on_rvimage";
 
 (*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
 Goal "[| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
 by (rtac well_ordI 1);