renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
authorwenzelm
Thu Jul 05 20:01:31 2007 +0200 (2007-07-05)
changeset 23594e65e466dda01
parent 23593 fd12f7d56bd7
child 23595 7ca68a2c8575
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
added flat_rule filter for addXXs etc.;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Thu Jul 05 20:01:30 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Jul 05 20:01:31 2007 +0200
     1.3 @@ -198,6 +198,8 @@
     1.4      in if Thm.equiv_thm (rule, rule'') then rule else rule'' end
     1.5    else rule;
     1.6  
     1.7 +(*flatten nested meta connectives in prems*)
     1.8 +val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
     1.9  
    1.10  
    1.11  (*** Useful tactics for classical reasoning ***)
    1.12 @@ -364,8 +366,9 @@
    1.13           (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
    1.14            cs)
    1.15    else
    1.16 -  let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.17 -          List.partition Thm.no_prems [th]
    1.18 +  let val th' = flat_rule th
    1.19 +      val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.20 +          List.partition Thm.no_prems [th']
    1.21        val nI = length safeIs + 1
    1.22        and nE = length safeEs
    1.23    in warn_dup th cs;
    1.24 @@ -392,7 +395,7 @@
    1.25      	error("Ill-formed elimination rule\n" ^ string_of_thm th)
    1.26    else
    1.27    let
    1.28 -      val th' = classical_rule th
    1.29 +      val th' = classical_rule (flat_rule th)
    1.30        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
    1.31            List.partition (fn rl => nprems_of rl=1) [th']
    1.32        val nI = length safeIs
    1.33 @@ -431,12 +434,13 @@
    1.34           (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
    1.35            cs)
    1.36    else
    1.37 -  let val nI = length hazIs + 1
    1.38 +  let val th' = flat_rule th
    1.39 +      val nI = length hazIs + 1
    1.40        and nE = length hazEs
    1.41    in warn_dup th cs;
    1.42       CS{hazIs   = th::hazIs,
    1.43 -        haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
    1.44 -        dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
    1.45 +        haz_netpair = insert (nI,nE) ([th'], []) haz_netpair,
    1.46 +        dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair,
    1.47          safeIs  = safeIs,
    1.48          safeEs  = safeEs,
    1.49          hazEs   = hazEs,
    1.50 @@ -459,7 +463,7 @@
    1.51      	error("Ill-formed elimination rule\n" ^ string_of_thm th)
    1.52    else
    1.53    let
    1.54 -      val th' = classical_rule th
    1.55 +      val th' = classical_rule (flat_rule th)
    1.56        val nI = length hazIs
    1.57        and nE = length hazEs + 1
    1.58    in warn_dup th cs;
    1.59 @@ -491,7 +495,8 @@
    1.60            (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.61                      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.62   if mem_thm safeIs th then
    1.63 -   let val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th]
    1.64 +   let val th' = flat_rule th
    1.65 +       val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']
    1.66     in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
    1.67           safep_netpair = delete (safep_rls, []) safep_netpair,
    1.68           safeIs = rem_thm th safeIs,
    1.69 @@ -511,7 +516,7 @@
    1.70                      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.71    if mem_thm safeEs th then
    1.72      let
    1.73 -      val th' = classical_rule th
    1.74 +      val th' = classical_rule (flat_rule th)
    1.75        val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
    1.76      in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
    1.77           safep_netpair = delete ([], safep_rls) safep_netpair,
    1.78 @@ -532,8 +537,9 @@
    1.79           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.80                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.81   if mem_thm hazIs th then
    1.82 -     CS{haz_netpair = delete ([th], []) haz_netpair,
    1.83 -        dup_netpair = delete ([dup_intr th], []) dup_netpair,
    1.84 +    let val th' = flat_rule th
    1.85 +    in CS{haz_netpair = delete ([th'], []) haz_netpair,
    1.86 +        dup_netpair = delete ([dup_intr th'], []) dup_netpair,
    1.87          safeIs  = safeIs,
    1.88          safeEs  = safeEs,
    1.89          hazIs   = rem_thm th hazIs,
    1.90 @@ -543,6 +549,7 @@
    1.91          safe0_netpair = safe0_netpair,
    1.92          safep_netpair = safep_netpair,
    1.93          xtra_netpair = delete' ([th], []) xtra_netpair}
    1.94 +    end
    1.95   else cs
    1.96   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
    1.97          error ("Ill-formed introduction rule\n" ^ string_of_thm th);
    1.98 @@ -551,9 +558,9 @@
    1.99  fun delE th
   1.100           (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.101                     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.102 -  let val th' = classical_rule th in
   1.103 -    if mem_thm hazEs th then
   1.104 -     CS{haz_netpair = delete ([], [th']) haz_netpair,
   1.105 + if mem_thm hazEs th then
   1.106 +   let val th' = classical_rule (flat_rule th)
   1.107 +   in CS{haz_netpair = delete ([], [th']) haz_netpair,
   1.108          dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   1.109          safeIs  = safeIs,
   1.110          safeEs  = safeEs,
   1.111 @@ -564,9 +571,8 @@
   1.112          safe0_netpair = safe0_netpair,
   1.113          safep_netpair = safep_netpair,
   1.114          xtra_netpair = delete' ([], [th]) xtra_netpair}
   1.115 -     else cs
   1.116 -   end;
   1.117 -
   1.118 +   end
   1.119 + else cs;
   1.120  
   1.121  (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   1.122  fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   1.123 @@ -745,24 +751,24 @@
   1.124  
   1.125  (*Dumb but fast*)
   1.126  fun fast_tac cs =
   1.127 -  ObjectLogic.atomize_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   1.128 +  ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   1.129  
   1.130  (*Slower but smarter than fast_tac*)
   1.131  fun best_tac cs =
   1.132 -  ObjectLogic.atomize_tac THEN'
   1.133 +  ObjectLogic.atomize_prems_tac THEN'
   1.134    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   1.135  
   1.136  (*even a bit smarter than best_tac*)
   1.137  fun first_best_tac cs =
   1.138 -  ObjectLogic.atomize_tac THEN'
   1.139 +  ObjectLogic.atomize_prems_tac THEN'
   1.140    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   1.141  
   1.142  fun slow_tac cs =
   1.143 -  ObjectLogic.atomize_tac THEN'
   1.144 +  ObjectLogic.atomize_prems_tac THEN'
   1.145    SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   1.146  
   1.147  fun slow_best_tac cs =
   1.148 -  ObjectLogic.atomize_tac THEN'
   1.149 +  ObjectLogic.atomize_prems_tac THEN'
   1.150    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   1.151  
   1.152  
   1.153 @@ -770,13 +776,13 @@
   1.154  val weight_ASTAR = ref 5;
   1.155  
   1.156  fun astar_tac cs =
   1.157 -  ObjectLogic.atomize_tac THEN'
   1.158 +  ObjectLogic.atomize_prems_tac THEN'
   1.159    SELECT_GOAL
   1.160      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   1.161        (step_tac cs 1));
   1.162  
   1.163  fun slow_astar_tac cs =
   1.164 -  ObjectLogic.atomize_tac THEN'
   1.165 +  ObjectLogic.atomize_prems_tac THEN'
   1.166    SELECT_GOAL
   1.167      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   1.168        (slow_step_tac cs 1));