src/Pure/tactic.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18500 8b1a4e8ed199
child 18977 f24c416a4814
permissions -rw-r--r--
simplified type attribute;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
     1
(*  Title:      Pure/tactic.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
     6
Tactics.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
     9
signature BASIC_TACTIC =
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
    10
sig
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    11
  val ares_tac          : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    12
  val assume_tac        : int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    13
  val atac      : int ->tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    14
  val bimatch_from_nets_tac:
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    15
      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    16
  val bimatch_tac       : (bool*thm)list -> int -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    17
  val biresolution_from_nets_tac:
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    18
        ('a list -> (bool * thm) list) ->
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    19
        bool -> 'a Net.net * 'a Net.net -> int -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    20
  val biresolve_from_nets_tac:
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    21
      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    22
  val biresolve_tac     : (bool*thm)list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    23
  val build_net : thm list -> (int*thm) Net.net
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    24
  val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    25
      (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    26
  val compose_inst_tac  : (string*string)list -> (bool*thm*int) ->
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    27
                          int -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    28
  val compose_tac       : (bool * thm * int) -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    29
  val cut_facts_tac     : thm list -> int -> tactic
13650
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13559
diff changeset
    30
  val cut_rules_tac     : thm list -> int -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    31
  val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
    32
  val datac             : thm -> int -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    33
  val defer_tac         : int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    34
  val distinct_subgoals_tac     : tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    35
  val dmatch_tac        : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    36
  val dresolve_tac      : thm list -> int -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    37
  val dres_inst_tac     : (string*string)list -> thm -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    38
  val dtac              : thm -> int ->tactic
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
    39
  val eatac             : thm -> int -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    40
  val etac              : thm -> int ->tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    41
  val eq_assume_tac     : int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    42
  val ematch_tac        : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    43
  val eresolve_tac      : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    44
  val eres_inst_tac     : (string*string)list -> thm -> int -> tactic
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
    45
  val fatac             : thm -> int -> int -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    46
  val filter_prems_tac  : (term -> bool) -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    47
  val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    48
  val filt_resolve_tac  : thm list -> int -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    49
  val flexflex_tac      : tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    50
  val fold_goals_tac    : thm list -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    51
  val fold_rule         : thm list -> thm -> thm
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    52
  val fold_tac          : thm list -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    53
  val forward_tac       : thm list -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    54
  val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    55
  val ftac              : thm -> int ->tactic
12320
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
    56
  val insert_tagged_brl : ('a * (bool * thm)) *
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
    57
    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
    58
      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
    59
  val delete_tagged_brl : (bool * thm) *
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
    60
    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
    61
      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    62
  val is_fact           : thm -> bool
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    63
  val lessb             : (bool * thm) * (bool * thm) -> bool
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    64
  val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    65
  val make_elim         : thm -> thm
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    66
  val match_from_net_tac        : (int*thm) Net.net -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    67
  val match_tac : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    68
  val metacut_tac       : thm -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    69
  val net_bimatch_tac   : (bool*thm) list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    70
  val net_biresolve_tac : (bool*thm) list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    71
  val net_match_tac     : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    72
  val net_resolve_tac   : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    73
  val norm_hhf_tac      : int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    74
  val prune_params_tac  : tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    75
  val rename_params_tac : string list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    76
  val rename_tac        : string -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    77
  val rename_last_tac   : string -> string list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    78
  val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    79
  val resolve_tac       : thm list -> int -> tactic
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
    80
  val res_inst_tac      : (string*string)list -> thm -> int -> tactic
10444
2dfa19236768 added rewrite_goal_tac;
wenzelm
parents: 10415
diff changeset
    81
  val rewrite_goal_tac  : thm list -> int -> tactic
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
    82
  val rewrite_goals_rule: thm list -> thm -> thm
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    83
  val rewrite_rule      : thm list -> thm -> thm
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    84
  val rewrite_goals_tac : thm list -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    85
  val rewrite_tac       : thm list -> tactic
17968
d50f08d9aabb moved norm_hhf_rule, prove etc. to goal.ML;
wenzelm
parents: 17892
diff changeset
    86
  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    87
  val rewtac            : thm -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    88
  val rotate_tac        : int -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    89
  val rtac              : thm -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    90
  val rule_by_tactic    : tactic -> thm -> thm
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    91
  val solve_tac         : thm list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    92
  val subgoal_tac       : string -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    93
  val subgoals_tac      : string list -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    94
  val subgoals_of_brl   : bool * thm -> int
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    95
  val term_lift_inst_rule       :
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15696
diff changeset
    96
      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm
1975
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
    97
      -> thm
10347
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9535
diff changeset
    98
  val instantiate_tac   : (string * string) list -> tactic
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
    99
  val thin_tac          : string -> int -> tactic
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   100
  val trace_goalno_tac  : (int -> tactic) -> int -> tactic
18500
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   101
  val CONJUNCTS: tactic -> int -> tactic
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   102
  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   103
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   105
signature TACTIC =
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   106
sig
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   107
  include BASIC_TACTIC
11929
a77ad6c86564 innermost_params;
wenzelm
parents: 11774
diff changeset
   108
  val innermost_params: int -> thm -> (string * typ) list
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   109
  val untaglist: (int * 'a) list -> 'a list
16809
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   110
  val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   111
  val orderlist: (int * 'a) list -> 'a list
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   112
  val rewrite: bool -> thm list -> cterm -> thm
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   113
  val simplify: bool -> thm list -> thm -> thm
18471
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   114
  val conjunction_tac: int -> tactic
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   115
  val precise_conjunction_tac: int -> int -> tactic
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   116
  val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   117
                          int -> tactic
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   118
  val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
15464
02cc838b64ca Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents: 15453
diff changeset
   119
  val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   120
  val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15696
diff changeset
   121
  val instantiate_tac'  : (indexname * string) list -> tactic
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   122
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   124
structure Tactic: TACTIC =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   127
(*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   128
fun trace_goalno_tac tac i st =
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   129
    case Seq.pull(tac i st) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   130
        NONE    => Seq.empty
12262
11ff5f47df6e use tracing function for trace output;
wenzelm
parents: 12212
diff changeset
   131
      | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected");
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   132
                         Seq.make(fn()=> seqcell));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
(*Makes a rule by applying a tactic to an existing rule*)
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   135
fun rule_by_tactic tac rl =
2688
889a1cbd1aca rule_by_tactic no longer standardizes its result
paulson
parents: 2672
diff changeset
   136
  let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   137
  in case Seq.pull (tac st)  of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   138
        NONE        => raise THM("rule_by_tactic", 0, [rl])
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   139
      | SOME(st',_) => Thm.varifyT (thaw st')
2688
889a1cbd1aca rule_by_tactic no longer standardizes its result
paulson
parents: 2672
diff changeset
   140
  end;
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   141
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
(*** Basic tactics ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
(*** The following fail if the goal number is out of range:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
     thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
(*Solve subgoal i by assumption*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
fun assume_tac i = PRIMSEQ (assumption i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
(*Solve subgoal i by assumption, using no unification*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
(** Resolution/matching tactics **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
(*The composition rule/state: no lifting or var renaming.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
  The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
  like [| P&Q; P==>R |] ==> R *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
(*Attack subgoal i by resolution, using flags to indicate elimination rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(*Resolution: the simple case, works for introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
fun resolve_tac rules = biresolve_tac (map (pair false) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
(*Resolution with elimination rules only*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
(*Forward reasoning using destruction rules.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
(*Like forward_tac, but deletes the assumption after use.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
fun dresolve_tac rls = eresolve_tac (map make_elim rls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
(*Shorthand versions: for resolution with a single theorem*)
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   179
val atac    =   assume_tac;
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   180
fun rtac rl =  resolve_tac [rl];
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   181
fun dtac rl = dresolve_tac [rl];
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   182
fun etac rl = eresolve_tac [rl];
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   183
fun ftac rl =  forward_tac [rl];
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   184
fun datac thm j = EVERY' (dtac thm::replicate j atac);
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   185
fun eatac thm j = EVERY' (etac thm::replicate j atac);
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   186
fun fatac thm j = EVERY' (ftac thm::replicate j atac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
(*Use an assumption or some rules ... A popular combination!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
5263
8862ed2db431 added solve_tac;
wenzelm
parents: 4713
diff changeset
   191
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
8862ed2db431 added solve_tac;
wenzelm
parents: 4713
diff changeset
   192
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
(*Matching tactics -- as above, but forbid updating of state*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
fun match_tac rules  = bimatch_tac (map (pair false) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
fun ematch_tac rules = bimatch_tac (map (pair true) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
fun dmatch_tac rls   = ematch_tac (map make_elim rls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
(*Smash all flex-flex disagreement pairs in the proof state.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
val flexflex_tac = PRIMSEQ flexflex_rule;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   202
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   203
(*Remove duplicate subgoals.  By Mark Staples*)
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   204
local
16666
9a987b59ecab cterm_aconv: avoid rep_cterm;
wenzelm
parents: 16425
diff changeset
   205
fun cterm_aconv (a,b) = term_of a aconv term_of b;
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   206
in
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   207
fun distinct_subgoals_tac state =
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   208
    let val (frozth,thawfn) = freeze_thaw state
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   209
        val froz_prems = cprems_of frozth
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   210
        val assumed = implies_elim_list frozth (map assume froz_prems)
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   211
        val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   212
                                        assumed;
15977
aa6744dd998e added comment
paulson
parents: 15874
diff changeset
   213
    in  (*Applying Thm.varifyT to the result of thawfn would (re-)generalize
aa6744dd998e added comment
paulson
parents: 15874
diff changeset
   214
          all type variables that appear in the subgoals. Unfortunately, it
aa6744dd998e added comment
paulson
parents: 15874
diff changeset
   215
          would also break the function AxClass.intro_classes_tac, even in the
aa6744dd998e added comment
paulson
parents: 15874
diff changeset
   216
          trivial case where the type class has no axioms.*)
aa6744dd998e added comment
paulson
parents: 15874
diff changeset
   217
        Seq.single (thawfn implied)
aa6744dd998e added comment
paulson
parents: 15874
diff changeset
   218
    end
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   219
end;
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   220
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   221
11929
a77ad6c86564 innermost_params;
wenzelm
parents: 11774
diff changeset
   222
(*Determine print names of goal parameters (reversed)*)
a77ad6c86564 innermost_params;
wenzelm
parents: 11774
diff changeset
   223
fun innermost_params i st =
a77ad6c86564 innermost_params;
wenzelm
parents: 11774
diff changeset
   224
  let val (_, _, Bi, _) = dest_state (st, i)
a77ad6c86564 innermost_params;
wenzelm
parents: 11774
diff changeset
   225
  in rename_wrt_term Bi (Logic.strip_params Bi) end;
a77ad6c86564 innermost_params;
wenzelm
parents: 11774
diff changeset
   226
15453
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   227
(*params of subgoal i as they are printed*)
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   228
fun params_of_state st i =
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   229
  let val (_, _, Bi, _) = dest_state(st,i)
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   230
      val params = Logic.strip_params Bi
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   231
  in rev(rename_wrt_term Bi params) end;
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   232
15453
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   233
(*read instantiations with respect to subgoal i of proof state st*)
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   234
fun read_insts_in_state (st, i, sinsts, rule) =
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   235
  let val thy = Thm.theory_of_thm st
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   236
      and params = params_of_state st i
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   237
      and rts = types_sorts rule and (types,sorts) = types_sorts st
17271
2756a73f63a5 introduced some new-style AList operations
haftmann
parents: 17203
diff changeset
   238
      fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   239
        | types' ixn = types ixn;
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   240
      val used = Drule.add_used rule (Drule.add_used st []);
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   241
  in read_insts thy rts (types',sorts) used sinsts end;
15453
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   242
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
(*Lift and instantiate a rule wrt the given state and subgoal number *)
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   244
fun lift_inst_rule' (st, i, sinsts, rule) =
15453
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   245
let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   246
    and {maxidx,...} = rep_thm st
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   247
    and params = params_of_state st i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
    val paramTs = map #2 params
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
    and inc = maxidx+1
16876
f57b38cced32 Logic.incr_tvar;
wenzelm
parents: 16809
diff changeset
   250
    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
      | liftvar t = raise TERM("Variable expected", [t]);
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   252
    fun liftterm t = list_abs_free (params,
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   253
                                    Logic.incr_indexes(paramTs,inc) t)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
    (*Lifts instantiation pair over params*)
230
ec8a2b6aa8a7 Many other files modified as follows:
lcp
parents: 214
diff changeset
   255
    fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
16876
f57b38cced32 Logic.incr_tvar;
wenzelm
parents: 16809
diff changeset
   256
    val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
8129
29e239c7b8c2 Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents: 7596
diff changeset
   257
in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
18145
6757627acf59 renamed Thm.cgoal_of to Thm.cprem_of;
wenzelm
parents: 18034
diff changeset
   258
                     (Thm.lift_rule (Thm.cprem_of st i) rule)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   261
fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   262
  (st, i, map (apfst Syntax.indexname) sinsts, rule);
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   263
3984
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   264
(*
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   265
Like lift_inst_rule but takes terms, not strings, where the terms may contain
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   266
Bounds referring to parameters of the subgoal.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   267
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   268
insts: [...,(vj,tj),...]
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   269
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   270
The tj may contain references to parameters of subgoal i of the state st
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   271
in the form of Bound k, i.e. the tj may be subterms of the subgoal.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   272
To saturate the lose bound vars, the tj are enclosed in abstractions
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   273
corresponding to the parameters of subgoal i, thus turning them into
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   274
functions. At the same time, the types of the vj are lifted.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   275
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   276
NB: the types in insts must be correctly instantiated already,
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   277
    i.e. Tinsts is not applied to insts.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   278
*)
1975
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
   279
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   280
let val {maxidx,thy,...} = rep_thm st
15453
6318e634e6cc some rationalizing of res_inst_tac
paulson
parents: 15442
diff changeset
   281
    val paramTs = map #2 (params_of_state st i)
1966
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   282
    and inc = maxidx+1
16876
f57b38cced32 Logic.incr_tvar;
wenzelm
parents: 16809
diff changeset
   283
    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
1975
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
   284
    (*lift only Var, not term, which must be lifted already*)
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   285
    fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15696
diff changeset
   286
    fun liftTpair (((a, i), S), T) =
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   287
      (ctyp_of thy (TVar ((a, i + inc), S)),
16876
f57b38cced32 Logic.incr_tvar;
wenzelm
parents: 16809
diff changeset
   288
       ctyp_of thy (Logic.incr_tvar inc T))
8129
29e239c7b8c2 Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents: 7596
diff changeset
   289
in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
18145
6757627acf59 renamed Thm.cgoal_of to Thm.cprem_of;
wenzelm
parents: 18034
diff changeset
   290
                     (Thm.lift_rule (Thm.cprem_of st i) rule)
1966
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   291
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
(*** Resolve after lifting and instantation; may refer to parameters of the
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
     subgoal.  Fails if "i" is out of range.  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
(*compose version: arguments are as for bicompose.*)
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   297
fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
8977
dd8bc754a072 res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents: 8129
diff changeset
   298
  if i > nprems_of st then no_tac st
dd8bc754a072 res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents: 8129
diff changeset
   299
  else st |>
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   300
    (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
12262
11ff5f47df6e use tracing function for trace output;
wenzelm
parents: 12212
diff changeset
   301
     handle TERM (msg,_)   => (warning msg;  no_tac)
11ff5f47df6e use tracing function for trace output;
wenzelm
parents: 12212
diff changeset
   302
          | THM  (msg,_,_) => (warning msg;  no_tac));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   304
val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   305
val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   306
761
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   307
(*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   308
  terms that are substituted contain (term or type) unknowns from the
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   309
  goal, because it is unable to instantiate goal unknowns at the same time.
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   310
2029
2fa4c4b1a7fe Generalized freeze to freeze_thaw in order to
paulson
parents: 1975
diff changeset
   311
  The type checker is instructed not to freeze flexible type vars that
952
9e10962866b0 Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents: 949
diff changeset
   312
  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
   313
  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
   314
  goals.
761
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   315
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
fun res_inst_tac sinsts rule i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
    compose_inst_tac sinsts (false, rule, nprems_of rule) i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
15442
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   319
fun res_inst_tac' sinsts rule i =
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   320
    compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
3b75e1b22ff1 Added variants of instantiation functions that operate on pairs of type
berghofe
parents: 15021
diff changeset
   321
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   322
(*eresolve elimination version*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
fun eres_inst_tac sinsts rule i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
    compose_inst_tac sinsts (true, rule, nprems_of rule) i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
15464
02cc838b64ca Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents: 15453
diff changeset
   326
fun eres_inst_tac' sinsts rule i =
02cc838b64ca Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents: 15453
diff changeset
   327
    compose_inst_tac' sinsts (true, rule, nprems_of rule) i;
02cc838b64ca Added variant of eres_inst_tac that operates on indexnames instead of strings.
berghofe
parents: 15453
diff changeset
   328
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   329
(*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
   330
  increment revcut_rl instead.*)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   331
fun make_elim_preserve rl =
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   332
  let val {maxidx,...} = rep_thm rl
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   333
      fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   334
      val revcut_rl' =
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   335
          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   336
                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
      val arg = (false, rl, nprems_of rl)
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   338
      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
  in  th  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
  handle Bind => raise THM("make_elim_preserve", 1, [rl]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   342
(*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
   343
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   345
(*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
   346
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
   347
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   348
(*dresolve tactic applies a RULE to replace an assumption*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
10347
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9535
diff changeset
   351
(*instantiate variables in the whole state*)
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9535
diff changeset
   352
val instantiate_tac = PRIMITIVE o read_instantiate;
c0cfc4ac12e2 added instantiate_tac
oheimb
parents: 9535
diff changeset
   353
15797
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15696
diff changeset
   354
val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
a63605582573 - Eliminated nodup_vars check.
berghofe
parents: 15696
diff changeset
   355
1951
f2b8005bdc6e Declared thin_tac
paulson
parents: 1801
diff changeset
   356
(*Deletion of an assumption*)
f2b8005bdc6e Declared thin_tac
paulson
parents: 1801
diff changeset
   357
fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
f2b8005bdc6e Declared thin_tac
paulson
parents: 1801
diff changeset
   358
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   359
(*** Applications of cut_rl ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
(*Used by metacut_tac*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
fun bires_cut_tac arg i =
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   363
    resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
(*The conclusion of the rule gets assumed in subgoal i,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
  while subgoal i+1,... are the premises of the rule.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
fun metacut_tac rule = bires_cut_tac [(false,rule)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
(*Recognizes theorems that are not rules, but simple propositions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
fun is_fact rl =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
    case prems_of rl of
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   372
        [] => true  |  _::_ => false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
13650
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13559
diff changeset
   374
(*"Cut" a list of rules into the goal.  Their premises will become new
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13559
diff changeset
   375
  subgoals.*)
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13559
diff changeset
   376
fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13559
diff changeset
   377
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13559
diff changeset
   378
(*As above, but inserts only facts (unconditional theorems);
31bd2a8cdbe2 fixing the cut_tac method to work when there are no instantiations and the
paulson
parents: 13559
diff changeset
   379
  generates no additional subgoals. *)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   380
fun cut_facts_tac ths = cut_rules_tac  (List.filter is_fact ths);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   382
(*Introduce the given proposition as a lemma and subgoal*)
12847
afa356dbcb15 fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents: 12801
diff changeset
   383
fun subgoal_tac sprop =
afa356dbcb15 fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents: 12801
diff changeset
   384
  DETERM o res_inst_tac [("psi", sprop)] cut_rl THEN' SUBGOAL (fn (prop, _) =>
afa356dbcb15 fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents: 12801
diff changeset
   385
    let val concl' = Logic.strip_assums_concl prop in
4178
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   386
      if null (term_tvars concl') then ()
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   387
      else warning"Type variables in new subgoal: add a type constraint?";
12847
afa356dbcb15 fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents: 12801
diff changeset
   388
      all_tac
afa356dbcb15 fixed subgoal_tac; fails on non-existent subgoal;
wenzelm
parents: 12801
diff changeset
   389
  end);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   390
439
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
   391
(*Introduce a list of lemmas and subgoals*)
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
   392
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
   393
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   394
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   395
(**** Indexing and filtering of theorems ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   396
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   397
(*Returns the list of potentially resolvable theorems for the goal "prem",
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   398
        using the predicate  could(subgoal,concl).
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
  Resulting list is no longer than "limit"*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   400
fun filter_thms could (limit, prem, ths) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   401
  let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   402
      fun filtr (limit, []) = []
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   403
        | filtr (limit, th::ths) =
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   404
            if limit=0 then  []
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   405
            else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   406
            else filtr(limit,ths)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
  in  filtr(limit,ths)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
(*** biresolution and resolution using nets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   411
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   412
(** To preserve the order of the rules, tag them with increasing integers **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   413
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
(*insert tags*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   415
fun taglist k [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   416
  | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   417
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
(*remove tags and suppress duplicates -- list is assumed sorted!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
fun untaglist [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
  | untaglist [(k:int,x)] = [x]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   421
  | untaglist ((k,x) :: (rest as (k',x')::_)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   422
      if k=k' then untaglist rest
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   423
      else    x :: untaglist rest;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   424
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
(*return list elements in original order*)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   426
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
(*insert one tagged brl into the pair of nets*)
12320
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
   429
fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
   430
  if eres then
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
   431
    (case try Thm.major_prem_of th of
16809
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   432
      SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   433
    | NONE => error "insert_tagged_brl: elimination rule with no premises")
16809
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   434
  else (Net.insert_term (K false) (concl_of th, kbrl) inet, enet);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
(*build a pair of nets for biresolution*)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   437
fun build_netpair netpair brls =
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   438
    foldr insert_tagged_brl netpair (taglist 1 brls);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
12320
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
   440
(*delete one kbrl from the pair of nets*)
16809
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   441
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   442
12320
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
   443
fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
13925
761af5c2fd59 catches exception DELETE
paulson
parents: 13650
diff changeset
   444
  (if eres then
12320
6e70d870ddf0 general type of delete_tagged_brl;
wenzelm
parents: 12262
diff changeset
   445
    (case try Thm.major_prem_of th of
16809
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   446
      SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   447
    | NONE => (inet, enet))  (*no major premise: ignore*)
16809
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   448
  else (Net.delete_term eq_kbrl (Thm.concl_of th, ((), brl)) inet, enet))
13925
761af5c2fd59 catches exception DELETE
paulson
parents: 13650
diff changeset
   449
  handle Net.DELETE => (inet,enet);
1801
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   450
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   451
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   452
(*biresolution using a pair of nets rather than rules.
3706
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   453
    function "order" must sort and possibly filter the list of brls.
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   454
    boolean "match" indicates matching or unification.*)
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   455
fun biresolution_from_nets_tac order match (inet,enet) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
  SUBGOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
    (fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
      let val hyps = Logic.strip_assums_hyp prem
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   459
          and concl = Logic.strip_assums_concl prem
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
          val kbrls = Net.unify_term inet concl @
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2580
diff changeset
   461
                      List.concat (map (Net.unify_term enet) hyps)
3706
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   462
      in PRIMSEQ (biresolution match (order kbrls) i) end);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
3706
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   464
(*versions taking pre-built nets.  No filtering of brls*)
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   465
val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   466
val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   467
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
(*fast versions using nets internally*)
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   469
val net_biresolve_tac =
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   470
    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
   471
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   472
val net_bimatch_tac =
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   473
    bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   475
(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   476
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
(*insert one tagged rl into the net*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   478
fun insert_krl (krl as (k,th), net) =
16809
8ca51a846576 export eq_brl;
wenzelm
parents: 16666
diff changeset
   479
    Net.insert_term (K false) (concl_of th, krl) net;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   480
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   481
(*build a net of rules for resolution*)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   482
fun build_net rls =
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   483
    foldr insert_krl Net.empty (taglist 1 rls);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   484
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   485
(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   486
fun filt_resolution_from_net_tac match pred net =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   487
  SUBGOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   488
    (fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   489
      let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   490
      in
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   491
         if pred krls
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   492
         then PRIMSEQ
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   493
                (biresolution match (map (pair false) (orderlist krls)) i)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
         else no_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   495
      end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   497
(*Resolve the subgoal using the rules (making a net) unless too flexible,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   498
   which means more than maxr rules are unifiable.      *)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   499
fun filt_resolve_tac rules maxr =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   500
    let fun pred krls = length krls <= maxr
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   501
    in  filt_resolution_from_net_tac false pred (build_net rules)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   502
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   503
(*versions taking pre-built nets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   504
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   505
val match_from_net_tac = filt_resolution_from_net_tac true (K true);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   506
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   507
(*fast versions using nets internally*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   508
val net_resolve_tac = resolve_from_net_tac o build_net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   509
val net_match_tac = match_from_net_tac o build_net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   510
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   511
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   512
(*** For Natural Deduction using (bires_flg, rule) pairs ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   513
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   514
(*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
   515
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
   516
  | subgoals_of_brl (false,rule) = nprems_of rule;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   517
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   518
(*Less-than test: for sorting to minimize number of new subgoals*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   520
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   521
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   522
(*** Meta-Rewriting Tactics ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   523
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   524
val simple_prover =
15021
6012f983a79f got rid of obsolete meta_simpset;
wenzelm
parents: 15011
diff changeset
   525
  SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   526
11768
48bc55f43774 unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents: 11762
diff changeset
   527
val rewrite = MetaSimplifier.rewrite_aux simple_prover;
48bc55f43774 unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents: 11762
diff changeset
   528
val simplify = MetaSimplifier.simplify_aux simple_prover;
48bc55f43774 unified rewrite/rewrite_cterm/simplify interface;
wenzelm
parents: 11762
diff changeset
   529
val rewrite_rule = simplify true;
10415
e6d7b77a0574 moved rewriting functions from Drule to MetaSimplifier
berghofe
parents: 10347
diff changeset
   530
val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   531
17968
d50f08d9aabb moved norm_hhf_rule, prove etc. to goal.ML;
wenzelm
parents: 17892
diff changeset
   532
(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
d50f08d9aabb moved norm_hhf_rule, prove etc. to goal.ML;
wenzelm
parents: 17892
diff changeset
   533
fun asm_rewrite_goal_tac mode prover_tac ss =
d50f08d9aabb moved norm_hhf_rule, prove etc. to goal.ML;
wenzelm
parents: 17892
diff changeset
   534
  SELECT_GOAL
d50f08d9aabb moved norm_hhf_rule, prove etc. to goal.ML;
wenzelm
parents: 17892
diff changeset
   535
    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
d50f08d9aabb moved norm_hhf_rule, prove etc. to goal.ML;
wenzelm
parents: 17892
diff changeset
   536
10444
2dfa19236768 added rewrite_goal_tac;
wenzelm
parents: 10415
diff changeset
   537
fun rewrite_goal_tac rews =
17892
62c397c17d18 Simplifier.theory_context;
wenzelm
parents: 17851
diff changeset
   538
  let val ss = MetaSimplifier.empty_ss addsimps rews in
17968
d50f08d9aabb moved norm_hhf_rule, prove etc. to goal.ML;
wenzelm
parents: 17892
diff changeset
   539
    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
17892
62c397c17d18 Simplifier.theory_context;
wenzelm
parents: 17851
diff changeset
   540
      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
62c397c17d18 Simplifier.theory_context;
wenzelm
parents: 17851
diff changeset
   541
  end;
10444
2dfa19236768 added rewrite_goal_tac;
wenzelm
parents: 10415
diff changeset
   542
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   543
(*Rewrite throughout proof state. *)
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   544
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   545
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   546
(*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
   547
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   548
fun rewtac def = rewrite_goals_tac [def];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
12782
a4183c50ae5f tune norm_hhf_tac;
wenzelm
parents: 12725
diff changeset
   550
val norm_hhf_tac =
a4183c50ae5f tune norm_hhf_tac;
wenzelm
parents: 12725
diff changeset
   551
  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
a4183c50ae5f tune norm_hhf_tac;
wenzelm
parents: 12725
diff changeset
   552
  THEN' SUBGOAL (fn (t, i) =>
12801
a94cef8982cc renamed norm_hhf to norm_hhf_rule;
wenzelm
parents: 12782
diff changeset
   553
    if Drule.is_norm_hhf t then all_tac
12782
a4183c50ae5f tune norm_hhf_tac;
wenzelm
parents: 12725
diff changeset
   554
    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
10805
89a29437cebc added norm_hhf(_tac);
wenzelm
parents: 10444
diff changeset
   555
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   556
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   557
(*** for folding definitions, handling critical pairs ***)
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   558
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   559
(*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
   560
fun term_depth (Abs(a,T,t)) = 1 + term_depth t
2145
5e8db0bc195e asm_rewrite_goal_tac now calls SELECT_GOAL.
paulson
parents: 2043
diff changeset
   561
  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   562
  | term_depth _ = 0;
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   563
12801
a94cef8982cc renamed norm_hhf to norm_hhf_rule;
wenzelm
parents: 12782
diff changeset
   564
val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   565
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   566
(*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
   567
  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
   568
fun sort_lhs_depths defs =
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17271
diff changeset
   569
  let val keylist = AList.make (term_depth o lhs_of_thm) defs
4438
ecfeff48bf0c adapted to new sort function;
wenzelm
parents: 4270
diff changeset
   570
      val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17271
diff changeset
   571
  in map (AList.find (op =) keylist) keys end;
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   572
7596
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
   573
val rev_defs = sort_lhs_depths o map symmetric;
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   574
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   575
fun fold_rule defs thm = Library.foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
7596
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
   576
fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
   577
fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   578
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   579
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   580
(*** Renaming of parameters in a subgoal
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   581
     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
   582
     separated by blanks ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   583
9535
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   584
fun rename_params_tac xs i =
14673
3d760a971fde use Syntax.is_identifier;
wenzelm
parents: 13925
diff changeset
   585
  case Library.find_first (not o Syntax.is_identifier) xs of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   586
      SOME x => error ("Not an identifier: " ^ x)
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   587
    | NONE =>
13559
51c3ac47d127 added checking so that (rename_tac "x y") is rejected, since
paulson
parents: 13105
diff changeset
   588
       (if !Logic.auto_rename
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   589
         then (warning "Resetting Logic.auto_rename";
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   590
             Logic.auto_rename := false)
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   591
        else (); PRIMITIVE (rename_params_rule (xs, i)));
9535
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   592
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   593
fun rename_tac str i =
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   594
  let val cs = Symbol.explode str in
4693
2e47ea2c6109 adapted to baroque chars;
wenzelm
parents: 4611
diff changeset
   595
  case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
9535
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   596
      [] => rename_params_tac (scanwords Symbol.is_letdig cs) i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   597
    | c::_ => error ("Illegal character: " ^ c)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   598
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   599
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   600
(*Rename recent parameters using names generated from a and the suffixes,
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   601
  provided the string a, which represents a term, is an identifier. *)
10817
083d4a6734b4 tuned norm_hhf(_tac);
wenzelm
parents: 10805
diff changeset
   602
fun rename_last_tac a sufs i =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   603
  let val names = map (curry op^ a) sufs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   604
  in  if Syntax.is_identifier a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   605
      then PRIMITIVE (rename_params_rule (names,i))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   606
      else all_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   607
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   608
2043
8de7a0ab463b prune_params_tac no longer rewrites main goal
paulson
parents: 2029
diff changeset
   609
(*Prunes all redundant parameters from the proof state by rewriting.
8de7a0ab463b prune_params_tac no longer rewrites main goal
paulson
parents: 2029
diff changeset
   610
  DOES NOT rewrite main goal, where quantification over an unused bound
8de7a0ab463b prune_params_tac no longer rewrites main goal
paulson
parents: 2029
diff changeset
   611
    variable is sometimes done to avoid the need for cut_facts_tac.*)
8de7a0ab463b prune_params_tac no longer rewrites main goal
paulson
parents: 2029
diff changeset
   612
val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   613
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   614
(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   615
  right to left if n is positive, and from left to right if n is negative.*)
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2580
diff changeset
   616
fun rotate_tac 0 i = all_tac
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2580
diff changeset
   617
  | rotate_tac k i = PRIMITIVE (rotate_rule k i);
1209
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   618
7248
322151fe6f02 new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents: 6979
diff changeset
   619
(*Rotates the given subgoal to be the last.*)
322151fe6f02 new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents: 6979
diff changeset
   620
fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
322151fe6f02 new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents: 6979
diff changeset
   621
5974
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   622
(* remove premises that do not satisfy p; fails if all prems satisfy p *)
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   623
fun filter_prems_tac p =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   624
  let fun Then NONE tac = SOME tac
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   625
        | Then (SOME tac) tac' = SOME(tac THEN' tac');
5974
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   626
      fun thins ((tac,n),H) =
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   627
        if p H then (tac,n+1)
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   628
        else (Then tac (rotate_tac n THEN' etac thin_rl),0);
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   629
  in SUBGOAL(fn (subg,n) =>
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   630
       let val Hs = Logic.strip_assums_hyp subg
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   631
       in case fst(Library.foldl thins ((NONE,0),Hs)) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15464
diff changeset
   632
            NONE => no_tac | SOME tac => tac n
5974
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   633
       end)
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   634
  end;
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   635
11961
e5911a25d094 prove: primitive goal interface for internal use;
wenzelm
parents: 11929
diff changeset
   636
18471
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   637
(* meta-level conjunction *)
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   638
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   639
val conj_tac = SUBGOAL (fn (goal, i) =>
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   640
  if can Logic.dest_conjunction goal then
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   641
    (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   642
  else no_tac);
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   643
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   644
val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
16425
2427be27cc60 accomodate identification of type Sign.sg and theory;
wenzelm
parents: 16325
diff changeset
   645
18471
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   646
val precise_conjunction_tac =
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   647
  let
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   648
    fun tac 0 i = eq_assume_tac i
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   649
      | tac 1 i = SUBGOAL (K all_tac) i
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   650
      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   651
  in TRY oo tac end;
12139
d51d50636332 added conjunction_tac;
wenzelm
parents: 11974
diff changeset
   652
18500
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   653
fun CONJUNCTS tac =
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   654
  SELECT_GOAL (conjunction_tac 1
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   655
    THEN tac
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   656
    THEN PRIMITIVE Drule.conj_curry);
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   657
8b1a4e8ed199 CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
wenzelm
parents: 18471
diff changeset
   658
fun PRECISE_CONJUNCTS n tac =
18471
ca9a864018d6 conjunction_tac: single goal;
wenzelm
parents: 18209
diff changeset
   659
  SELECT_GOAL (precise_conjunction_tac n 1
18209
6bcd9b2ca49b added CONJUNCTS: treat conjunction as separate sub-goals;
wenzelm
parents: 18145
diff changeset
   660
    THEN tac
6bcd9b2ca49b added CONJUNCTS: treat conjunction as separate sub-goals;
wenzelm
parents: 18145
diff changeset
   661
    THEN PRIMITIVE Drule.conj_curry);
6bcd9b2ca49b added CONJUNCTS: treat conjunction as separate sub-goals;
wenzelm
parents: 18145
diff changeset
   662
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   663
end;
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   664
11774
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   665
structure BasicTactic: BASIC_TACTIC = Tactic;
3bc4f67d7fe1 qualify some names;
wenzelm
parents: 11768
diff changeset
   666
open BasicTactic;