src/Provers/clasimp.ML
author oheimb
Wed Feb 25 20:25:27 1998 +0100 (1998-02-25)
changeset 4652 d24cca140eeb
child 4659 a78ecc7341e3
permissions -rw-r--r--
factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML
explicitly introducing combined type clasimpset
oheimb@4652
     1
(*  Title: 	Provers/clasimp.ML
oheimb@4652
     2
    ID:         $Id$
oheimb@4652
     3
    Author:     David von Oheimb, TU Muenchen
oheimb@4652
     4
oheimb@4652
     5
Combination of classical reasoner and simplifier
oheimb@4652
     6
to be used after installing both of them
oheimb@4652
     7
*)
oheimb@4652
     8
oheimb@4652
     9
infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
oheimb@4652
    10
	addsimps2 delsimps2 addcongs2 delcongs2;
oheimb@4652
    11
infix 4 addSss addss;
oheimb@4652
    12
oheimb@4652
    13
type clasimpset = claset * simpset;
oheimb@4652
    14
oheimb@4652
    15
signature CLASIMP =
oheimb@4652
    16
sig
oheimb@4652
    17
  val addSIs2	: clasimpset * thm list -> clasimpset
oheimb@4652
    18
  val addSEs2	: clasimpset * thm list -> clasimpset
oheimb@4652
    19
  val addSDs2	: clasimpset * thm list -> clasimpset
oheimb@4652
    20
  val addIs2	: clasimpset * thm list -> clasimpset
oheimb@4652
    21
  val addEs2	: clasimpset * thm list -> clasimpset
oheimb@4652
    22
  val addDs2	: clasimpset * thm list -> clasimpset
oheimb@4652
    23
  val addsimps2	: clasimpset * thm list -> clasimpset
oheimb@4652
    24
  val delsimps2	: clasimpset * thm list -> clasimpset
oheimb@4652
    25
  val addSss	: claset * simpset -> claset
oheimb@4652
    26
  val addss	: claset * simpset -> claset
oheimb@4652
    27
  val mk_auto_tac:clasimpset -> int -> int -> tactic
oheimb@4652
    28
  val auto_tac	: clasimpset -> tactic
oheimb@4652
    29
  val Auto_tac	: tactic
oheimb@4652
    30
  val auto	: unit -> unit
oheimb@4652
    31
end;
oheimb@4652
    32
oheimb@4652
    33
structure Clasimp: CLASIMP =
oheimb@4652
    34
struct
oheimb@4652
    35
oheimb@4652
    36
local 
oheimb@4652
    37
  fun pair_upd1 f ((a,b),x) = (f(a,x), b);
oheimb@4652
    38
  fun pair_upd2 f ((a,b),x) = (a, f(b,x));
oheimb@4652
    39
in
oheimb@4652
    40
  fun op addSIs2   arg = pair_upd1 (op addSIs) arg;
oheimb@4652
    41
  fun op addSEs2   arg = pair_upd1 (op addSEs) arg;
oheimb@4652
    42
  fun op addSDs2   arg = pair_upd1 (op addSDs) arg;
oheimb@4652
    43
  fun op addIs2    arg = pair_upd1 (op addIs ) arg;
oheimb@4652
    44
  fun op addEs2    arg = pair_upd1 (op addEs ) arg;
oheimb@4652
    45
  fun op addDs2    arg = pair_upd1 (op addDs ) arg;
oheimb@4652
    46
  fun op addsimps2 arg = pair_upd2 (op addsimps) arg;
oheimb@4652
    47
  fun op delsimps2 arg = pair_upd2 (op delsimps) arg;
oheimb@4652
    48
  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
oheimb@4652
    49
  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
oheimb@4652
    50
end;
oheimb@4652
    51
oheimb@4652
    52
(*an unsatisfactory fix for the incomplete safe_asm_full_simp_tac!
oheimb@4652
    53
  better: asm_really_full_simp_tac, a yet to be implemented version of
oheimb@4652
    54
			asm_full_simp_tac that applies all equalities in the
oheimb@4652
    55
			premises to all the premises *)
oheimb@4652
    56
fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
oheimb@4652
    57
				     safe_asm_full_simp_tac ss;
oheimb@4652
    58
oheimb@4652
    59
(*Add a simpset to a classical set!*)
oheimb@4652
    60
(*Caution: only one simpset added can be added by each of addSss and addss*)
oheimb@4652
    61
fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
oheimb@4652
    62
			CHANGED o (safe_asm_more_full_simp_tac ss));
oheimb@4652
    63
fun cs addss  ss = cs addbefore  (     "asm_full_simp_tac",
oheimb@4652
    64
					asm_full_simp_tac ss);
oheimb@4652
    65
oheimb@4652
    66
oheimb@4652
    67
local
oheimb@4652
    68
oheimb@4652
    69
	fun blast_depth_tac cs m i thm = Blast.depth_tac cs m i thm 
oheimb@4652
    70
		handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
oheimb@4652
    71
oheimb@4652
    72
	(* a variant of depth_tac that avoids interference of the simplifier 
oheimb@4652
    73
	   with dup_step_tac when they are combined by auto_tac *)
oheimb@4652
    74
	fun nodup_depth_tac cs m i state = 
oheimb@4652
    75
	  SELECT_GOAL 
oheimb@4652
    76
	   (appWrappers cs
oheimb@4652
    77
	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
oheimb@4652
    78
	                             (safe_step_tac cs i)) THEN_ELSE
oheimb@4652
    79
	     (DEPTH_SOLVE (nodup_depth_tac cs m i),
oheimb@4652
    80
	      inst0_step_tac cs i  APPEND
oheimb@4652
    81
	      COND (K(m=0)) no_tac
oheimb@4652
    82
	        ((instp_step_tac cs i APPEND step_tac cs i)
oheimb@4652
    83
	         THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
oheimb@4652
    84
	  i state;
oheimb@4652
    85
oheimb@4652
    86
in
oheimb@4652
    87
oheimb@4652
    88
(*Designed to be idempotent, except if best_tac instantiates variables
oheimb@4652
    89
  in some of the subgoals*)
oheimb@4652
    90
fun mk_auto_tac (cs, ss) m n =
oheimb@4652
    91
    let val cs' = cs addss ss 
oheimb@4652
    92
        val maintac = 
oheimb@4652
    93
          blast_depth_tac cs m		(*fast but can't use addss*)
oheimb@4652
    94
          ORELSE'
oheimb@4652
    95
          nodup_depth_tac cs' n;	(*slower but more general*)
oheimb@4652
    96
    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
oheimb@4652
    97
	       TRY (safe_tac cs'),
oheimb@4652
    98
	       REPEAT (FIRSTGOAL maintac),
oheimb@4652
    99
               TRY (safe_tac (cs addSss ss)),
oheimb@4652
   100
	       prune_params_tac] 
oheimb@4652
   101
    end;
oheimb@4652
   102
end;
oheimb@4652
   103
oheimb@4652
   104
fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
oheimb@4652
   105
oheimb@4652
   106
fun Auto_tac st = auto_tac (claset(), simpset()) st;
oheimb@4652
   107
oheimb@4652
   108
fun auto () = by Auto_tac;
oheimb@4652
   109
oheimb@4652
   110
end;