Solvers are now named and stamped.
authornipkow
Tue Sep 21 19:05:38 1999 +0200 (1999-09-21)
changeset 7568436c87ac2fac
parent 7567 62384a807775
child 7569 1d9263172b54
Solvers are now named and stamped.
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/simplifier.ML	Tue Sep 21 18:11:08 1999 +0200
     1.2 +++ b/src/Provers/simplifier.ML	Tue Sep 21 19:05:38 1999 +0200
     1.3 @@ -16,24 +16,26 @@
     1.4    type simproc
     1.5    val mk_simproc: string -> cterm list
     1.6      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
     1.7 +  type solver
     1.8 +  val mk_solver: string -> (thm list -> int -> tactic) -> solver
     1.9    type simpset
    1.10    val empty_ss: simpset
    1.11    val rep_ss: simpset ->
    1.12     {mss: meta_simpset,
    1.13      subgoal_tac:        simpset -> int -> tactic,
    1.14      loop_tacs:          (string * (int -> tactic))list,
    1.15 -    unsafe_finish_tac: thm list -> int -> tactic,
    1.16 -           finish_tac: thm list -> int -> tactic};
    1.17 +    unsafe_solvers: solver list,
    1.18 +           solvers: solver list};
    1.19    val print_ss: simpset -> unit
    1.20    val print_simpset: theory -> unit
    1.21    val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    1.22    val setloop:      simpset *             (int -> tactic) -> simpset
    1.23    val addloop:      simpset *  (string * (int -> tactic)) -> simpset
    1.24    val delloop:      simpset *   string                    -> simpset
    1.25 -  val setSSolver:   simpset * (thm list -> int -> tactic) -> simpset
    1.26 -  val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
    1.27 -  val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
    1.28 -  val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
    1.29 +  val setSSolver:   simpset * solver -> simpset
    1.30 +  val addSSolver:   simpset * solver -> simpset
    1.31 +  val setSolver:    simpset * solver -> simpset
    1.32 +  val addSolver:    simpset * solver -> simpset
    1.33    val setmksimps:   simpset * (thm -> thm list) -> simpset
    1.34    val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
    1.35    val setmksym:     simpset * (thm -> thm option) -> simpset
    1.36 @@ -110,7 +112,19 @@
    1.37  
    1.38  fun rep_simproc (Simproc args) = args;
    1.39  
    1.40 +(** solvers **)
    1.41  
    1.42 +datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
    1.43 +
    1.44 +fun mk_solver name solver = Solver(name, solver, stamp());
    1.45 +
    1.46 +fun eq_solver (Solver(_,_,s1),Solver(_,_,s2)) = s1=s2;
    1.47 +
    1.48 +val merge_solvers = generic_merge eq_solver I I;
    1.49 +
    1.50 +fun app_sols [] _ _ = no_tac
    1.51 +  | app_sols (Solver(_,solver,_)::sols) thms i =
    1.52 +       solver thms i ORELSE app_sols sols thms i;
    1.53  
    1.54  (** simplification sets **)
    1.55  
    1.56 @@ -121,16 +135,16 @@
    1.57      mss: meta_simpset,
    1.58      subgoal_tac:        simpset -> int -> tactic,
    1.59      loop_tacs:          (string * (int -> tactic))list,
    1.60 -    unsafe_finish_tac: thm list -> int -> tactic,
    1.61 -           finish_tac: thm list -> int -> tactic};
    1.62 +    unsafe_solvers: solver list,
    1.63 +           solvers: solver list};
    1.64  
    1.65 -fun make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac) =
    1.66 +fun make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =
    1.67    Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
    1.68 -    unsafe_finish_tac = unsafe_finish_tac, finish_tac = finish_tac};
    1.69 +    unsafe_solvers = unsafe_solvers, solvers = solvers};
    1.70  
    1.71  val empty_ss =
    1.72    let val mss = Thm.set_mk_sym (Thm.empty_mss, Some o symmetric_fun)
    1.73 -  in make_ss (mss, K (K no_tac), [], K (K no_tac), K (K no_tac)) end;
    1.74 +  in make_ss (mss, K (K no_tac), [], [], []) end;
    1.75  
    1.76  fun rep_ss (Simpset args) = args;
    1.77  fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
    1.78 @@ -155,108 +169,113 @@
    1.79  
    1.80  (* extend simpsets *)
    1.81  
    1.82 -fun (Simpset {mss, subgoal_tac = _, loop_tacs, unsafe_finish_tac, finish_tac})
    1.83 +fun (Simpset {mss, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
    1.84      setsubgoaler subgoal_tac =
    1.85 -  make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
    1.86 +  make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers);
    1.87  
    1.88 -fun (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_finish_tac, finish_tac})
    1.89 +fun (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
    1.90      setloop tac =
    1.91 -  make_ss (mss, subgoal_tac, [("",tac)], unsafe_finish_tac, finish_tac);
    1.92 +  make_ss (mss, subgoal_tac, [("",tac)], unsafe_solvers, solvers);
    1.93  
    1.94 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
    1.95 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
    1.96      addloop tac = make_ss (mss, subgoal_tac, 
    1.97          (case assoc_string (loop_tacs,(fst tac)) of None => () | Some x => 
    1.98           warning ("overwriting looper "^fst tac); overwrite(loop_tacs,tac)),
    1.99 -           unsafe_finish_tac, finish_tac);
   1.100 +           unsafe_solvers, solvers);
   1.101  
   1.102 -fun (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.103 +fun (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.104   delloop name =
   1.105    let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
   1.106      if null del then (warning ("No such looper in simpset: " ^ name); ss)
   1.107 -    else make_ss (mss, subgoal_tac, rest, unsafe_finish_tac, finish_tac)
   1.108 +    else make_ss (mss, subgoal_tac, rest, unsafe_solvers, solvers)
   1.109    end;
   1.110 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...})
   1.111 -    setSSolver finish_tac =
   1.112 -  make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.113  
   1.114 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.115 -    addSSolver tac =
   1.116 -  make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac,
   1.117 -	fn hyps => finish_tac hyps ORELSE' tac hyps);
   1.118 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...})
   1.119 +    setSSolver solver =
   1.120 +  make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, [solver]);
   1.121  
   1.122 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac = _, finish_tac})
   1.123 -    setSolver unsafe_finish_tac =
   1.124 -  make_ss (mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.125 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.126 +    addSSolver sol =
   1.127 +  make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers,
   1.128 +           merge_solvers solvers [sol]);
   1.129  
   1.130 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.131 -    addSolver tac =
   1.132 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
   1.133 +    setSolver unsafe_solver =
   1.134 +  make_ss (mss, subgoal_tac, loop_tacs, [unsafe_solver], solvers);
   1.135 +
   1.136 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.137 +    addSolver sol =
   1.138    make_ss (mss, subgoal_tac, loop_tacs, 
   1.139 -    fn hyps => unsafe_finish_tac hyps ORELSE' tac hyps, finish_tac);
   1.140 +    merge_solvers unsafe_solvers [sol], solvers);
   1.141  
   1.142 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.143 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.144      setmksimps mk_simps =
   1.145    make_ss (Thm.set_mk_rews (mss, map (Thm.strip_shyps o Drule.zero_var_indexes) o mk_simps),
   1.146 -    subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.147 +    subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   1.148  
   1.149 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.150 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.151      setmkeqTrue mk_eq_True =
   1.152    make_ss (Thm.set_mk_eq_True (mss, mk_eq_True),
   1.153 -    subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.154 +    subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   1.155  
   1.156 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.157 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.158      setmksym mksym =
   1.159    make_ss (Thm.set_mk_sym (mss, mksym),
   1.160 -    subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.161 +    subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   1.162  
   1.163 -fun (Simpset {mss, subgoal_tac, loop_tacs,  unsafe_finish_tac, finish_tac})
   1.164 +fun (Simpset {mss, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
   1.165      settermless termless =
   1.166    make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,
   1.167 -    unsafe_finish_tac, finish_tac);
   1.168 +    unsafe_solvers, solvers);
   1.169  
   1.170 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.171 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.172      addsimps rews =
   1.173    make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs, 
   1.174 -	   unsafe_finish_tac, finish_tac);
   1.175 +	   unsafe_solvers, solvers);
   1.176  
   1.177 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.178 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.179      delsimps rews =
   1.180    make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs, 
   1.181 -	   unsafe_finish_tac, finish_tac);
   1.182 +	   unsafe_solvers, solvers);
   1.183  
   1.184 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.185 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.186      addeqcongs newcongs =
   1.187    make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs, 
   1.188 -	   unsafe_finish_tac, finish_tac);
   1.189 +	   unsafe_solvers, solvers);
   1.190  
   1.191 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.192 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.193      deleqcongs oldcongs =
   1.194    make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs, 
   1.195 -	   unsafe_finish_tac, finish_tac);
   1.196 +	   unsafe_solvers, solvers);
   1.197  
   1.198 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.199 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.200      addsimprocs simprocs =
   1.201    make_ss
   1.202      (Thm.add_simprocs (mss, map rep_simproc simprocs),
   1.203 -      subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.204 +      subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   1.205  
   1.206 -fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac})
   1.207 +fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.208      delsimprocs simprocs =
   1.209    make_ss
   1.210      (Thm.del_simprocs (mss, map rep_simproc simprocs),
   1.211 -      subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.212 +      subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   1.213  
   1.214 -fun clear_ss (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac}) =
   1.215 -  make_ss (Thm.clear_mss mss, subgoal_tac, loop_tacs, unsafe_finish_tac, finish_tac);
   1.216 +fun clear_ss (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers}) =
   1.217 +  make_ss (Thm.clear_mss mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers);
   1.218  
   1.219  
   1.220 -(* merge simpsets *)    (*NOTE: ignores tactics of 2nd simpset (except loopers)*)
   1.221 +(* merge simpsets *)
   1.222 +(*NOTE: ignores subgoal_tac of 2nd simpset *)
   1.223  
   1.224  fun merge_ss
   1.225 -   (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac, unsafe_finish_tac, finish_tac},
   1.226 -    Simpset {mss = mss2, loop_tacs = loop_tacs2, ...}) =
   1.227 +   (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac,
   1.228 +             unsafe_solvers = unsafe_solvers1, solvers = solvers1},
   1.229 +    Simpset {mss = mss2, loop_tacs = loop_tacs2,
   1.230 +             unsafe_solvers = unsafe_solvers2, solvers = solvers2, ...}) =
   1.231    make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac,
   1.232 -    merge_alists loop_tacs1 loop_tacs2, unsafe_finish_tac, finish_tac);
   1.233 -
   1.234 +    merge_alists loop_tacs1 loop_tacs2,
   1.235 +    merge_solvers unsafe_solvers1 unsafe_solvers2,
   1.236 +    merge_solvers solvers1 solvers2);
   1.237  
   1.238  
   1.239  (** global and local simpset data **)
   1.240 @@ -343,30 +362,30 @@
   1.241  
   1.242  (** simplification tactics **)
   1.243  
   1.244 -fun solve_all_tac (subgoal_tac, loop_tacs, unsafe_finish_tac) mss =
   1.245 +fun solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers) mss =
   1.246    let
   1.247      val ss =
   1.248 -      make_ss (mss, subgoal_tac, loop_tacs,unsafe_finish_tac,unsafe_finish_tac);
   1.249 +      make_ss (mss, subgoal_tac, loop_tacs,unsafe_solvers,unsafe_solvers);
   1.250      val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   1.251    in DEPTH_SOLVE solve1_tac end;
   1.252  
   1.253  fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
   1.254  
   1.255  (*unsafe: may instantiate unknowns that appear also in other subgoals*)
   1.256 -fun basic_gen_simp_tac mode finish_tac =
   1.257 -  fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...}) =>
   1.258 +fun basic_gen_simp_tac mode solvers =
   1.259 +  fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) =>
   1.260      let
   1.261        fun simp_loop_tac i =
   1.262          asm_rewrite_goal_tac mode
   1.263 -          (solve_all_tac (subgoal_tac,loop_tacs,unsafe_finish_tac))
   1.264 +          (solve_all_tac (subgoal_tac,loop_tacs,unsafe_solvers))
   1.265            mss i
   1.266 -        THEN (finish_tac (prems_of_mss mss) i ORELSE
   1.267 +        THEN (solvers (prems_of_mss mss) i ORELSE
   1.268                TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   1.269      in simp_loop_tac end;
   1.270  
   1.271  fun gen_simp_tac mode 
   1.272 -      (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...}) =
   1.273 -  basic_gen_simp_tac mode unsafe_finish_tac ss;
   1.274 +      (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) =
   1.275 +  basic_gen_simp_tac mode (app_sols unsafe_solvers) ss;
   1.276  
   1.277  val          simp_tac = gen_simp_tac (false, false, false);
   1.278  val      asm_simp_tac = gen_simp_tac (false, true, false);
   1.279 @@ -376,8 +395,8 @@
   1.280  
   1.281  (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   1.282  fun safe_asm_full_simp_tac (ss as Simpset {mss, subgoal_tac, loop_tacs, 
   1.283 -	unsafe_finish_tac, finish_tac}) = 
   1.284 -  basic_gen_simp_tac (true, true, true) finish_tac ss;
   1.285 +	unsafe_solvers, solvers}) = 
   1.286 +  basic_gen_simp_tac (true, true, true) (app_sols solvers) ss;
   1.287  
   1.288  (*the abstraction over the proof state delays the dereferencing*)
   1.289  fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   1.290 @@ -391,9 +410,9 @@
   1.291  (** simplification rules and conversions **)
   1.292  
   1.293  fun simp rew mode 
   1.294 -     (Simpset {mss, subgoal_tac, loop_tacs, unsafe_finish_tac, ...}) thm =
   1.295 +     (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   1.296    let
   1.297 -    val tacf = solve_all_tac (subgoal_tac, loop_tacs, unsafe_finish_tac);
   1.298 +    val tacf = solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers);
   1.299      fun prover m th = apsome fst (Seq.pull (tacf m th));
   1.300    in rew mode prover mss thm end;
   1.301  
   1.302 @@ -417,6 +436,7 @@
   1.303  (* add / del *)
   1.304  
   1.305  val simpN = "simp";
   1.306 +val asm_simpN = "asm_simp";
   1.307  val addN = "add";
   1.308  val delN = "del";
   1.309  val onlyN = "only";
   1.310 @@ -467,21 +487,32 @@
   1.311    Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
   1.312    Args.$$$ otherN >> K (I, I)];
   1.313  
   1.314 +val simp_args = Method.only_sectioned_args simp_modifiers';
   1.315 +
   1.316 +fun simp_meth thin cut tac ctxt = Method.METHOD (fn facts =>
   1.317 +  FIRSTGOAL
   1.318 +    ((if thin then REPEAT_DETERM o etac Drule.thin_rl else K all_tac)
   1.319 +      THEN' (if cut then Method.insert_tac facts else K all_tac)
   1.320 +      THEN' tac (get_local_simpset ctxt)));
   1.321 +
   1.322  fun simp_method tac =
   1.323    (fn prems => fn ctxt => Method.METHOD (fn facts =>
   1.324      FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_simpset ctxt))))
   1.325    |> Method.bang_sectioned_args simp_modifiers';
   1.326 -
   1.327 +  
   1.328  
   1.329  (* setup_methods *)
   1.330  
   1.331  val setup_methods = Method.add_methods
   1.332 - [(simpN,               simp_method (CHANGED oo asm_full_simp_tac), "full simplification"),
   1.333 -  ("simp_tac",          simp_method simp_tac, "simp_tac (improper!)"),
   1.334 -  ("asm_simp_tac",      simp_method asm_simp_tac, "asm_simp_tac (improper!)"),
   1.335 -  ("full_simp_tac",     simp_method full_simp_tac, "full_simp_tac (improper!)"),
   1.336 -  ("asm_full_simp_tac", simp_method asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
   1.337 -  ("asm_lr_simp_tac",   simp_method asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
   1.338 + [(simpN,               simp_method true true (CHANGED oo asm_full_simp_tac),
   1.339 +    "full simplification (including facts, excluding assumptions)"),
   1.340 +  (asm_simpN,           simp_method false true (CHANGED oo asm_full_simp_tac),
   1.341 +    "full simplification (including facts and assumptions)"),
   1.342 +  ("simp_tac",          simp_method false false simp_tac, "simp_tac (improper!)"),
   1.343 +  ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"),
   1.344 +  ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac (improper!)"),
   1.345 +  ("asm_full_simp_tac", simp_method false false asm_full_simp_tac, "asm_full_simp_tac (improper!)"),
   1.346 +  ("asm_lr_simp_tac",   simp_method false false asm_lr_simp_tac, "asm_lr_simp_tac (improper!)")];
   1.347  
   1.348  
   1.349