atomize: all automated tactics that "solve" goals;
authorwenzelm
Fri Nov 03 21:29:56 2000 +0100 (2000-11-03 ago)
changeset 103821fb807260ff1
parent 10381 4dfbcad19bfb
child 10383 a092ae7bb2a6
atomize: all automated tactics that "solve" goals;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Fri Nov 03 21:28:15 2000 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Nov 03 21:29:56 2000 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4    val classical : thm           (* (~P ==> P) ==> P *)
     1.5    val sizef     : thm -> int    (* size function for BEST_FIRST *)
     1.6    val hyp_subst_tacs: (int -> tactic) list
     1.7 +  val atomize: thm list
     1.8  end;
     1.9  
    1.10  signature BASIC_CLASSICAL =
    1.11 @@ -182,6 +183,8 @@
    1.12  
    1.13  (*** Useful tactics for classical reasoning ***)
    1.14  
    1.15 +val atomize_tac = Method.atomize_tac atomize;
    1.16 +
    1.17  val imp_elim = (*cannot use bind_thm within a structure!*)
    1.18    store_thm ("imp_elim", Data.make_elim mp);
    1.19  
    1.20 @@ -832,34 +835,42 @@
    1.21  (**** The following tactics all fail unless they solve one goal ****)
    1.22  
    1.23  (*Dumb but fast*)
    1.24 -fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    1.25 +fun fast_tac cs =
    1.26 +  atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    1.27  
    1.28  (*Slower but smarter than fast_tac*)
    1.29 -fun best_tac cs = 
    1.30 +fun best_tac cs =
    1.31 +  atomize_tac THEN'
    1.32    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
    1.33  
    1.34  (*even a bit smarter than best_tac*)
    1.35 -fun first_best_tac cs = 
    1.36 +fun first_best_tac cs =
    1.37 +  atomize_tac THEN'
    1.38    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
    1.39  
    1.40 -fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
    1.41 +fun slow_tac cs =
    1.42 +  atomize_tac THEN'
    1.43 +  SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
    1.44  
    1.45 -fun slow_best_tac cs = 
    1.46 +fun slow_best_tac cs =
    1.47 +  atomize_tac THEN'
    1.48    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
    1.49  
    1.50  
    1.51  (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
    1.52  val weight_ASTAR = ref 5; 
    1.53  
    1.54 -fun astar_tac cs = 
    1.55 -  SELECT_GOAL ( ASTAR (has_fewer_prems 1
    1.56 -              , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
    1.57 -              (step_tac cs 1));
    1.58 +fun astar_tac cs =
    1.59 +  atomize_tac THEN' 
    1.60 +  SELECT_GOAL
    1.61 +    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
    1.62 +      (step_tac cs 1));
    1.63  
    1.64  fun slow_astar_tac cs = 
    1.65 -  SELECT_GOAL ( ASTAR (has_fewer_prems 1
    1.66 -              , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
    1.67 -              (slow_step_tac cs 1));
    1.68 +  atomize_tac THEN' 
    1.69 +  SELECT_GOAL
    1.70 +    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
    1.71 +      (slow_step_tac cs 1));
    1.72  
    1.73  (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
    1.74    of much experimentation!  Changing APPEND to ORELSE below would prove
    1.75 @@ -1111,12 +1122,14 @@
    1.76  fun rule_tac [] cs facts = some_rule_tac cs facts
    1.77    | rule_tac rules _ facts = Method.rule_tac rules facts;
    1.78  
    1.79 -fun default_tac rules cs facts =
    1.80 -  rule_tac rules cs facts ORELSE' AxClass.default_intro_classes_tac facts;
    1.81 +fun default_tac rules ctxt cs facts =
    1.82 +  rule_tac rules cs facts ORELSE'
    1.83 +  Method.some_rule_tac rules ctxt facts ORELSE'
    1.84 +  AxClass.default_intro_classes_tac facts;
    1.85  
    1.86  in
    1.87    val rule = METHOD_CLASET' o rule_tac;
    1.88 -  val default = METHOD_CLASET' o default_tac;
    1.89 +  fun default rules ctxt = METHOD_CLASET' (default_tac rules ctxt) ctxt;
    1.90  end;
    1.91  
    1.92