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