src/Provers/classical.ML
changeset 42790 e07e56300faa
parent 42439 9efdd0af15ac
child 42791 36f787ae5f70
     1.1 --- a/src/Provers/classical.ML	Fri May 13 14:39:55 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri May 13 15:47:54 2011 +0200
     1.3 @@ -25,11 +25,11 @@
     1.4  
     1.5  signature CLASSICAL_DATA =
     1.6  sig
     1.7 -  val imp_elim  : thm           (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
     1.8 -  val not_elim  : thm           (* ~P ==> P ==> R *)
     1.9 -  val swap      : thm           (* ~ P ==> (~ R ==> P) ==> R *)
    1.10 -  val classical : thm           (* (~ P ==> P) ==> P *)
    1.11 -  val sizef     : thm -> int    (* size function for BEST_FIRST *)
    1.12 +  val imp_elim: thm  (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *)
    1.13 +  val not_elim: thm  (* ~P ==> P ==> R *)
    1.14 +  val swap: thm  (* ~ P ==> (~ R ==> P) ==> R *)
    1.15 +  val classical: thm  (* (~ P ==> P) ==> P *)
    1.16 +  val sizef: thm -> int  (* size function for BEST_FIRST *)
    1.17    val hyp_subst_tacs: (int -> tactic) list
    1.18  end;
    1.19  
    1.20 @@ -38,71 +38,75 @@
    1.21    type claset
    1.22    val empty_cs: claset
    1.23    val print_cs: Proof.context -> claset -> unit
    1.24 -  val rep_cs:
    1.25 -    claset -> {safeIs: thm list, safeEs: thm list,
    1.26 -                 hazIs: thm list, hazEs: thm list,
    1.27 -                 swrappers: (string * wrapper) list,
    1.28 -                 uwrappers: (string * wrapper) list,
    1.29 -                 safe0_netpair: netpair, safep_netpair: netpair,
    1.30 -                 haz_netpair: netpair, dup_netpair: netpair,
    1.31 -                 xtra_netpair: Context_Rules.netpair}
    1.32 -  val merge_cs          : claset * claset -> claset
    1.33 -  val addDs             : claset * thm list -> claset
    1.34 -  val addEs             : claset * thm list -> claset
    1.35 -  val addIs             : claset * thm list -> claset
    1.36 -  val addSDs            : claset * thm list -> claset
    1.37 -  val addSEs            : claset * thm list -> claset
    1.38 -  val addSIs            : claset * thm list -> claset
    1.39 -  val delrules          : claset * thm list -> claset
    1.40 -  val addSWrapper       : claset * (string * wrapper) -> claset
    1.41 -  val delSWrapper       : claset *  string            -> claset
    1.42 -  val addWrapper        : claset * (string * wrapper) -> claset
    1.43 -  val delWrapper        : claset *  string            -> claset
    1.44 -  val addSbefore        : claset * (string * (int -> tactic)) -> claset
    1.45 -  val addSafter         : claset * (string * (int -> tactic)) -> claset
    1.46 -  val addbefore         : claset * (string * (int -> tactic)) -> claset
    1.47 -  val addafter          : claset * (string * (int -> tactic)) -> claset
    1.48 -  val addD2             : claset * (string * thm) -> claset
    1.49 -  val addE2             : claset * (string * thm) -> claset
    1.50 -  val addSD2            : claset * (string * thm) -> claset
    1.51 -  val addSE2            : claset * (string * thm) -> claset
    1.52 -  val appSWrappers      : claset -> wrapper
    1.53 -  val appWrappers       : claset -> wrapper
    1.54 +  val rep_cs: claset ->
    1.55 +   {safeIs: thm list,
    1.56 +    safeEs: thm list,
    1.57 +    hazIs: thm list,
    1.58 +    hazEs: thm list,
    1.59 +    swrappers: (string * wrapper) list,
    1.60 +    uwrappers: (string * wrapper) list,
    1.61 +    safe0_netpair: netpair,
    1.62 +    safep_netpair: netpair,
    1.63 +    haz_netpair: netpair,
    1.64 +    dup_netpair: netpair,
    1.65 +    xtra_netpair: Context_Rules.netpair}
    1.66 +  val merge_cs: claset * claset -> claset
    1.67 +  val addDs: claset * thm list -> claset
    1.68 +  val addEs: claset * thm list -> claset
    1.69 +  val addIs: claset * thm list -> claset
    1.70 +  val addSDs: claset * thm list -> claset
    1.71 +  val addSEs: claset * thm list -> claset
    1.72 +  val addSIs: claset * thm list -> claset
    1.73 +  val delrules: claset * thm list -> claset
    1.74 +  val addSWrapper: claset * (string * wrapper) -> claset
    1.75 +  val delSWrapper: claset *  string -> claset
    1.76 +  val addWrapper: claset * (string * wrapper) -> claset
    1.77 +  val delWrapper: claset *  string -> claset
    1.78 +  val addSbefore: claset * (string * (int -> tactic)) -> claset
    1.79 +  val addSafter: claset * (string * (int -> tactic)) -> claset
    1.80 +  val addbefore: claset * (string * (int -> tactic)) -> claset
    1.81 +  val addafter: claset * (string * (int -> tactic)) -> claset
    1.82 +  val addD2: claset * (string * thm) -> claset
    1.83 +  val addE2: claset * (string * thm) -> claset
    1.84 +  val addSD2: claset * (string * thm) -> claset
    1.85 +  val addSE2: claset * (string * thm) -> claset
    1.86 +  val appSWrappers: claset -> wrapper
    1.87 +  val appWrappers: claset -> wrapper
    1.88  
    1.89 -  val global_claset_of  : theory -> claset
    1.90 -  val claset_of         : Proof.context -> claset
    1.91 +  val global_claset_of: theory -> claset
    1.92 +  val claset_of: Proof.context -> claset
    1.93  
    1.94 -  val fast_tac          : claset -> int -> tactic
    1.95 -  val slow_tac          : claset -> int -> tactic
    1.96 -  val weight_ASTAR      : int Unsynchronized.ref
    1.97 -  val astar_tac         : claset -> int -> tactic
    1.98 -  val slow_astar_tac    : claset -> int -> tactic
    1.99 -  val best_tac          : claset -> int -> tactic
   1.100 -  val first_best_tac    : claset -> int -> tactic
   1.101 -  val slow_best_tac     : claset -> int -> tactic
   1.102 -  val depth_tac         : claset -> int -> int -> tactic
   1.103 -  val deepen_tac        : claset -> int -> int -> tactic
   1.104 +  val fast_tac: claset -> int -> tactic
   1.105 +  val slow_tac: claset -> int -> tactic
   1.106 +  val weight_ASTAR: int Unsynchronized.ref
   1.107 +  val astar_tac: claset -> int -> tactic
   1.108 +  val slow_astar_tac: claset -> int -> tactic
   1.109 +  val best_tac: claset -> int -> tactic
   1.110 +  val first_best_tac: claset -> int -> tactic
   1.111 +  val slow_best_tac: claset -> int -> tactic
   1.112 +  val depth_tac: claset -> int -> int -> tactic
   1.113 +  val deepen_tac: claset -> int -> int -> tactic
   1.114  
   1.115 -  val contr_tac         : int -> tactic
   1.116 -  val dup_elim          : thm -> thm
   1.117 -  val dup_intr          : thm -> thm
   1.118 -  val dup_step_tac      : claset -> int -> tactic
   1.119 -  val eq_mp_tac         : int -> tactic
   1.120 -  val haz_step_tac      : claset -> int -> tactic
   1.121 -  val joinrules         : thm list * thm list -> (bool * thm) list
   1.122 -  val mp_tac            : int -> tactic
   1.123 -  val safe_tac          : claset -> tactic
   1.124 -  val safe_steps_tac    : claset -> int -> tactic
   1.125 -  val safe_step_tac     : claset -> int -> tactic
   1.126 -  val clarify_tac       : claset -> int -> tactic
   1.127 -  val clarify_step_tac  : claset -> int -> tactic
   1.128 -  val step_tac          : claset -> int -> tactic
   1.129 -  val slow_step_tac     : claset -> int -> tactic
   1.130 -  val swapify           : thm list -> thm list
   1.131 -  val swap_res_tac      : thm list -> int -> tactic
   1.132 -  val inst_step_tac     : claset -> int -> tactic
   1.133 -  val inst0_step_tac    : claset -> int -> tactic
   1.134 -  val instp_step_tac    : claset -> int -> tactic
   1.135 +  val contr_tac: int -> tactic
   1.136 +  val dup_elim: thm -> thm
   1.137 +  val dup_intr: thm -> thm
   1.138 +  val dup_step_tac: claset -> int -> tactic
   1.139 +  val eq_mp_tac: int -> tactic
   1.140 +  val haz_step_tac: claset -> int -> tactic
   1.141 +  val joinrules: thm list * thm list -> (bool * thm) list
   1.142 +  val mp_tac: int -> tactic
   1.143 +  val safe_tac: claset -> tactic
   1.144 +  val safe_steps_tac: claset -> int -> tactic
   1.145 +  val safe_step_tac: claset -> int -> tactic
   1.146 +  val clarify_tac: claset -> int -> tactic
   1.147 +  val clarify_step_tac: claset -> int -> tactic
   1.148 +  val step_tac: claset -> int -> tactic
   1.149 +  val slow_step_tac: claset -> int -> tactic
   1.150 +  val swapify: thm list -> thm list
   1.151 +  val swap_res_tac: thm list -> int -> tactic
   1.152 +  val inst_step_tac: claset -> int -> tactic
   1.153 +  val inst0_step_tac: claset -> int -> tactic
   1.154 +  val instp_step_tac: claset -> int -> tactic
   1.155  end;
   1.156  
   1.157  signature CLASSICAL =
   1.158 @@ -313,151 +317,131 @@
   1.159  val mem_thm = member Thm.eq_thm_prop
   1.160  and rem_thm = remove Thm.eq_thm_prop;
   1.161  
   1.162 -(*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   1.163 -  is still allowed.*)
   1.164 -fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   1.165 -  if mem_thm safeIs th then
   1.166 -    warning ("Rule already declared as safe introduction (intro!)\n" ^
   1.167 -      Display.string_of_thm_without_context th)
   1.168 -  else if mem_thm safeEs th then
   1.169 -    warning ("Rule already declared as safe elimination (elim!)\n" ^
   1.170 -      Display.string_of_thm_without_context th)
   1.171 -  else if mem_thm hazIs th then
   1.172 -    warning ("Rule already declared as introduction (intro)\n" ^
   1.173 -      Display.string_of_thm_without_context th)
   1.174 -  else if mem_thm hazEs th then
   1.175 -    warning ("Rule already declared as elimination (elim)\n" ^
   1.176 -      Display.string_of_thm_without_context th)
   1.177 -  else ();
   1.178 +fun warn msg rules th =
   1.179 +  mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true);
   1.180 +
   1.181 +fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   1.182 +  warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
   1.183 +  warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
   1.184 +  warn "Rule already declared as introduction (intro)\n" hazIs th orelse
   1.185 +  warn "Rule already declared as elimination (elim)\n" hazEs th;
   1.186  
   1.187  
   1.188  (*** Safe rules ***)
   1.189  
   1.190  fun addSI w th
   1.191 -  (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.192 -             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.193 -  if mem_thm safeIs th then
   1.194 -    (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
   1.195 -      Display.string_of_thm_without_context th); cs)
   1.196 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.197 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.198 +  if warn "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   1.199    else
   1.200 -  let val th' = flat_rule th
   1.201 +    let
   1.202 +      val th' = flat_rule th;
   1.203        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   1.204 -          List.partition Thm.no_prems [th']
   1.205 -      val nI = length safeIs + 1
   1.206 -      and nE = length safeEs
   1.207 -  in warn_dup th cs;
   1.208 -     CS{safeIs  = th::safeIs,
   1.209 +        List.partition Thm.no_prems [th'];
   1.210 +      val nI = length safeIs + 1;
   1.211 +      val nE = length safeEs;
   1.212 +      val _ = warn_other th cs;
   1.213 +    in
   1.214 +      CS
   1.215 +       {safeIs  = th::safeIs,
   1.216          safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   1.217          safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   1.218 -        safeEs  = safeEs,
   1.219 -        hazIs   = hazIs,
   1.220 -        hazEs   = hazEs,
   1.221 -        swrappers    = swrappers,
   1.222 -        uwrappers    = uwrappers,
   1.223 -        haz_netpair  = haz_netpair,
   1.224 -        dup_netpair  = dup_netpair,
   1.225 +        safeEs = safeEs,
   1.226 +        hazIs = hazIs,
   1.227 +        hazEs = hazEs,
   1.228 +        swrappers = swrappers,
   1.229 +        uwrappers = uwrappers,
   1.230 +        haz_netpair = haz_netpair,
   1.231 +        dup_netpair = dup_netpair,
   1.232          xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
   1.233 -  end;
   1.234 +    end;
   1.235  
   1.236  fun addSE w th
   1.237 -  (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.238 -             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.239 -  if mem_thm safeEs th then
   1.240 -    (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
   1.241 -        Display.string_of_thm_without_context th); cs)
   1.242 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.243 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.244 +  if warn "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
   1.245    else if has_fewer_prems 1 th then
   1.246 -        error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   1.247 +    error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   1.248    else
   1.249 -  let
   1.250 -      val th' = classical_rule (flat_rule th)
   1.251 +    let
   1.252 +      val th' = classical_rule (flat_rule th);
   1.253        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   1.254 -          List.partition (fn rl => nprems_of rl=1) [th']
   1.255 -      val nI = length safeIs
   1.256 -      and nE = length safeEs + 1
   1.257 -  in warn_dup th cs;
   1.258 -     CS{safeEs  = th::safeEs,
   1.259 +        List.partition (fn rl => nprems_of rl=1) [th'];
   1.260 +      val nI = length safeIs;
   1.261 +      val nE = length safeEs + 1;
   1.262 +      val _ = warn_other th cs;
   1.263 +    in
   1.264 +      CS
   1.265 +       {safeEs  = th::safeEs,
   1.266          safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   1.267          safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   1.268 -        safeIs  = safeIs,
   1.269 -        hazIs   = hazIs,
   1.270 -        hazEs   = hazEs,
   1.271 -        swrappers    = swrappers,
   1.272 -        uwrappers    = uwrappers,
   1.273 -        haz_netpair  = haz_netpair,
   1.274 -        dup_netpair  = dup_netpair,
   1.275 +        safeIs = safeIs,
   1.276 +        hazIs = hazIs,
   1.277 +        hazEs = hazEs,
   1.278 +        swrappers = swrappers,
   1.279 +        uwrappers = uwrappers,
   1.280 +        haz_netpair = haz_netpair,
   1.281 +        dup_netpair = dup_netpair,
   1.282          xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   1.283 -  end;
   1.284 -
   1.285 -fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   1.286 -fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   1.287 -
   1.288 -fun make_elim th =
   1.289 -    if has_fewer_prems 1 th then
   1.290 -          error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
   1.291 -    else Tactic.make_elim th;
   1.292 -
   1.293 -fun cs addSDs ths = cs addSEs (map make_elim ths);
   1.294 +    end;
   1.295  
   1.296  
   1.297  (*** Hazardous (unsafe) rules ***)
   1.298  
   1.299  fun addI w th
   1.300 -  (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.301 -             safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.302 -  if mem_thm hazIs th then
   1.303 -    (warning ("Ignoring duplicate introduction (intro)\n" ^
   1.304 -        Display.string_of_thm_without_context th); cs)
   1.305 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.306 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.307 +  if warn "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   1.308    else
   1.309 -  let val th' = flat_rule th
   1.310 -      val nI = length hazIs + 1
   1.311 -      and nE = length hazEs
   1.312 -  in warn_dup th cs;
   1.313 -     CS{hazIs   = th::hazIs,
   1.314 -        haz_netpair = insert (nI,nE) ([th'], []) haz_netpair,
   1.315 -        dup_netpair = insert (nI,nE) (map dup_intr [th'], []) dup_netpair,
   1.316 -        safeIs  = safeIs,
   1.317 -        safeEs  = safeEs,
   1.318 -        hazEs   = hazEs,
   1.319 -        swrappers     = swrappers,
   1.320 -        uwrappers     = uwrappers,
   1.321 +    let
   1.322 +      val th' = flat_rule th;
   1.323 +      val nI = length hazIs + 1;
   1.324 +      val nE = length hazEs;
   1.325 +      val _ = warn_other th cs;
   1.326 +    in
   1.327 +      CS
   1.328 +       {hazIs = th :: hazIs,
   1.329 +        haz_netpair = insert (nI, nE) ([th'], []) haz_netpair,
   1.330 +        dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair,
   1.331 +        safeIs = safeIs,
   1.332 +        safeEs = safeEs,
   1.333 +        hazEs = hazEs,
   1.334 +        swrappers = swrappers,
   1.335 +        uwrappers = uwrappers,
   1.336          safe0_netpair = safe0_netpair,
   1.337          safep_netpair = safep_netpair,
   1.338 -        xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   1.339 -  end
   1.340 -  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   1.341 -    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   1.342 +        xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
   1.343 +    end
   1.344 +    handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
   1.345 +      error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   1.346  
   1.347  fun addE w th
   1.348 -  (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.349 -            safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.350 -  if mem_thm hazEs th then
   1.351 -    (warning ("Ignoring duplicate elimination (elim)\n" ^
   1.352 -        Display.string_of_thm_without_context th); cs)
   1.353 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.354 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.355 +  if warn "Ignoring duplicate elimination (elim)\n" hazEs th then cs
   1.356    else if has_fewer_prems 1 th then
   1.357 -        error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   1.358 +    error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   1.359    else
   1.360 -  let
   1.361 -      val th' = classical_rule (flat_rule th)
   1.362 -      val nI = length hazIs
   1.363 -      and nE = length hazEs + 1
   1.364 -  in warn_dup th cs;
   1.365 -     CS{hazEs   = th::hazEs,
   1.366 -        haz_netpair = insert (nI,nE) ([], [th']) haz_netpair,
   1.367 -        dup_netpair = insert (nI,nE) ([], map dup_elim [th']) dup_netpair,
   1.368 -        safeIs  = safeIs,
   1.369 -        safeEs  = safeEs,
   1.370 -        hazIs   = hazIs,
   1.371 -        swrappers     = swrappers,
   1.372 -        uwrappers     = uwrappers,
   1.373 +    let
   1.374 +      val th' = classical_rule (flat_rule th);
   1.375 +      val nI = length hazIs;
   1.376 +      val nE = length hazEs + 1;
   1.377 +      val _ = warn_other th cs;
   1.378 +    in
   1.379 +      CS
   1.380 +       {hazEs = th :: hazEs,
   1.381 +        haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
   1.382 +        dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair,
   1.383 +        safeIs = safeIs,
   1.384 +        safeEs = safeEs,
   1.385 +        hazIs = hazIs,
   1.386 +        swrappers = swrappers,
   1.387 +        uwrappers = uwrappers,
   1.388          safe0_netpair = safe0_netpair,
   1.389          safep_netpair = safep_netpair,
   1.390 -        xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair}
   1.391 -  end;
   1.392 +        xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
   1.393 +    end;
   1.394  
   1.395 -fun cs addIs ths = fold_rev (addI NONE) ths cs;
   1.396 -fun cs addEs ths = fold_rev (addE NONE) ths cs;
   1.397 -
   1.398 -fun cs addDs ths = cs addEs (map make_elim ths);
   1.399  
   1.400  
   1.401  (*** Deletion of rules
   1.402 @@ -466,91 +450,96 @@
   1.403  ***)
   1.404  
   1.405  fun delSI th
   1.406 -          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.407 -                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.408 - if mem_thm safeIs th then
   1.409 -   let val th' = flat_rule th
   1.410 -       val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']
   1.411 -   in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   1.412 -         safep_netpair = delete (safep_rls, []) safep_netpair,
   1.413 -         safeIs = rem_thm th safeIs,
   1.414 -         safeEs = safeEs,
   1.415 -         hazIs  = hazIs,
   1.416 -         hazEs  = hazEs,
   1.417 -         swrappers    = swrappers,
   1.418 -         uwrappers    = uwrappers,
   1.419 -         haz_netpair  = haz_netpair,
   1.420 -         dup_netpair  = dup_netpair,
   1.421 -         xtra_netpair = delete' ([th], []) xtra_netpair}
   1.422 -   end
   1.423 - else cs;
   1.424 -
   1.425 -fun delSE th
   1.426 -          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.427 -                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.428 -  if mem_thm safeEs th then
   1.429 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.430 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.431 +  if mem_thm safeIs th then
   1.432      let
   1.433 -      val th' = classical_rule (flat_rule th)
   1.434 -      val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl=1) [th']
   1.435 -    in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   1.436 -         safep_netpair = delete ([], safep_rls) safep_netpair,
   1.437 -         safeIs = safeIs,
   1.438 -         safeEs = rem_thm th safeEs,
   1.439 -         hazIs  = hazIs,
   1.440 -         hazEs  = hazEs,
   1.441 -         swrappers    = swrappers,
   1.442 -         uwrappers    = uwrappers,
   1.443 -         haz_netpair  = haz_netpair,
   1.444 -         dup_netpair  = dup_netpair,
   1.445 -         xtra_netpair = delete' ([], [th]) xtra_netpair}
   1.446 +      val th' = flat_rule th;
   1.447 +      val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
   1.448 +    in
   1.449 +      CS
   1.450 +       {safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   1.451 +        safep_netpair = delete (safep_rls, []) safep_netpair,
   1.452 +        safeIs = rem_thm th safeIs,
   1.453 +        safeEs = safeEs,
   1.454 +        hazIs = hazIs,
   1.455 +        hazEs = hazEs,
   1.456 +        swrappers = swrappers,
   1.457 +        uwrappers = uwrappers,
   1.458 +        haz_netpair = haz_netpair,
   1.459 +        dup_netpair = dup_netpair,
   1.460 +        xtra_netpair = delete' ([th], []) xtra_netpair}
   1.461      end
   1.462    else cs;
   1.463  
   1.464 +fun delSE th
   1.465 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.466 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.467 +  if mem_thm safeEs th then
   1.468 +    let
   1.469 +      val th' = classical_rule (flat_rule th);
   1.470 +      val (safe0_rls, safep_rls) = List.partition (fn rl => nprems_of rl = 1) [th'];
   1.471 +    in
   1.472 +      CS
   1.473 +       {safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   1.474 +        safep_netpair = delete ([], safep_rls) safep_netpair,
   1.475 +        safeIs = safeIs,
   1.476 +        safeEs = rem_thm th safeEs,
   1.477 +        hazIs = hazIs,
   1.478 +        hazEs = hazEs,
   1.479 +        swrappers = swrappers,
   1.480 +        uwrappers = uwrappers,
   1.481 +        haz_netpair = haz_netpair,
   1.482 +        dup_netpair = dup_netpair,
   1.483 +        xtra_netpair = delete' ([], [th]) xtra_netpair}
   1.484 +    end
   1.485 +  else cs;
   1.486  
   1.487  fun delI th
   1.488 -         (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.489 -                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.490 - if mem_thm hazIs th then
   1.491 -    let val th' = flat_rule th
   1.492 -    in CS{haz_netpair = delete ([th'], []) haz_netpair,
   1.493 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.494 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.495 +  if mem_thm hazIs th then
   1.496 +    let val th' = flat_rule th in
   1.497 +      CS
   1.498 +       {haz_netpair = delete ([th'], []) haz_netpair,
   1.499          dup_netpair = delete ([dup_intr th'], []) dup_netpair,
   1.500 -        safeIs  = safeIs,
   1.501 -        safeEs  = safeEs,
   1.502 -        hazIs   = rem_thm th hazIs,
   1.503 -        hazEs   = hazEs,
   1.504 -        swrappers     = swrappers,
   1.505 -        uwrappers     = uwrappers,
   1.506 +        safeIs = safeIs,
   1.507 +        safeEs = safeEs,
   1.508 +        hazIs = rem_thm th hazIs,
   1.509 +        hazEs = hazEs,
   1.510 +        swrappers = swrappers,
   1.511 +        uwrappers = uwrappers,
   1.512          safe0_netpair = safe0_netpair,
   1.513          safep_netpair = safep_netpair,
   1.514          xtra_netpair = delete' ([th], []) xtra_netpair}
   1.515      end
   1.516 - else cs
   1.517 - handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   1.518 -   error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   1.519 -
   1.520 +  else cs
   1.521 +  handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
   1.522 +    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   1.523  
   1.524  fun delE th
   1.525 -         (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.526 -                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.527 - if mem_thm hazEs th then
   1.528 -   let val th' = classical_rule (flat_rule th)
   1.529 -   in CS{haz_netpair = delete ([], [th']) haz_netpair,
   1.530 +    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.531 +      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.532 +  if mem_thm hazEs th then
   1.533 +    let val th' = classical_rule (flat_rule th) in
   1.534 +      CS
   1.535 +       {haz_netpair = delete ([], [th']) haz_netpair,
   1.536          dup_netpair = delete ([], [dup_elim th']) dup_netpair,
   1.537 -        safeIs  = safeIs,
   1.538 -        safeEs  = safeEs,
   1.539 -        hazIs   = hazIs,
   1.540 -        hazEs   = rem_thm th hazEs,
   1.541 -        swrappers     = swrappers,
   1.542 -        uwrappers     = uwrappers,
   1.543 +        safeIs = safeIs,
   1.544 +        safeEs = safeEs,
   1.545 +        hazIs = hazIs,
   1.546 +        hazEs = rem_thm th hazEs,
   1.547 +        swrappers = swrappers,
   1.548 +        uwrappers = uwrappers,
   1.549          safe0_netpair = safe0_netpair,
   1.550          safep_netpair = safep_netpair,
   1.551          xtra_netpair = delete' ([], [th]) xtra_netpair}
   1.552 -   end
   1.553 - else cs;
   1.554 +    end
   1.555 +  else cs;
   1.556  
   1.557  (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   1.558  fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   1.559 -  let val th' = Tactic.make_elim th in
   1.560 +  let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in
   1.561      if mem_thm safeIs th orelse mem_thm safeEs th orelse
   1.562        mem_thm hazIs th orelse mem_thm hazEs th orelse
   1.563        mem_thm safeEs th' orelse mem_thm hazEs th'
   1.564 @@ -561,6 +550,19 @@
   1.565  fun cs delrules ths = fold delrule ths cs;
   1.566  
   1.567  
   1.568 +fun make_elim th =
   1.569 +  if has_fewer_prems 1 th then
   1.570 +    error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
   1.571 +  else Tactic.make_elim th;
   1.572 +
   1.573 +fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   1.574 +fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   1.575 +fun cs addSDs ths = cs addSEs (map make_elim ths);
   1.576 +fun cs addIs ths = fold_rev (addI NONE) ths cs;
   1.577 +fun cs addEs ths = fold_rev (addE NONE) ths cs;
   1.578 +fun cs addDs ths = cs addEs (map make_elim ths);
   1.579 +
   1.580 +
   1.581  (*** Modifying the wrapper tacticals ***)
   1.582  fun map_swrappers f
   1.583    (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.584 @@ -579,12 +581,11 @@
   1.585      haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   1.586  
   1.587  fun update_warn msg (p as (key : string, _)) xs =
   1.588 -  (if AList.defined (op =) xs key then warning msg else ();
   1.589 -    AList.update (op =) p xs);
   1.590 +  (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
   1.591  
   1.592  fun delete_warn msg (key : string) xs =
   1.593    if AList.defined (op =) xs key then AList.delete (op =) key xs
   1.594 -    else (warning msg; xs);
   1.595 +  else (warning msg; xs);
   1.596  
   1.597  (*Add/replace a safe wrapper*)
   1.598  fun cs addSWrapper new_swrapper = map_swrappers
   1.599 @@ -603,25 +604,17 @@
   1.600    (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
   1.601  
   1.602  (* compose a safe tactic alternatively before/after safe_step_tac *)
   1.603 -fun cs addSbefore  (name,    tac1) =
   1.604 -    cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   1.605 -fun cs addSafter   (name,    tac2) =
   1.606 -    cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   1.607 +fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   1.608 +fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   1.609  
   1.610  (*compose a tactic alternatively before/after the step tactic *)
   1.611 -fun cs addbefore   (name,    tac1) =
   1.612 -    cs addWrapper  (name, fn tac2 => tac1 APPEND' tac2);
   1.613 -fun cs addafter    (name,    tac2) =
   1.614 -    cs addWrapper  (name, fn tac1 => tac1 APPEND' tac2);
   1.615 +fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
   1.616 +fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
   1.617  
   1.618 -fun cs addD2     (name, thm) =
   1.619 -    cs addafter  (name, datac thm 1);
   1.620 -fun cs addE2     (name, thm) =
   1.621 -    cs addafter  (name, eatac thm 1);
   1.622 -fun cs addSD2    (name, thm) =
   1.623 -    cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   1.624 -fun cs addSE2    (name, thm) =
   1.625 -    cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   1.626 +fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
   1.627 +fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
   1.628 +fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   1.629 +fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   1.630  
   1.631  (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   1.632    Merging the term nets may look more efficient, but the rather delicate
   1.633 @@ -636,21 +629,16 @@
   1.634        val safeEs' = fold rem_thm safeEs safeEs2;
   1.635        val hazIs' = fold rem_thm hazIs hazIs2;
   1.636        val hazEs' = fold rem_thm hazEs hazEs2;
   1.637 -      val cs1   = cs addSIs safeIs'
   1.638 -                     addSEs safeEs'
   1.639 -                     addIs  hazIs'
   1.640 -                     addEs  hazEs';
   1.641 -      val cs2 = map_swrappers
   1.642 -        (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
   1.643 -      val cs3 = map_uwrappers
   1.644 -        (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
   1.645 +      val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs';
   1.646 +      val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
   1.647 +      val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
   1.648      in cs3 end;
   1.649  
   1.650  
   1.651  (**** Simple tactics for theorem proving ****)
   1.652  
   1.653  (*Attack subgoals using safe inferences -- matching, not resolution*)
   1.654 -fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   1.655 +fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) =
   1.656    appSWrappers cs (FIRST' [
   1.657          eq_assume_tac,
   1.658          eq_mp_tac,
   1.659 @@ -659,8 +647,8 @@
   1.660          bimatch_from_nets_tac safep_netpair]);
   1.661  
   1.662  (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   1.663 -fun safe_steps_tac cs = REPEAT_DETERM1 o
   1.664 -        (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   1.665 +fun safe_steps_tac cs =
   1.666 +  REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   1.667  
   1.668  (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   1.669  fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   1.670 @@ -668,20 +656,20 @@
   1.671  
   1.672  (*** Clarify_tac: do safe steps without causing branching ***)
   1.673  
   1.674 -fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n);
   1.675 +fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n);
   1.676  
   1.677  (*version of bimatch_from_nets_tac that only applies rules that
   1.678    create precisely n subgoals.*)
   1.679  fun n_bimatch_from_nets_tac n =
   1.680 -    biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
   1.681 +  biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
   1.682  
   1.683  fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   1.684  val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   1.685  
   1.686  (*Two-way branching is allowed only if one of the branches immediately closes*)
   1.687  fun bimatch2_tac netpair i =
   1.688 -    n_bimatch_from_nets_tac 2 netpair i THEN
   1.689 -    (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1));
   1.690 +  n_bimatch_from_nets_tac 2 netpair i THEN
   1.691 +  (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
   1.692  
   1.693  (*Attack subgoals using safe inferences -- matching, not resolution*)
   1.694  fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   1.695 @@ -715,13 +703,13 @@
   1.696    biresolve_from_nets_tac haz_netpair;
   1.697  
   1.698  (*Single step for the prover.  FAILS unless it makes progress. *)
   1.699 -fun step_tac cs i = safe_tac cs ORELSE appWrappers cs
   1.700 -        (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   1.701 +fun step_tac cs i =
   1.702 +  safe_tac cs ORELSE appWrappers cs (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   1.703  
   1.704  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   1.705    allows backtracking from "safe" rules to "unsafe" rules here.*)
   1.706 -fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs
   1.707 -        (inst_step_tac cs APPEND' haz_step_tac cs) i;
   1.708 +fun slow_step_tac cs i =
   1.709 +  safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i;
   1.710  
   1.711  (**** The following tactics all fail unless they solve one goal ****)
   1.712  
   1.713 @@ -749,20 +737,21 @@
   1.714  
   1.715  
   1.716  (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   1.717 -val weight_ASTAR = Unsynchronized.ref 5;
   1.718 +val weight_ASTAR = Unsynchronized.ref 5;  (* FIXME argument / config option !? *)
   1.719  
   1.720  fun astar_tac cs =
   1.721    Object_Logic.atomize_prems_tac THEN'
   1.722    SELECT_GOAL
   1.723 -    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   1.724 +    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev)
   1.725        (step_tac cs 1));
   1.726  
   1.727  fun slow_astar_tac cs =
   1.728    Object_Logic.atomize_prems_tac THEN'
   1.729    SELECT_GOAL
   1.730 -    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   1.731 +    (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev)
   1.732        (slow_step_tac cs 1));
   1.733  
   1.734 +
   1.735  (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   1.736    of much experimentation!  Changing APPEND to ORELSE below would prove
   1.737    easy theorems faster, but loses completeness -- and many of the harder
   1.738 @@ -776,29 +765,26 @@
   1.739  
   1.740  (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   1.741  local
   1.742 -fun slow_step_tac' cs = appWrappers cs
   1.743 -        (instp_step_tac cs APPEND' dup_step_tac cs);
   1.744 -in fun depth_tac cs m i state = SELECT_GOAL
   1.745 -   (safe_steps_tac cs 1 THEN_ELSE
   1.746 -        (DEPTH_SOLVE (depth_tac cs m 1),
   1.747 -         inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   1.748 -                (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   1.749 -        )) i state;
   1.750 +  fun slow_step_tac' cs = appWrappers cs (instp_step_tac cs APPEND' dup_step_tac cs);
   1.751 +in
   1.752 +  fun depth_tac cs m i state = SELECT_GOAL
   1.753 +    (safe_steps_tac cs 1 THEN_ELSE
   1.754 +      (DEPTH_SOLVE (depth_tac cs m 1),
   1.755 +        inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
   1.756 +          (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m - 1) 1)))) i state;
   1.757  end;
   1.758  
   1.759  (*Search, with depth bound m.
   1.760    This is the "entry point", which does safe inferences first.*)
   1.761 -fun safe_depth_tac cs m =
   1.762 -  SUBGOAL
   1.763 -    (fn (prem,i) =>
   1.764 -      let val deti =
   1.765 -          (*No Vars in the goal?  No need to backtrack between goals.*)
   1.766 -          if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
   1.767 -      in  SELECT_GOAL (TRY (safe_tac cs) THEN
   1.768 -                       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   1.769 -      end);
   1.770 +fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) =>
   1.771 +  let val deti =
   1.772 +      (*No Vars in the goal?  No need to backtrack between goals.*)
   1.773 +    if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
   1.774 +  in
   1.775 +    SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   1.776 +  end);
   1.777  
   1.778 -fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   1.779 +fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs);
   1.780  
   1.781  
   1.782