--- a/src/Provers/simplifier.ML Tue Aug 29 00:55:59 2000 +0200
+++ b/src/Provers/simplifier.ML Tue Aug 29 00:56:22 2000 +0200
@@ -8,8 +8,8 @@
infix 4
setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
- addSolver addsimps delsimps addeqcongs deleqcongs
- setmksimps setmkeqTrue setmksym settermless addsimprocs delsimprocs;
+ addSolver addsimps delsimps addeqcongs deleqcongs addcongs delcongs
+ setmksimps setmkeqTrue setmkcong setmksym settermless addsimprocs delsimprocs;
signature BASIC_SIMPLIFIER =
sig
@@ -22,10 +22,11 @@
val empty_ss: simpset
val rep_ss: simpset ->
{mss: meta_simpset,
- subgoal_tac: simpset -> int -> tactic,
- loop_tacs: (string * (int -> tactic))list,
+ mk_cong: thm -> thm,
+ subgoal_tac: simpset -> int -> tactic,
+ loop_tacs: (string * (int -> tactic)) list,
unsafe_solvers: solver list,
- solvers: solver list};
+ solvers: solver list};
val print_ss: simpset -> unit
val print_simpset: theory -> unit
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
@@ -38,12 +39,15 @@
val addSolver: simpset * solver -> simpset
val setmksimps: simpset * (thm -> thm list) -> simpset
val setmkeqTrue: simpset * (thm -> thm option) -> simpset
+ val setmkcong: simpset * (thm -> thm) -> simpset
val setmksym: simpset * (thm -> thm option) -> simpset
val settermless: simpset * (term * term -> bool) -> simpset
val addsimps: simpset * thm list -> simpset
val delsimps: simpset * thm list -> simpset
val addeqcongs: simpset * thm list -> simpset
val deleqcongs: simpset * thm list -> simpset
+ val addcongs: simpset * thm list -> simpset
+ val delcongs: simpset * thm list -> simpset
val addsimprocs: simpset * simproc list -> simpset
val delsimprocs: simpset * simproc list -> simpset
val merge_ss: simpset * simpset -> simpset
@@ -60,6 +64,8 @@
val Delsimps: thm list -> unit
val Addsimprocs: simproc list -> unit
val Delsimprocs: simproc list -> unit
+ val Addcongs: thm list -> unit
+ val Delcongs: thm list -> unit
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
val simp_tac: simpset -> int -> tactic
val asm_simp_tac: simpset -> int -> tactic
@@ -93,6 +99,10 @@
val simp_del_global: theory attribute
val simp_add_local: Proof.context attribute
val simp_del_local: Proof.context attribute
+ val cong_add_global: theory attribute
+ val cong_del_global: theory attribute
+ val cong_add_local: Proof.context attribute
+ val cong_del_local: Proof.context attribute
val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val setup: (theory -> theory) list
@@ -142,18 +152,19 @@
datatype simpset =
Simpset of {
mss: meta_simpset,
- subgoal_tac: simpset -> int -> tactic,
- loop_tacs: (string * (int -> tactic))list,
+ mk_cong: thm -> thm,
+ subgoal_tac: simpset -> int -> tactic,
+ loop_tacs: (string * (int -> tactic)) list,
unsafe_solvers: solver list,
- solvers: solver list};
+ solvers: solver list};
-fun make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =
- Simpset {mss = mss, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
- unsafe_solvers = unsafe_solvers, solvers = solvers};
+fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
+ Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
+ loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
val empty_ss =
let val mss = Thm.set_mk_sym (Thm.empty_mss, Some o symmetric_fun)
- in make_ss (mss, K (K no_tac), [], [], []) end;
+ in make_ss mss I (K (K no_tac)) [] [] [] end;
fun rep_ss (Simpset args) = args;
fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss;
@@ -179,98 +190,99 @@
(* extend simpsets *)
-fun (Simpset {mss, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
setsubgoaler subgoal_tac =
- make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+ make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
setloop tac =
- make_ss (mss, subgoal_tac, [("", tac)], unsafe_solvers, solvers);
+ make_ss mss mk_cong subgoal_tac [("", tac)] unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
- addloop tac = make_ss (mss, subgoal_tac,
- (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
- warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac)),
- unsafe_solvers, solvers);
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+ addloop tac = make_ss mss mk_cong subgoal_tac
+ (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
+ warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac))
+ unsafe_solvers solvers;
-fun (ss as Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (ss as Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
delloop name =
let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
if null del then (warning ("No such looper in simpset: " ^ name); ss)
- else make_ss (mss, subgoal_tac, rest, unsafe_solvers, solvers)
+ else make_ss mss mk_cong subgoal_tac rest unsafe_solvers solvers
end;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...})
setSSolver solver =
- make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers, [solver]);
+ make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers [solver];
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
addSSolver sol =
- make_ss (mss, subgoal_tac, loop_tacs, unsafe_solvers,
- merge_solvers solvers [sol]);
+ make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers (merge_solvers solvers [sol]);
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
setSolver unsafe_solver =
- make_ss (mss, subgoal_tac, loop_tacs, [unsafe_solver], solvers);
+ make_ss mss mk_cong subgoal_tac loop_tacs [unsafe_solver] solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
addSolver sol =
- make_ss (mss, subgoal_tac, loop_tacs,
- merge_solvers unsafe_solvers [sol], solvers);
+ make_ss mss mk_cong subgoal_tac loop_tacs (merge_solvers unsafe_solvers [sol]) solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
setmksimps mk_simps =
- make_ss (Thm.set_mk_rews (mss, mk_simps), subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+ make_ss (Thm.set_mk_rews (mss, mk_simps)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
setmkeqTrue mk_eq_True =
- make_ss (Thm.set_mk_eq_True (mss, mk_eq_True),
- subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+ make_ss (Thm.set_mk_eq_True (mss, mk_eq_True)) mk_cong subgoal_tac loop_tacs
+ unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong = _, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+ setmkcong mk_cong =
+ make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
setmksym mksym =
- make_ss (Thm.set_mk_sym (mss, mksym),
- subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+ make_ss (Thm.set_mk_sym (mss, mksym)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
settermless termless =
- make_ss (Thm.set_termless (mss, termless), subgoal_tac, loop_tacs,
- unsafe_solvers, solvers);
+ make_ss (Thm.set_termless (mss, termless)) mk_cong subgoal_tac loop_tacs
+ unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
addsimps rews =
- make_ss (Thm.add_simps (mss, rews), subgoal_tac, loop_tacs,
- unsafe_solvers, solvers);
+ make_ss (Thm.add_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
delsimps rews =
- make_ss (Thm.del_simps (mss, rews), subgoal_tac, loop_tacs,
- unsafe_solvers, solvers);
+ make_ss (Thm.del_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
addeqcongs newcongs =
- make_ss (Thm.add_congs (mss, newcongs), subgoal_tac, loop_tacs,
- unsafe_solvers, solvers);
+ make_ss (Thm.add_congs (mss, newcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
+
+fun (Simpset {mss, subgoal_tac, mk_cong, loop_tacs, unsafe_solvers, solvers})
+ deleqcongs oldcongs =
+ make_ss (Thm.del_congs (mss, oldcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
- deleqcongs oldcongs =
- make_ss (Thm.del_congs (mss, oldcongs), subgoal_tac, loop_tacs,
- unsafe_solvers, solvers);
+fun (ss as Simpset {mk_cong, ...}) addcongs newcongs =
+ ss addeqcongs map mk_cong newcongs;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (ss as Simpset {mk_cong, ...}) delcongs oldcongs =
+ ss deleqcongs map mk_cong oldcongs;
+
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
addsimprocs simprocs =
- make_ss
- (Thm.add_simprocs (mss, map rep_simproc simprocs),
- subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+ make_ss (Thm.add_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac loop_tacs
+ unsafe_solvers solvers;
-fun (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
+fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
delsimprocs simprocs =
- make_ss
- (Thm.del_simprocs (mss, map rep_simproc simprocs),
- subgoal_tac, loop_tacs, unsafe_solvers, solvers);
+ make_ss (Thm.del_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac
+ loop_tacs unsafe_solvers solvers;
-fun clear_ss (Simpset {mss, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
- make_ss (Thm.clear_mss mss, subgoal_tac, [], unsafe_solvers, solvers);
+fun clear_ss (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
+ make_ss (Thm.clear_mss mss) mk_cong subgoal_tac [] unsafe_solvers solvers;
(* merge simpsets *)
@@ -278,14 +290,14 @@
(*ignores subgoal_tac of 2nd simpset!*)
fun merge_ss
- (Simpset {mss = mss1, loop_tacs = loop_tacs1, subgoal_tac,
+ (Simpset {mss = mss1, mk_cong, loop_tacs = loop_tacs1, subgoal_tac,
unsafe_solvers = unsafe_solvers1, solvers = solvers1},
- Simpset {mss = mss2, loop_tacs = loop_tacs2,
- unsafe_solvers = unsafe_solvers2, solvers = solvers2, ...}) =
- make_ss (Thm.merge_mss (mss1, mss2), subgoal_tac,
- merge_alists loop_tacs1 loop_tacs2,
- merge_solvers unsafe_solvers1 unsafe_solvers2,
- merge_solvers solvers1 solvers2);
+ Simpset {mss = mss2, mk_cong = _, loop_tacs = loop_tacs2, subgoal_tac = _,
+ unsafe_solvers = unsafe_solvers2, solvers = solvers2}) =
+ make_ss (Thm.merge_mss (mss1, mss2)) mk_cong subgoal_tac
+ (merge_alists loop_tacs1 loop_tacs2)
+ (merge_solvers unsafe_solvers1 unsafe_solvers2)
+ (merge_solvers solvers1 solvers2);
@@ -335,6 +347,8 @@
val Delsimps = change_simpset (op delsimps);
val Addsimprocs = change_simpset (op addsimprocs);
val Delsimprocs = change_simpset (op delsimprocs);
+val Addcongs = change_simpset (op addcongs);
+val Delcongs = change_simpset (op delcongs);
(* proof data kind 'Provers/simpset' *)
@@ -369,14 +383,19 @@
val simp_add_local = change_local_ss (op addsimps);
val simp_del_local = change_local_ss (op delsimps);
+val cong_add_global = change_global_ss (op addcongs);
+val cong_del_global = change_global_ss (op delcongs);
+val cong_add_local = change_local_ss (op addcongs);
+val cong_del_local = change_local_ss (op delcongs);
+
(** simplification tactics **)
-fun solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers) mss =
+fun solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers) mss =
let
val ss =
- make_ss (mss, subgoal_tac, loop_tacs,unsafe_solvers,unsafe_solvers);
+ make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers unsafe_solvers;
val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
in DEPTH_SOLVE solve1_tac end;
@@ -384,12 +403,12 @@
(*note: may instantiate unknowns that appear also in other subgoals*)
fun generic_simp_tac safe mode =
- fn (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
+ fn (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
let
val solvs = app_sols (if safe then solvers else unsafe_solvers);
fun simp_loop_tac i =
asm_rewrite_goal_tac mode
- (solve_all_tac (subgoal_tac,loop_tacs,unsafe_solvers))
+ (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
mss i
THEN (solvs (prems_of_mss mss) i ORELSE
TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
@@ -413,10 +432,10 @@
(** simplification rules and conversions **)
-fun simp rew mode
- (Simpset {mss, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
+fun simp rew mode
+ (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
let
- val tacf = solve_all_tac (subgoal_tac, loop_tacs, unsafe_solvers);
+ val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
fun prover m th = apsome fst (Seq.pull (tacf m th));
in rew mode prover mss thm end;
@@ -440,6 +459,7 @@
(* add / del *)
val simpN = "simp";
+val congN = "cong";
val addN = "add";
val delN = "del";
val onlyN = "only";
@@ -449,6 +469,10 @@
(Attrib.add_del_args simp_add_global simp_del_global,
Attrib.add_del_args simp_add_local simp_del_local);
+val cong_attr =
+ (Attrib.add_del_args cong_add_global cong_del_global,
+ Attrib.add_del_args cong_add_local cong_del_local);
+
(* conversions *)
@@ -461,6 +485,7 @@
val setup_attrs = Attrib.add_attributes
[(simpN, simp_attr, "declare simplification rule"),
+ (congN, cong_attr, "declare Simplifier congruence rule"),
("simplify", conv_attr simplify, "simplify rule"),
("asm_simplify", conv_attr asm_simplify, "simplify rule, using assumptions"),
("full_simplify", conv_attr full_simplify, "fully simplify rule"),
@@ -478,18 +503,23 @@
Args.parens (Args.$$$ "no_asm_use") >> K full_simp_tac ||
Scan.succeed asm_full_simp_tac);
+val cong_modifiers =
+ [Args.$$$ congN -- Args.colon >> K (I, cong_add_local),
+ Args.$$$ congN -- Args.$$$ addN -- Args.colon >> K (I, cong_add_local),
+ Args.$$$ congN -- Args.$$$ delN -- Args.colon >> K (I, cong_del_local)];
+
val simp_modifiers =
[Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
Args.$$$ simpN -- Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
Args.$$$ simpN -- Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local),
- Args.$$$ otherN -- Args.colon >> K (I, I)];
+ Args.$$$ otherN -- Args.colon >> K (I, I)] @ cong_modifiers;
val simp_modifiers' =
[Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local),
- Args.$$$ otherN -- Args.colon >> K (I, I)];
+ Args.$$$ otherN -- Args.colon >> K (I, I)] @ cong_modifiers;
fun simp_args more_mods =
Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');
@@ -501,7 +531,7 @@
fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN' (CHANGED oo tac) (get_local_simpset ctxt)));
-
+
(* setup_methods *)