# HG changeset patch
# User wenzelm
# Date 967503382 -7200
# Node ID 5705a04d24eaa8162c9b26d2f325d11b6f620540
# Parent  79db0e5b782430790234961a34f7e566fd2c351a
proper cong setup;

diff -r 79db0e5b7824 -r 5705a04d24ea src/Provers/simplifier.ML
--- 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 *)