src/Pure/tactic.ML
author nipkow
Fri, 28 Jul 1995 17:24:53 +0200
changeset 1209 03dc596b3a18
parent 1077 c2df11ae8b55
child 1458 fd510875fb71
permissions -rw-r--r--
added rotate_tac.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Tactics 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
signature TACTIC =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
  structure Tactical: TACTICAL and Net: NET
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  local open Tactical Tactical.Thm Net
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  val ares_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val asm_rewrite_goal_tac:
214
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 191
diff changeset
    16
        bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val assume_tac: int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  val atac: int ->tactic
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    19
  val bimatch_from_nets_tac: 
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    20
      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val bimatch_tac: (bool*thm)list -> int -> tactic
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    22
  val biresolve_from_nets_tac: 
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    23
      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  val biresolve_tac: (bool*thm)list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  val build_net: thm list -> (int*thm) net
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    26
  val build_netpair:    (int*(bool*thm)) net * (int*(bool*thm)) net ->
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    27
      (bool*thm)list -> (int*(bool*thm)) net * (int*(bool*thm)) net
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val compose_tac: (bool * thm * int) -> int -> tactic 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val cut_facts_tac: thm list -> int -> tactic
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
    31
  val cut_inst_tac: (string*string)list -> thm -> int -> tactic   
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
  val dmatch_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  val dresolve_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  val dres_inst_tac: (string*string)list -> thm -> int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  val dtac: thm -> int ->tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  val etac: thm -> int ->tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  val eq_assume_tac: int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  val ematch_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  val eresolve_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  val eres_inst_tac: (string*string)list -> thm -> int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  val filter_thms: (term*term->bool) -> int*term*thm list -> thm list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  val filt_resolve_tac: thm list -> int -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  val flexflex_tac: tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  val fold_goals_tac: thm list -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  val fold_tac: thm list -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  val forward_tac: thm list -> int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  val forw_inst_tac: (string*string)list -> thm -> int -> tactic
947
812ccc91bfa0 Put freeze into the signature TACTIC for export
lcp
parents: 922
diff changeset
    48
  val freeze: thm -> thm   
1077
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
    49
  val insert_tagged_brl:  ('a*(bool*thm)) * 
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
    50
                    (('a*(bool*thm))net * ('a*(bool*thm))net) ->
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
    51
                    ('a*(bool*thm))net * ('a*(bool*thm))net
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  val is_fact: thm -> bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  val lessb: (bool * thm) * (bool * thm) -> bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  val lift_inst_rule: thm * int * (string*string)list * thm -> thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
  val make_elim: thm -> thm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  val match_from_net_tac: (int*thm) net -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  val match_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
  val metacut_tac: thm -> int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  val net_bimatch_tac: (bool*thm) list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
  val net_biresolve_tac: (bool*thm) list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  val net_match_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  val net_resolve_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  val PRIMITIVE: (thm -> thm) -> tactic  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
  val PRIMSEQ: (thm -> thm Sequence.seq) -> tactic  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
  val prune_params_tac: tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
  val rename_tac: string -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  val rename_last_tac: string -> string list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  val resolve_from_net_tac: (int*thm) net -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  val resolve_tac: thm list -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
  val res_inst_tac: (string*string)list -> thm -> int -> tactic   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  val rewrite_goals_tac: thm list -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  val rewrite_tac: thm list -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
  val rewtac: thm -> tactic
1209
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
    74
  val rotate_tac: int -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
  val rtac: thm -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  val rule_by_tactic: tactic -> thm -> thm
439
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
    77
  val subgoal_tac: string -> int -> tactic
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
    78
  val subgoals_tac: string list -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
  val subgoals_of_brl: bool * thm -> int
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
  val trace_goalno_tac: (int -> tactic) -> int -> tactic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
		   Tactical: TACTICAL and Net: NET
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
	  sharing Drule.Thm = Tactical.Thm) : TACTIC = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
structure Tactical = Tactical;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
structure Thm = Tactical.Thm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
structure Net = Net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
structure Sequence = Thm.Sequence;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
structure Sign = Thm.Sign;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
local open Tactical Tactical.Thm Drule
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
(*Discover what goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
fun trace_goalno_tac tf i = Tactic (fn state => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
    case Sequence.pull(tapply(tf i, state)) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
	None    => Sequence.null
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
      | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
    			 Sequence.seqof(fn()=> seqcell)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
fun string_of (a,0) = a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
  | string_of (a,i) = a ^ "_" ^ string_of_int i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
947
812ccc91bfa0 Put freeze into the signature TACTIC for export
lcp
parents: 922
diff changeset
   107
(*convert all Vars in a theorem to Frees*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
fun freeze th =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
  let val fth = freezeT th
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
      val {prop,sign,...} = rep_thm fth
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
      fun mk_inst (Var(v,T)) = 
230
ec8a2b6aa8a7 Many other files modified as follows:
lcp
parents: 214
diff changeset
   112
	  (cterm_of sign (Var(v,T)),
ec8a2b6aa8a7 Many other files modified as follows:
lcp
parents: 214
diff changeset
   113
	   cterm_of sign (Free(string_of v, T)))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
      val insts = map mk_inst (term_vars prop)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
  in  instantiate ([],insts) fth  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
(*Makes a rule by applying a tactic to an existing rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
fun rule_by_tactic (Tactic tf) rl =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    case Sequence.pull(tf (freeze (standard rl))) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
	None        => raise THM("rule_by_tactic", 0, [rl])
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
      | Some(rl',_) => standard rl';
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(*** Basic tactics ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
			                 handle THM _ => Sequence.null);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
(*** The following fail if the goal number is out of range:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
     thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
(*Solve subgoal i by assumption*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
fun assume_tac i = PRIMSEQ (assumption i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
(*Solve subgoal i by assumption, using no unification*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
(** Resolution/matching tactics **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
(*The composition rule/state: no lifting or var renaming.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
  The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
  like [| P&Q; P==>R |] ==> R *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
(*Attack subgoal i by resolution, using flags to indicate elimination rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
(*Resolution: the simple case, works for introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
fun resolve_tac rules = biresolve_tac (map (pair false) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
(*Resolution with elimination rules only*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
(*Forward reasoning using destruction rules.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
(*Like forward_tac, but deletes the assumption after use.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
fun dresolve_tac rls = eresolve_tac (map make_elim rls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(*Shorthand versions: for resolution with a single theorem*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
fun rtac rl = resolve_tac [rl];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
fun etac rl = eresolve_tac [rl];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
fun dtac rl = dresolve_tac [rl];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
val atac = assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
(*Use an assumption or some rules ... A popular combination!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
(*Matching tactics -- as above, but forbid updating of state*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
fun match_tac rules  = bimatch_tac (map (pair false) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
fun ematch_tac rules = bimatch_tac (map (pair true) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
fun dmatch_tac rls   = ematch_tac (map make_elim rls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
(*Smash all flex-flex disagreement pairs in the proof state.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
val flexflex_tac = PRIMSEQ flexflex_rule;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
(*Lift and instantiate a rule wrt the given state and subgoal number *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
fun lift_inst_rule (state, i, sinsts, rule) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
let val {maxidx,sign,...} = rep_thm state
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
    val (_, _, Bi, _) = dest_state(state,i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
    val params = Logic.strip_params Bi	        (*params of subgoal i*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
    val params = rev(rename_wrt_term Bi params) (*as they are printed*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
    val paramTs = map #2 params
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
    and inc = maxidx+1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
      | liftvar t = raise TERM("Variable expected", [t]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
    fun liftterm t = list_abs_free (params, 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
				    Logic.incr_indexes(paramTs,inc) t)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
    (*Lifts instantiation pair over params*)
230
ec8a2b6aa8a7 Many other files modified as follows:
lcp
parents: 214
diff changeset
   197
    fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
    fun lifttvar((a,i),ctyp) =
230
ec8a2b6aa8a7 Many other files modified as follows:
lcp
parents: 214
diff changeset
   199
	let val {T,sign} = rep_ctyp ctyp
ec8a2b6aa8a7 Many other files modified as follows:
lcp
parents: 214
diff changeset
   200
	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
    val rts = types_sorts rule and (types,sorts) = types_sorts state
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
      | types'(ixn) = types ixn;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 947
diff changeset
   204
    val used = add_term_tvarnames
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 947
diff changeset
   205
                  (#prop(rep_thm state) $ #prop(rep_thm rule),[])
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 947
diff changeset
   206
    val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
in instantiate (map lifttvar Tinsts, map liftpair insts)
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 947
diff changeset
   208
               (lift_rule (state,i) rule)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
(*** Resolve after lifting and instantation; may refer to parameters of the
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
     subgoal.  Fails if "i" is out of range.  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
(*compose version: arguments are as for bicompose.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
  STATE ( fn state => 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
			nsubgoal) i
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
	   handle TERM (msg,_) => (writeln msg;  no_tac)
191
fe5d88d4c7e1 Pure/tactic/compose_inst_tac: when catching exception THM, prints the
lcp
parents: 69
diff changeset
   221
		| THM  (msg,_,_) => (writeln msg;  no_tac) );
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
761
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   223
(*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   224
  terms that are substituted contain (term or type) unknowns from the
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   225
  goal, because it is unable to instantiate goal unknowns at the same time.
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   226
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   227
  The type checker is instructed not to freezes flexible type vars that
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   228
  were introduced during type inference and still remain in the term at the
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   229
  end.  This increases flexibility but can introduce schematic type vars in
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   230
  goals.
761
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   231
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
fun res_inst_tac sinsts rule i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
    compose_inst_tac sinsts (false, rule, nprems_of rule) i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
(*eresolve (elimination) version*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
fun eres_inst_tac sinsts rule i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
    compose_inst_tac sinsts (true, rule, nprems_of rule) i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   239
(*For forw_inst_tac and dres_inst_tac.  Preserve Var indexes of rl;
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   240
  increment revcut_rl instead.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
fun make_elim_preserve rl = 
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   242
  let val {maxidx,...} = rep_thm rl
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 761
diff changeset
   243
      fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   244
      val revcut_rl' = 
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   245
	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   246
			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
      val arg = (false, rl, nprems_of rl)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
      val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
  in  th  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
  handle Bind => raise THM("make_elim_preserve", 1, [rl]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   252
(*instantiate and cut -- for a FACT, anyway...*)
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   253
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   255
(*forward tactic applies a RULE to an assumption without deleting it*)
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   256
fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac;
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   257
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   258
(*dresolve tactic applies a RULE to replace an assumption*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   261
(*** Applications of cut_rl ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
(*Used by metacut_tac*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
fun bires_cut_tac arg i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
    resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
(*The conclusion of the rule gets assumed in subgoal i,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
  while subgoal i+1,... are the premises of the rule.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
fun metacut_tac rule = bires_cut_tac [(false,rule)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
(*Recognizes theorems that are not rules, but simple propositions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
fun is_fact rl =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
    case prems_of rl of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
	[] => true  |  _::_ => false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
(*"Cut" all facts from theorem list into the goal as assumptions. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
fun cut_facts_tac ths i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
    EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
(*Introduce the given proposition as a lemma and subgoal*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
439
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
   283
(*Introduce a list of lemmas and subgoals*)
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
   284
fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops);
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
   285
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
(**** Indexing and filtering of theorems ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
(*Returns the list of potentially resolvable theorems for the goal "prem",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
	using the predicate  could(subgoal,concl).
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
  Resulting list is no longer than "limit"*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
fun filter_thms could (limit, prem, ths) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
  let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
      fun filtr (limit, []) = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
	| filtr (limit, th::ths) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
	    if limit=0 then  []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
	    else filtr(limit,ths)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
  in  filtr(limit,ths)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
(*** biresolution and resolution using nets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
(** To preserve the order of the rules, tag them with increasing integers **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
(*insert tags*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
fun taglist k [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
  | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   310
(*remove tags and suppress duplicates -- list is assumed sorted!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
fun untaglist [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
  | untaglist [(k:int,x)] = [x]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
  | untaglist ((k,x) :: (rest as (k',x')::_)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
      if k=k' then untaglist rest
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
      else    x :: untaglist rest;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
(*return list elements in original order*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
(*insert one tagged brl into the pair of nets*)
1077
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
   321
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
    if eres then 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
	case prems_of th of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
1077
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
   325
	  | [] => error"insert_tagged_brl: elimination rule with no premises"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
    else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
(*build a pair of nets for biresolution*)
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   329
fun build_netpair netpair brls = 
1077
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
   330
    foldr insert_tagged_brl (taglist 1 brls, netpair);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
(*biresolution using a pair of nets rather than rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
fun biresolution_from_nets_tac match (inet,enet) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
  SUBGOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
    (fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
      let val hyps = Logic.strip_assums_hyp prem
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
          and concl = Logic.strip_assums_concl prem 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
          val kbrls = Net.unify_term inet concl @
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
                      flat (map (Net.unify_term enet) hyps)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
      in PRIMSEQ (biresolution match (orderlist kbrls) i) end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   342
(*versions taking pre-built nets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
val biresolve_from_nets_tac = biresolution_from_nets_tac false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
val bimatch_from_nets_tac = biresolution_from_nets_tac true;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
(*fast versions using nets internally*)
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   347
val net_biresolve_tac =
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   348
    biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty);
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   349
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   350
val net_bimatch_tac =
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   351
    bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   352
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   353
(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   354
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   355
(*insert one tagged rl into the net*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
fun insert_krl (krl as (k,th), net) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
    Net.insert_term ((concl_of th, krl), net, K false);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
(*build a net of rules for resolution*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
fun build_net rls = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
    foldr insert_krl (taglist 1 rls, Net.empty);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
fun filt_resolution_from_net_tac match pred net =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
  SUBGOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
    (fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
      let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
      in 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
	 if pred krls  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
         then PRIMSEQ
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
		(biresolution match (map (pair false) (orderlist krls)) i)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
         else no_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
      end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   375
(*Resolve the subgoal using the rules (making a net) unless too flexible,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
   which means more than maxr rules are unifiable.      *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
fun filt_resolve_tac rules maxr = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
    let fun pred krls = length krls <= maxr
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
    in  filt_resolution_from_net_tac false pred (build_net rules)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   380
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
(*versions taking pre-built nets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
val match_from_net_tac = filt_resolution_from_net_tac true (K true);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
(*fast versions using nets internally*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
val net_resolve_tac = resolve_from_net_tac o build_net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
val net_match_tac = match_from_net_tac o build_net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
(*** For Natural Deduction using (bires_flg, rule) pairs ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   392
(*The number of new subgoals produced by the brule*)
1077
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
   393
fun subgoals_of_brl (true,rule)  = nprems_of rule - 1
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
   394
  | subgoals_of_brl (false,rule) = nprems_of rule;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
(*Less-than test: for sorting to minimize number of new subgoals*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   398
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
(*** Meta-Rewriting Tactics ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
fun result1 tacf mss thm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   403
  case Sequence.pull(tapply(tacf mss,thm)) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   404
    None => None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   405
  | Some(thm,_) => Some(thm);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   406
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
(*Rewrite subgoal i only *)
214
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 191
diff changeset
   408
fun asm_rewrite_goal_tac mode prover_tac mss i =
ed6a3e2b1a33 added new parameter to the simplification tactics which indicates if
nipkow
parents: 191
diff changeset
   409
      PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   411
(*Rewrite throughout proof state. *)
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   412
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
(*Rewrite subgoals only, not main goal. *)
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   415
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   417
fun rewtac def = rewrite_goals_tac [def];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   420
(*** Tactic for folding definitions, handling critical pairs ***)
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   421
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   422
(*The depth of nesting in a term*)
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   423
fun term_depth (Abs(a,T,t)) = 1 + term_depth t
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   424
  | term_depth (f$t) = 1 + max [term_depth f, term_depth t]
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   425
  | term_depth _ = 0;
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   426
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   427
val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm;
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   428
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   429
(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   430
  Returns longest lhs first to avoid folding its subexpressions.*)
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   431
fun sort_lhs_depths defs =
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   432
  let val keylist = make_keylist (term_depth o lhs_of_thm) defs
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   433
      val keys = distinct (sort op> (map #2 keylist))
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   434
  in  map (keyfilter keylist) keys  end;
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   435
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   436
fun fold_tac defs = EVERY 
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   437
    (map rewrite_tac (sort_lhs_depths (map symmetric defs)));
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   438
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   439
fun fold_goals_tac defs = EVERY 
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   440
    (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs)));
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   441
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   442
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   443
(*** Renaming of parameters in a subgoal
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   444
     Names may contain letters, digits or primes and must be
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   445
     separated by blanks ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
(*Calling this will generate the warning "Same as previous level" since
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   448
  it affects nothing but the names of bound variables!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
fun rename_tac str i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
  let val cs = explode str 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
  in  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   452
  if !Logic.auto_rename 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
  then (writeln"Note: setting Logic.auto_rename := false"; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
	Logic.auto_rename := false)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
  else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
  case #2 (take_prefix (is_letdig orf is_blank) cs) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
      [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
    | c::_ => error ("Illegal character: " ^ c)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
(*Rename recent parameters using names generated from (a) and the suffixes,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
  provided the string (a), which represents a term, is an identifier. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
fun rename_last_tac a sufs i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
  let val names = map (curry op^ a) sufs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
  in  if Syntax.is_identifier a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   466
      then PRIMITIVE (rename_params_rule (names,i))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
      else all_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   470
(*Prunes all redundant parameters from the proof state by rewriting*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
val prune_params_tac = rewrite_tac [triv_forall_equality];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
1209
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   473
(* rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   474
 * right to left if n is positive, and from left to right if n is negative.
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   475
 *)
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   476
fun rotate_tac n =
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   477
  let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   478
  in if n >= 0 then rot n
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   479
     else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i)
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   480
  end;
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   481
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   482
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   483
end;