tidying
authorpaulson
Tue Sep 22 13:50:57 1998 +0200 (1998-09-22)
changeset 55294a54acae6a15
parent 5528 4896b4e4077b
child 5530 c361279ebc66
tidying
src/ZF/Arith.ML
src/ZF/CardinalArith.ML
src/ZF/Coind/Types.ML
src/ZF/List.ML
src/ZF/Nat.ML
src/ZF/OrdQuant.ML
src/ZF/OrderType.ML
src/ZF/Perm.ML
src/ZF/ROOT.ML
src/ZF/ex/LList.ML
src/ZF/ex/Limit.ML
src/ZF/indrule.ML
     1.1 --- a/src/ZF/Arith.ML	Tue Sep 22 13:49:22 1998 +0200
     1.2 +++ b/src/ZF/Arith.ML	Tue Sep 22 13:50:57 1998 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4  by (rtac (prems MRS diff_induct) 1);
     1.5  by (etac leE 3);
     1.6  by (ALLGOALS
     1.7 -    (asm_simp_tac (simpset() addsimps (prems @ [le_iff, nat_into_Ord]))));
     1.8 +    (asm_simp_tac (simpset() addsimps prems @ [le_iff, nat_into_Ord])));
     1.9  qed "diff_le_self";
    1.10  
    1.11  (*** Simplification over add, mult, diff ***)
     2.1 --- a/src/ZF/CardinalArith.ML	Tue Sep 22 13:49:22 1998 +0200
     2.2 +++ b/src/ZF/CardinalArith.ML	Tue Sep 22 13:50:57 1998 +0200
     2.3 @@ -708,7 +708,7 @@
     2.4  
     2.5  Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
     2.6  by (etac nat_induct 1);
     2.7 -by (simp_tac (simpset() addsimps (eqpoll_0_iff::Fin.intrs)) 1);
     2.8 +by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1);
     2.9  by (Clarify_tac 1);
    2.10  by (subgoal_tac "EX u. u:A" 1);
    2.11  by (etac exE 1);
     3.1 --- a/src/ZF/Coind/Types.ML	Tue Sep 22 13:49:22 1998 +0200
     3.2 +++ b/src/ZF/Coind/Types.ML	Tue Sep 22 13:50:57 1998 +0200
     3.3 @@ -15,13 +15,13 @@
     3.4  
     3.5  Goal "te_rec(te_emp,c_te_emp,f_te_owr) = c_te_emp";
     3.6  by (rtac (te_rec_def RS def_Vrec RS trans) 1);
     3.7 -by (simp_tac (simpset() addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
     3.8 +by (simp_tac (simpset() addsimps rank_te_owr1::TyEnv.case_eqns) 1);
     3.9  qed "te_rec_emp";
    3.10  
    3.11  Goal " te_rec(te_owr(te,x,t),c_te_emp,f_te_owr) = \
    3.12  \   f_te_owr(te,x,t,te_rec(te,c_te_emp,f_te_owr))";
    3.13  by (rtac (te_rec_def RS def_Vrec RS trans) 1);
    3.14 -by (simp_tac (rank_ss addsimps (rank_te_owr1::TyEnv.case_eqns)) 1);
    3.15 +by (simp_tac (rank_ss addsimps rank_te_owr1::TyEnv.case_eqns) 1);
    3.16  qed "te_rec_owr";
    3.17  
    3.18  Goalw [te_dom_def] "te_dom(te_emp) = 0";
     4.1 --- a/src/ZF/List.ML	Tue Sep 22 13:49:22 1998 +0200
     4.2 +++ b/src/ZF/List.ML	Tue Sep 22 13:50:57 1998 +0200
     4.3 @@ -61,7 +61,7 @@
     4.4  \       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
     4.5  \    |] ==> list_case(c,h,l) : C(l)";
     4.6  by (rtac (major RS list.induct) 1);
     4.7 -by (ALLGOALS (asm_simp_tac (simpset() addsimps (list.case_eqns @ prems))));
     4.8 +by (ALLGOALS (asm_simp_tac (simpset() addsimps list.case_eqns @ prems)));
     4.9  qed "list_case_type";
    4.10  
    4.11  
    4.12 @@ -135,7 +135,7 @@
    4.13  
    4.14  Goal "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
    4.15  by (rtac (list_rec_def RS def_Vrec RS trans) 1);
    4.16 -by (simp_tac (rank_ss addsimps (rank_Cons2::list.case_eqns)) 1);
    4.17 +by (simp_tac (rank_ss addsimps rank_Cons2::list.case_eqns) 1);
    4.18  qed "list_rec_Cons";
    4.19  
    4.20  Addsimps [list_rec_Nil, list_rec_Cons];
     5.1 --- a/src/ZF/Nat.ML	Tue Sep 22 13:49:22 1998 +0200
     5.2 +++ b/src/ZF/Nat.ML	Tue Sep 22 13:50:57 1998 +0200
     5.3 @@ -142,7 +142,7 @@
     5.4  by (nat_ind_tac "n" prems 1);
     5.5  by (ALLGOALS
     5.6      (asm_simp_tac
     5.7 -     (simpset() addsimps (prems@distrib_simps@[le0_iff, le_succ_iff]))));
     5.8 +     (simpset() addsimps prems @ distrib_simps @ [le0_iff, le_succ_iff])));
     5.9  qed "nat_induct_from_lemma";
    5.10  
    5.11  (*Induction starting from m rather than 0*)
     6.1 --- a/src/ZF/OrdQuant.ML	Tue Sep 22 13:49:22 1998 +0200
     6.2 +++ b/src/ZF/OrdQuant.ML	Tue Sep 22 13:50:57 1998 +0200
     6.3 @@ -88,7 +88,7 @@
     6.4      "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
     6.5   (fn prems=>
     6.6        [ rtac equality_iffI 1,
     6.7 -        simp_tac (simpset() addcongs [oex_cong] addsimps (OUN_iff::prems)) 1 ]);
     6.8 +        simp_tac (simpset() addcongs [oex_cong] addsimps OUN_iff::prems) 1 ]);
     6.9  
    6.10  AddSIs [oallI];
    6.11  AddIs  [oexI, OUN_I];
     7.1 --- a/src/ZF/OrderType.ML	Tue Sep 22 13:49:22 1998 +0200
     7.2 +++ b/src/ZF/OrderType.ML	Tue Sep 22 13:50:57 1998 +0200
     7.3 @@ -793,7 +793,7 @@
     7.4  val prems = 
     7.5  Goal "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
     7.6  \     i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
     7.7 -by (asm_simp_tac (simpset() addsimps (prems@[Ord_UN, omult_unfold])) 1);
     7.8 +by (asm_simp_tac (simpset() addsimps prems @ [Ord_UN, omult_unfold]) 1);
     7.9  by (Blast_tac 1);
    7.10  qed "omult_UN";
    7.11  
     8.1 --- a/src/ZF/Perm.ML	Tue Sep 22 13:49:22 1998 +0200
     8.2 +++ b/src/ZF/Perm.ML	Tue Sep 22 13:50:57 1998 +0200
     8.3 @@ -39,7 +39,7 @@
     8.4  \       !!y. y:B ==> c(d(y)) = y        \
     8.5  \    |] ==> (lam x:A. c(x)) : surj(A,B)";
     8.6  by (res_inst_tac [("d", "d")] f_imp_surjective 1);
     8.7 -by (ALLGOALS (asm_simp_tac (simpset() addsimps ([lam_type]@prems)) ));
     8.8 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems) ));
     8.9  qed "lam_surjective";
    8.10  
    8.11  (*Cantor's theorem revisited*)
    8.12 @@ -79,7 +79,7 @@
    8.13  \       !!x. x:A ==> d(c(x)) = x        \
    8.14  \    |] ==> (lam x:A. c(x)) : inj(A,B)";
    8.15  by (res_inst_tac [("d", "d")] f_imp_injective 1);
    8.16 -by (ALLGOALS (asm_simp_tac (simpset() addsimps ([lam_type]@prems)) ));
    8.17 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [lam_type]@prems)));
    8.18  qed "lam_injective";
    8.19  
    8.20  (** Bijections **)
     9.1 --- a/src/ZF/ROOT.ML	Tue Sep 22 13:49:22 1998 +0200
     9.2 +++ b/src/ZF/ROOT.ML	Tue Sep 22 13:50:57 1998 +0200
     9.3 @@ -38,9 +38,15 @@
     9.4  use     "typechk.ML";
     9.5  use_thy "InfDatatype";
     9.6  use_thy "List";
     9.7 -use_thy "EquivClass";
     9.8  
     9.9 -(*printing functions are inherited from FOL*)
    9.10 +(*Integers & binary integer arithmetic*)
    9.11 +cd "Integ";
    9.12 +use_thy "Bin";
    9.13 +cd "..";
    9.14 +
    9.15 +(*the all-in-one theory*)
    9.16 +use_thy "Main";
    9.17 +
    9.18  print_depth 8;
    9.19  
    9.20  Goal "True";  (*leave subgoal package empty*)
    10.1 --- a/src/ZF/ex/LList.ML	Tue Sep 22 13:49:22 1998 +0200
    10.2 +++ b/src/ZF/ex/LList.ML	Tue Sep 22 13:50:57 1998 +0200
    10.3 @@ -160,7 +160,7 @@
    10.4  by (etac llist.elim 1);
    10.5  by (ALLGOALS Asm_simp_tac);
    10.6  by (ALLGOALS 
    10.7 -    (asm_simp_tac (simpset() addsimps ([QInl_def,QInr_def]@llist.con_defs))));
    10.8 +    (asm_simp_tac (simpset() addsimps [QInl_def,QInr_def] @ llist.con_defs)));
    10.9  (*LCons case*)
   10.10  by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
   10.11  qed "flip_llist_quniv_lemma";
    11.1 --- a/src/ZF/ex/Limit.ML	Tue Sep 22 13:49:22 1998 +0200
    11.2 +++ b/src/ZF/ex/Limit.ML	Tue Sep 22 13:50:57 1998 +0200
    11.3 @@ -1530,7 +1530,7 @@
    11.4  val prems = goal Limit.thy  (* e_less_succ_emb *)
    11.5      "[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==>   \
    11.6  \    e_less(DD,ee,m,succ(m)) = ee`m";
    11.7 -by (asm_simp_tac(simpset() addsimps(e_less_succ::prems)) 1);
    11.8 +by (asm_simp_tac(simpset() addsimps e_less_succ::prems) 1);
    11.9  by (stac comp_id 1);
   11.10  brr(emb_cont::cont_fun::refl::prems) 1;
   11.11  qed "e_less_succ_emb";
   11.12 @@ -1822,15 +1822,15 @@
   11.13  val prems = goal Limit.thy  (* eps_succ_ee *)
   11.14      "[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==>  \
   11.15  \    eps(DD,ee,m,succ(m)) = ee`m";
   11.16 -by (asm_simp_tac(simpset() addsimps(eps_e_less::le_succ_iff::e_less_succ_emb::
   11.17 -   prems)) 1);
   11.18 +by (asm_simp_tac(simpset() addsimps eps_e_less::le_succ_iff::e_less_succ_emb::
   11.19 +   prems) 1);
   11.20  qed "eps_succ_ee";
   11.21  
   11.22  Goal  (* eps_succ_Rp *)
   11.23      "[|emb_chain(DD,ee); m:nat|] ==>  \
   11.24  \    eps(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)";
   11.25 -by (asm_simp_tac(simpset() addsimps(eps_e_gr::le_succ_iff::e_gr_succ_emb::
   11.26 -   prems)) 1);
   11.27 +by (asm_simp_tac(simpset() addsimps eps_e_gr::le_succ_iff::e_gr_succ_emb::
   11.28 +   prems) 1);
   11.29  qed "eps_succ_Rp";
   11.30  
   11.31  Goal  (* eps_cont *)
    12.1 --- a/src/ZF/indrule.ML	Tue Sep 22 13:49:22 1998 +0200
    12.2 +++ b/src/ZF/indrule.ML	Tue Sep 22 13:50:57 1998 +0200
    12.3 @@ -226,7 +226,7 @@
    12.4                (*some risk of excessive simplification here -- might have
    12.5                  to identify the bare minimum set of rewrites*)
    12.6                full_simp_tac 
    12.7 -                 (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
    12.8 +                 (mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1
    12.9                THEN
   12.10                (*unpackage and use "prem" in the corresponding place*)
   12.11                REPEAT (rtac impI 1)  THEN