added simplification meta rules;
authorwenzelm
Wed Jul 23 11:03:54 1997 +0200 (1997-07-23)
changeset 35579546f8185c43
parent 3556 229a40c2b19e
child 3558 258eee1a056e
added simplification meta rules;
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/simplifier.ML	Wed Jul 23 10:34:18 1997 +0200
     1.2 +++ b/src/Provers/simplifier.ML	Wed Jul 23 11:03:54 1997 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      Provers/simplifier.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1993  TU Munich
     1.8 +    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     1.9  
    1.10  Generic simplifier, suitable for most logics.
    1.11  *)
    1.12 @@ -17,7 +16,7 @@
    1.13    type simproc
    1.14    val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc
    1.15    val conv_prover: (term * term -> term) -> thm -> (thm -> thm)
    1.16 -    -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm	(* FIXME move?, rename? *)
    1.17 +    -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm
    1.18    type simpset
    1.19    val empty_ss: simpset
    1.20    val rep_ss: simpset ->
    1.21 @@ -58,6 +57,10 @@
    1.22    val           Asm_simp_tac:            int -> tactic
    1.23    val          Full_simp_tac:            int -> tactic
    1.24    val      Asm_full_simp_tac:            int -> tactic
    1.25 +  val          simplify: simpset -> thm -> thm
    1.26 +  val      asm_simplify: simpset -> thm -> thm
    1.27 +  val     full_simplify: simpset -> thm -> thm
    1.28 +  val asm_full_simplify: simpset -> thm -> thm
    1.29  end;
    1.30  
    1.31  
    1.32 @@ -72,7 +75,9 @@
    1.33  datatype simproc =
    1.34    Simproc of string * cterm list * (Sign.sg -> term -> thm option) * stamp;
    1.35  
    1.36 -fun mk_simproc name lhss proc = Simproc (name, lhss, proc, stamp ());
    1.37 +fun mk_simproc name lhss proc =
    1.38 +  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
    1.39 +
    1.40  fun rep_simproc (Simproc args) = args;
    1.41  
    1.42  
    1.43 @@ -224,7 +229,8 @@
    1.44      subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
    1.45  
    1.46  
    1.47 -(* the current simpset *)
    1.48 +
    1.49 +(** the current simpset **)
    1.50  
    1.51  val simpset = ref empty_ss;
    1.52  
    1.53 @@ -235,26 +241,29 @@
    1.54  fun Delsimprocs procs = (simpset := ! simpset delsimprocs procs);
    1.55  
    1.56  
    1.57 +
    1.58  (** simplification tactics **)
    1.59  
    1.60  fun NEWSUBGOALS tac tacf st0 =
    1.61    st0 |> (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1));
    1.62  
    1.63 +fun solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac) mss =
    1.64 +  let
    1.65 +    val ss =
    1.66 +      make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
    1.67 +    val solve1_tac =
    1.68 +      NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n < 0 then all_tac else no_tac);
    1.69 +  in DEPTH_SOLVE solve1_tac end;
    1.70 +
    1.71 +
    1.72  (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
    1.73  fun basic_gen_simp_tac mode =
    1.74    fn (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) =>
    1.75      let
    1.76 -      fun solve_all_tac mss =
    1.77 -        let
    1.78 -          val ss =
    1.79 -            make_ss (mss, subgoal_tac, loop_tac, unsafe_finish_tac, unsafe_finish_tac);
    1.80 -          val solve1_tac =
    1.81 -            NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n < 0 then all_tac else no_tac)
    1.82 -        in DEPTH_SOLVE solve1_tac end;
    1.83 -
    1.84        fun simp_loop_tac i thm =
    1.85 -        (asm_rewrite_goal_tac mode solve_all_tac mss i THEN
    1.86 -          (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm
    1.87 +        (asm_rewrite_goal_tac mode
    1.88 +          (solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac)) mss i
    1.89 +        THEN (finish_tac (prems_of_mss mss) i ORELSE looper i)) thm
    1.90        and allsimp i n = EVERY (map (fn j => simp_loop_tac (i + j)) (n downto 0))
    1.91        and looper i = TRY (NEWSUBGOALS (loop_tac i) (allsimp i));
    1.92    in simp_loop_tac end;
    1.93 @@ -276,4 +285,22 @@
    1.94  fun     Full_simp_tac i =     full_simp_tac (! simpset) i;
    1.95  fun Asm_full_simp_tac i = asm_full_simp_tac (! simpset) i;
    1.96  
    1.97 +
    1.98 +
    1.99 +(** simplification meta rules **)
   1.100 +
   1.101 +fun simp mode (Simpset {mss, subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac}) thm =
   1.102 +  let
   1.103 +    val tacf = solve_all_tac (subgoal_tac, loop_tac, finish_tac, unsafe_finish_tac);
   1.104 +    fun prover m th = apsome fst (Sequence.pull (tacf m th));
   1.105 +  in
   1.106 +    Drule.rewrite_thm mode prover mss thm
   1.107 +  end;
   1.108 +
   1.109 +val          simplify = simp (false, false);
   1.110 +val      asm_simplify = simp (false, true);
   1.111 +val     full_simplify = simp (true, false);
   1.112 +val asm_full_simplify = simp (true, true);
   1.113 +
   1.114 +
   1.115  end;