Mod because of new solver interface.
authornipkow
Tue Sep 21 19:11:07 1999 +0200 (1999-09-21)
changeset 7570a9391550eea1
parent 7569 1d9263172b54
child 7571 44e9db3150f6
Mod because of new solver interface.
src/FOL/simpdata.ML
src/HOL/Arith.ML
src/HOL/List.ML
src/HOL/TLA/Memory/MemoryImplementation.ML
src/HOL/WF.ML
src/HOL/simpdata.ML
src/HOLCF/HOLCF.ML
src/HOLCF/Lift.ML
src/Provers/Arith/fast_lin_arith.ML
src/Sequents/simpdata.ML
src/ZF/Order.ML
src/ZF/Perm.ML
src/ZF/Tools/inductive_package.ML
src/ZF/WF.ML
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -325,8 +325,8 @@
     1.4  (*No simprules, but basic infastructure for simplification*)
     1.5  val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
     1.6                              addsimprocs [defALL_regroup,defEX_regroup]
     1.7 -			    setSSolver   safe_solver
     1.8 -			    setSolver  unsafe_solver
     1.9 +			    setSSolver  (mk_solver "FOL safe" safe_solver)
    1.10 +			    setSolver  (mk_solver "FOL unsafe" unsafe_solver)
    1.11  			    setmksimps (mksimps mksimps_pairs);
    1.12  
    1.13  
     2.1 --- a/src/HOL/Arith.ML	Tue Sep 21 19:10:39 1999 +0200
     2.2 +++ b/src/HOL/Arith.ML	Tue Sep 21 19:11:07 1999 +0200
     2.3 @@ -1000,7 +1000,8 @@
     2.4  fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
     2.5  solver all the time rather than add the additional check. *)
     2.6  
     2.7 -simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac);
     2.8 +simpset_ref () := (simpset() addSolver
     2.9 +   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
    2.10  
    2.11  (* Elimination of `-' on nat due to John Harrison *)
    2.12  Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
     3.1 --- a/src/HOL/List.ML	Tue Sep 21 19:10:39 1999 +0200
     3.2 +++ b/src/HOL/List.ML	Tue Sep 21 19:11:07 1999 +0200
     3.3 @@ -804,6 +804,7 @@
     3.4  by (exhaust_tac "na" 1);
     3.5   by Auto_tac;
     3.6  qed_spec_mp "take_take";
     3.7 +Addsimps [take_take];
     3.8  
     3.9  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
    3.10  by (induct_tac "m" 1);
    3.11 @@ -811,6 +812,7 @@
    3.12  by (exhaust_tac "xs" 1);
    3.13   by Auto_tac;
    3.14  qed_spec_mp "drop_drop";
    3.15 +Addsimps [drop_drop];
    3.16  
    3.17  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
    3.18  by (induct_tac "m" 1);
     4.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Sep 21 19:10:39 1999 +0200
     4.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Sep 21 19:11:07 1999 +0200
     4.3 @@ -28,7 +28,7 @@
     4.4    let 
     4.5      val (cs,ss) = MI_css
     4.6    in
     4.7 -    (cs addSEs [squareE], ss addSSolver (fn thms => assume_tac ORELSE' (etac notE)))
     4.8 +    (cs addSEs [squareE], ss addSSolver (mk_solver "" (fn thms => assume_tac ORELSE' (etac notE))))
     4.9  end;
    4.10  
    4.11  val temp_elim = make_elim o temp_use;
     5.1 --- a/src/HOL/WF.ML	Tue Sep 21 19:10:39 1999 +0200
     5.2 +++ b/src/HOL/WF.ML	Tue Sep 21 19:11:07 1999 +0200
     5.3 @@ -260,7 +260,7 @@
     5.4      (cut_facts_tac hyps THEN'
     5.5         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
     5.6                          eresolve_tac [transD, mp, allE]));
     5.7 -val wf_super_ss = HOL_ss addSolver indhyp_tac;
     5.8 +val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac);
     5.9  
    5.10  Goalw [is_recfun_def,cut_def]
    5.11      "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
     6.1 --- a/src/HOL/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
     6.2 +++ b/src/HOL/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
     6.3 @@ -429,14 +429,18 @@
     6.4  
     6.5  fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
     6.6  
     6.7 -fun unsafe_solver prems = FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems),
     6.8 -				 atac         ,       etac  FalseE ];
     6.9 +fun unsafe_solver_tac prems =
    6.10 +  FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
    6.11 +val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
    6.12 +
    6.13  (*No premature instantiation of variables during simplification*)
    6.14 -fun   safe_solver prems = FIRST'[  match_tac(reflexive_thm::TrueI::refl::prems),
    6.15 -				 eq_assume_tac, ematch_tac [FalseE]];
    6.16 +fun safe_solver_tac prems =
    6.17 +  FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
    6.18 +         eq_assume_tac, ematch_tac [FalseE]];
    6.19 +val safe_solver = mk_solver "HOL safe" safe_solver_tac;
    6.20  
    6.21  val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
    6.22 -			    setSSolver   safe_solver
    6.23 +			    setSSolver safe_solver
    6.24  			    setSolver  unsafe_solver
    6.25  			    setmksimps (mksimps mksimps_pairs)
    6.26  			    setmkeqTrue mk_eq_True;
     7.1 --- a/src/HOLCF/HOLCF.ML	Tue Sep 21 19:10:39 1999 +0200
     7.2 +++ b/src/HOLCF/HOLCF.ML	Tue Sep 21 19:11:07 1999 +0200
     7.3 @@ -8,7 +8,7 @@
     7.4  
     7.5  use"adm.ML";
     7.6  
     7.7 -simpset_ref() := simpset() addSolver(fn thms =>
     7.8 -            (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
     7.9 +simpset_ref() := simpset() addSolver
    7.10 +   (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
    7.11  
    7.12  val HOLCF_ss = simpset();
     8.1 --- a/src/HOLCF/Lift.ML	Tue Sep 21 19:10:39 1999 +0200
     8.2 +++ b/src/HOLCF/Lift.ML	Tue Sep 21 19:11:07 1999 +0200
     8.3 @@ -71,7 +71,8 @@
     8.4                    REPEAT (cont_tac i);
     8.5  
     8.6  
     8.7 -simpset_ref() := simpset() addSolver (K (DEPTH_SOLVE_1 o cont_tac));
     8.8 +simpset_ref() := simpset() addSolver
     8.9 +  (mk_solver "cont_tac" (K (DEPTH_SOLVE_1 o cont_tac)));
    8.10  
    8.11  
    8.12  
     9.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 21 19:10:39 1999 +0200
     9.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Sep 21 19:11:07 1999 +0200
     9.3 @@ -277,7 +277,7 @@
     9.4          | mk(NotLeD(j)) = ((*writeln"NLe";prth*)(mk j RS LA_Logic.not_leD))
     9.5          | mk(NotLeDD(j)) = ((*writeln"NLeD";prth*)(hd([mk j RS LA_Logic.not_leD] RL !LA_Data.lessD)))
     9.6          | mk(NotLessD(j)) = ((*writeln"NL";prth*)(mk j RS LA_Logic.not_lessD))
     9.7 -        | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp(prth(addthms (mk j1) (mk j2)))))
     9.8 +        | mk(Added(j1,j2)) = ((*writeln"+";prth*)(simp((*prth*)(addthms (mk j1) (mk j2)))))
     9.9          | mk(Multiplied(n,j)) = ((*writeln"*";*)multn(n,mk j))
    9.10  
    9.11    in (*writeln"mkthm";*)!LA_Data.simp(mk just) handle FalseE thm => thm end
    10.1 --- a/src/Sequents/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
    10.2 +++ b/src/Sequents/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
    10.3 @@ -241,8 +241,8 @@
    10.4  
    10.5  (*No simprules, but basic infrastructure for simplification*)
    10.6  val LK_basic_ss = empty_ss setsubgoaler asm_simp_tac
    10.7 -			   setSSolver   safe_solver
    10.8 -			   setSolver    unsafe_solver
    10.9 +			   setSSolver   (mk_solver "safe" safe_solver)
   10.10 +			   setSolver    (mk_solver "unsafe" unsafe_solver)
   10.11  			   setmksimps   (map mk_meta_eq o atomize o gen_all);
   10.12  
   10.13  val LK_simps =
    11.1 --- a/src/ZF/Order.ML	Tue Sep 21 19:10:39 1999 +0200
    11.2 +++ b/src/ZF/Order.ML	Tue Sep 21 19:11:07 1999 +0200
    11.3 @@ -242,9 +242,9 @@
    11.4  
    11.5  (*Rewriting with bijections and converse (function inverse)*)
    11.6  val bij_inverse_ss = 
    11.7 -    simpset() setSolver 
    11.8 -      type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
    11.9 -				       inj_is_fun, comp_fun, comp_bij])
   11.10 +    simpset() setSolver (mk_solver ""
   11.11 +      (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
   11.12 +				        inj_is_fun, comp_fun, comp_bij])))
   11.13            addsimps [right_inverse_bij];
   11.14  
   11.15  Goalw [ord_iso_def] 
    12.1 --- a/src/ZF/Perm.ML	Tue Sep 21 19:10:39 1999 +0200
    12.2 +++ b/src/ZF/Perm.ML	Tue Sep 21 19:11:07 1999 +0200
    12.3 @@ -344,8 +344,8 @@
    12.4  by (rtac lam_funtype 2);
    12.5  by (typecheck_tac (tcset() addTCs [prem]));
    12.6  by (asm_simp_tac (simpset() 
    12.7 -                   setSolver 
    12.8 -                   type_solver_tac (tcset() addTCs [prem, lam_funtype])) 1);
    12.9 +                   setSolver (mk_solver ""
   12.10 +                   (type_solver_tac (tcset() addTCs [prem, lam_funtype])))) 1);
   12.11  qed "comp_lam";
   12.12  
   12.13  Goal "[| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
   12.14 @@ -353,8 +353,8 @@
   12.15      f_imp_injective 1);
   12.16  by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
   12.17  by (asm_simp_tac (simpset()  
   12.18 -		  setSolver
   12.19 -		  type_solver_tac (tcset() addTCs [inj_is_fun])) 1);
   12.20 +		  setSolver (mk_solver ""
   12.21 +		  (type_solver_tac (tcset() addTCs [inj_is_fun])))) 1);
   12.22  qed "comp_inj";
   12.23  
   12.24  Goalw [surj_def]
    13.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Sep 21 19:10:39 1999 +0200
    13.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 21 19:11:07 1999 +0200
    13.3 @@ -335,9 +335,10 @@
    13.4         If the premises get simplified, then the proofs could fail.*)
    13.5       val min_ss = empty_ss
    13.6  	   setmksimps (map mk_eq o ZF_atomize o gen_all)
    13.7 -	   setSolver  (fn prems => resolve_tac (triv_rls@prems) 
    13.8 +	   setSolver (mk_solver "minimal"
    13.9 +                      (fn prems => resolve_tac (triv_rls@prems) 
   13.10  				   ORELSE' assume_tac
   13.11 -				   ORELSE' etac FalseE);
   13.12 +				   ORELSE' etac FalseE));
   13.13  
   13.14       val quant_induct = 
   13.15  	 prove_goalw_cterm part_rec_defs 
    14.1 --- a/src/ZF/WF.ML	Tue Sep 21 19:10:39 1999 +0200
    14.2 +++ b/src/ZF/WF.ML	Tue Sep 21 19:11:07 1999 +0200
    14.3 @@ -229,7 +229,7 @@
    14.4                          eresolve_tac [underD, transD, spec RS mp]));
    14.5  
    14.6  (*** NOTE! some simplifications need a different solver!! ***)
    14.7 -val wf_super_ss = simpset() setSolver indhyp_tac;
    14.8 +val wf_super_ss = simpset() setSolver (mk_solver "WF" indhyp_tac);
    14.9  
   14.10  Goalw [is_recfun_def]
   14.11      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
    15.1 --- a/src/ZF/simpdata.ML	Tue Sep 21 19:10:39 1999 +0200
    15.2 +++ b/src/ZF/simpdata.ML	Tue Sep 21 19:11:07 1999 +0200
    15.3 @@ -107,6 +107,6 @@
    15.4  
    15.5  simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
    15.6                             addsplits [split_if]
    15.7 -                           setSolver Type_solver_tac;
    15.8 +                           setSolver (mk_solver "types" Type_solver_tac);
    15.9  
   15.10  val ZF_ss = simpset();