src/Pure/tactic.ML
author wenzelm
Fri, 04 Aug 2000 22:59:08 +0200
changeset 9535 a60b0be5ee96
parent 8977 dd8bc754a072
child 10347 c0cfc4ac12e2
permissions -rw-r--r--
added rename_params_tac;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
     1
(*  Title: 	Pure/tactic.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
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
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 =
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    10
  sig
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    11
  val ares_tac		: thm list -> int -> tactic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  val asm_rewrite_goal_tac:
4713
bea2ab2e360b New simplifier flag for mutual simplification.
nipkow
parents: 4693
diff changeset
    13
    bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    14
  val assume_tac	: int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    15
  val atac	: int ->tactic
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    16
  val bimatch_from_nets_tac: 
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    17
      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    18
  val bimatch_tac	: (bool*thm)list -> int -> tactic
3706
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
    19
  val biresolution_from_nets_tac: 
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
    20
	('a list -> (bool * thm) list) ->
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
    21
	bool -> 'a Net.net * 'a Net.net -> int -> tactic
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
    22
  val biresolve_from_nets_tac: 
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    23
      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    24
  val biresolve_tac	: (bool*thm)list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    25
  val build_net	: thm list -> (int*thm) Net.net
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    26
  val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
    27
      (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    28
  val compose_inst_tac	: (string*string)list -> (bool*thm*int) -> 
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    29
                          int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    30
  val compose_tac	: (bool * thm * int) -> int -> tactic 
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    31
  val cut_facts_tac	: thm list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    32
  val cut_inst_tac	: (string*string)list -> thm -> int -> tactic   
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
    33
  val datac             : thm -> int -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    34
  val defer_tac 	: int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    35
  val distinct_subgoals_tac	: tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    36
  val dmatch_tac	: thm list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    37
  val dresolve_tac	: thm list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    38
  val dres_inst_tac	: (string*string)list -> thm -> int -> tactic   
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    39
  val dtac		: thm -> int ->tactic
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
    40
  val eatac             : thm -> int -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    41
  val etac		: thm -> int ->tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    42
  val eq_assume_tac	: int -> tactic   
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    43
  val ematch_tac	: thm list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    44
  val eresolve_tac	: thm list -> int -> tactic
5974
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
    45
  val eres_inst_tac	: (string*string)list -> thm -> int -> tactic
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
    46
  val fatac             : thm -> int -> int -> tactic
5974
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
    47
  val filter_prems_tac  : (term -> bool) -> int -> tactic  
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    48
  val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    49
  val filt_resolve_tac	: thm list -> int -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    50
  val flexflex_tac	: tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    51
  val fold_goals_tac	: thm list -> tactic
7596
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
    52
  val fold_rule		: thm list -> thm -> thm
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    53
  val fold_tac		: thm list -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    54
  val forward_tac	: thm list -> int -> tactic   
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    55
  val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
    56
  val ftac		: thm -> int ->tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    57
  val insert_tagged_brl : ('a*(bool*thm)) * 
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    58
                          (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    59
                          ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    60
  val delete_tagged_brl	: (bool*thm) * 
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    61
                         ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
1801
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
    62
                    (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    63
  val is_fact		: thm -> bool
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    64
  val lessb		: (bool * thm) * (bool * thm) -> bool
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    65
  val lift_inst_rule	: thm * int * (string*string)list * thm -> thm
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    66
  val make_elim		: thm -> thm
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    67
  val match_from_net_tac	: (int*thm) Net.net -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    68
  val match_tac	: thm list -> int -> tactic
5838
a4122945d638 added metacuts_tac;
wenzelm
parents: 5263
diff changeset
    69
  val metacut_tac	: thm -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    70
  val net_bimatch_tac	: (bool*thm) list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    71
  val net_biresolve_tac	: (bool*thm) list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    72
  val net_match_tac	: thm list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    73
  val net_resolve_tac	: thm list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    74
  val orderlist		: (int * 'a) list -> 'a list
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    75
  val PRIMITIVE		: (thm -> thm) -> tactic  
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
    76
  val PRIMSEQ		: (thm -> thm Seq.seq) -> tactic  
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    77
  val prune_params_tac	: tactic
9535
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
    78
  val rename_params_tac	: string list -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    79
  val rename_tac	: string -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    80
  val rename_last_tac	: string -> string list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    81
  val resolve_from_net_tac	: (int*thm) Net.net -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    82
  val resolve_tac	: thm list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    83
  val res_inst_tac	: (string*string)list -> thm -> int -> tactic   
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
    84
  val rewrite_goals_rule: thm list -> thm -> thm
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
    85
  val rewrite_rule	: thm list -> thm -> thm
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    86
  val rewrite_goals_tac	: thm list -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    87
  val rewrite_tac	: thm list -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    88
  val rewtac		: thm -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    89
  val rotate_tac	: int -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    90
  val rtac		: thm -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    91
  val rule_by_tactic	: tactic -> thm -> thm
5263
8862ed2db431 added solve_tac;
wenzelm
parents: 4713
diff changeset
    92
  val solve_tac		: thm list -> int -> tactic
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    93
  val subgoal_tac	: string -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    94
  val subgoals_tac	: string list -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    95
  val subgoals_of_brl	: bool * thm -> int
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    96
  val term_lift_inst_rule	:
1975
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
    97
      thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
    98
      -> thm
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
    99
  val thin_tac		: string -> int -> tactic
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   100
  val trace_goalno_tac	: (int -> tactic) -> int -> tactic
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   101
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   104
structure Tactic : TACTIC = 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   107
(*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   108
fun trace_goalno_tac tac i st =  
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   109
    case Seq.pull(tac i st) of
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   110
	None    => Seq.empty
5956
ab4d13e9e77a replaced prs by writeln;
wenzelm
parents: 5838
diff changeset
   111
      | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected"); 
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   112
    			 Seq.make(fn()=> seqcell));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
(*Makes a rule by applying a tactic to an existing rule*)
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   115
fun rule_by_tactic tac rl =
2688
889a1cbd1aca rule_by_tactic no longer standardizes its result
paulson
parents: 2672
diff changeset
   116
  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
   117
  in case Seq.pull (tac st)  of
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   118
	None        => raise THM("rule_by_tactic", 0, [rl])
2688
889a1cbd1aca rule_by_tactic no longer standardizes its result
paulson
parents: 2672
diff changeset
   119
      | Some(st',_) => Thm.varifyT (thaw st')
889a1cbd1aca rule_by_tactic no longer standardizes its result
paulson
parents: 2672
diff changeset
   120
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
(*** Basic tactics ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   125
fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   128
fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
(*** The following fail if the goal number is out of range:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
     thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
(*Solve subgoal i by assumption*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
fun assume_tac i = PRIMSEQ (assumption i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
(*Solve subgoal i by assumption, using no unification*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
(** Resolution/matching tactics **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
(*The composition rule/state: no lifting or var renaming.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
  The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
  like [| P&Q; P==>R |] ==> R *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*Attack subgoal i by resolution, using flags to indicate elimination rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
(*Resolution: the simple case, works for introduction rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
fun resolve_tac rules = biresolve_tac (map (pair false) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
(*Resolution with elimination rules only*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(*Forward reasoning using destruction rules.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
(*Like forward_tac, but deletes the assumption after use.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
fun dresolve_tac rls = eresolve_tac (map make_elim rls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
(*Shorthand versions: for resolution with a single theorem*)
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   165
val atac    =   assume_tac;
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   166
fun rtac rl =  resolve_tac [rl];
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   167
fun dtac rl = dresolve_tac [rl];
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   168
fun etac rl = eresolve_tac [rl];
7491
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   169
fun ftac rl =  forward_tac [rl];
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   170
fun datac thm j = EVERY' (dtac thm::replicate j atac);
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   171
fun eatac thm j = EVERY' (etac thm::replicate j atac);
95a4af0e10a7 added ftac, eatac, datac, fatac
oheimb
parents: 7248
diff changeset
   172
fun fatac thm j = EVERY' (ftac thm::replicate j atac);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
(*Use an assumption or some rules ... A popular combination!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
5263
8862ed2db431 added solve_tac;
wenzelm
parents: 4713
diff changeset
   177
fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
8862ed2db431 added solve_tac;
wenzelm
parents: 4713
diff changeset
   178
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
(*Matching tactics -- as above, but forbid updating of state*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
fun match_tac rules  = bimatch_tac (map (pair false) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
fun ematch_tac rules = bimatch_tac (map (pair true) rules);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
fun dmatch_tac rls   = ematch_tac (map make_elim rls);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(*Smash all flex-flex disagreement pairs in the proof state.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
val flexflex_tac = PRIMSEQ flexflex_rule;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   188
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   189
(*Remove duplicate subgoals.  By Mark Staples*)
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   190
local
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   191
fun cterm_aconv (a,b) = #t (rep_cterm a) aconv #t (rep_cterm b);
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   192
in
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   193
fun distinct_subgoals_tac state = 
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   194
    let val (frozth,thawfn) = freeze_thaw state
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   195
	val froz_prems = cprems_of frozth
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   196
	val assumed = implies_elim_list frozth (map assume froz_prems)
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   197
	val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   198
					assumed;
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   199
    in  Seq.single (thawfn implied)  end
3409
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   200
end; 
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   201
c0466958df5d Tidying of signature. More robust renaming in freeze_thaw.
paulson
parents: 2814
diff changeset
   202
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
(*Lift and instantiate a rule wrt the given state and subgoal number *)
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   204
fun lift_inst_rule (st, i, sinsts, rule) =
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   205
let val {maxidx,sign,...} = rep_thm st
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   206
    val (_, _, Bi, _) = dest_state(st,i)
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   207
    val params = Logic.strip_params Bi	        (*params of subgoal i*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
    val params = rev(rename_wrt_term Bi params) (*as they are printed*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
    val paramTs = map #2 params
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
    and inc = maxidx+1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
      | liftvar t = raise TERM("Variable expected", [t]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
    fun liftterm t = list_abs_free (params, 
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   214
				    Logic.incr_indexes(paramTs,inc) t)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
    (*Lifts instantiation pair over params*)
230
ec8a2b6aa8a7 Many other files modified as follows:
lcp
parents: 214
diff changeset
   216
    fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
    fun lifttvar((a,i),ctyp) =
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   218
	let val {T,sign} = rep_ctyp ctyp
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   219
	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   220
    val rts = types_sorts rule and (types,sorts) = types_sorts st
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
    fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
      | types'(ixn) = types ixn;
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 947
diff changeset
   223
    val used = add_term_tvarnames
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   224
                  (#prop(rep_thm st) $ #prop(rep_thm rule),[])
949
83c588d6fee9 Changed treatment of during type inference internally generated type
nipkow
parents: 947
diff changeset
   225
    val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
8129
29e239c7b8c2 Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents: 7596
diff changeset
   226
in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
29e239c7b8c2 Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents: 7596
diff changeset
   227
                     (lift_rule (st,i) rule)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
3984
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   230
(*
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   231
Like lift_inst_rule but takes terms, not strings, where the terms may contain
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   232
Bounds referring to parameters of the subgoal.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   233
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   234
insts: [...,(vj,tj),...]
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   235
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   236
The tj may contain references to parameters of subgoal i of the state st
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   237
in the form of Bound k, i.e. the tj may be subterms of the subgoal.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   238
To saturate the lose bound vars, the tj are enclosed in abstractions
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   239
corresponding to the parameters of subgoal i, thus turning them into
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   240
functions. At the same time, the types of the vj are lifted.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   241
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   242
NB: the types in insts must be correctly instantiated already,
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   243
    i.e. Tinsts is not applied to insts.
8fc76a487616 Modified comment.
nipkow
parents: 3706
diff changeset
   244
*)
1975
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
   245
fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
1966
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   246
let val {maxidx,sign,...} = rep_thm st
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   247
    val (_, _, Bi, _) = dest_state(st,i)
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   248
    val params = Logic.strip_params Bi          (*params of subgoal i*)
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   249
    val paramTs = map #2 params
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   250
    and inc = maxidx+1
1975
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
   251
    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
   252
    (*lift only Var, not term, which must be lifted already*)
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
   253
    fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
eec67972b1bf renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
nipkow
parents: 1966
diff changeset
   254
    fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
8129
29e239c7b8c2 Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents: 7596
diff changeset
   255
in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
29e239c7b8c2 Thm.instantiate no longer normalizes, but Drule.instantiate does
paulson
parents: 7596
diff changeset
   256
                     (lift_rule (st,i) rule)
1966
9e626f86e335 added cterm_lift_inst_rule
nipkow
parents: 1955
diff changeset
   257
end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
(*** Resolve after lifting and instantation; may refer to parameters of the
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
     subgoal.  Fails if "i" is out of range.  ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
(*compose version: arguments are as for bicompose.*)
8977
dd8bc754a072 res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents: 8129
diff changeset
   263
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = 
dd8bc754a072 res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents: 8129
diff changeset
   264
  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
   265
  else st |>
dd8bc754a072 res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents: 8129
diff changeset
   266
    (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
dd8bc754a072 res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents: 8129
diff changeset
   267
     handle TERM (msg,_)   => (writeln msg;  no_tac)
dd8bc754a072 res_inst_tac, etc., no longer print the "dest_state" message when the selected
paulson
parents: 8129
diff changeset
   268
	  | THM  (msg,_,_) => (writeln msg;  no_tac));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
761
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   270
(*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   271
  terms that are substituted contain (term or type) unknowns from the
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   272
  goal, because it is unable to instantiate goal unknowns at the same time.
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   273
2029
2fa4c4b1a7fe Generalized freeze to freeze_thaw in order to
paulson
parents: 1975
diff changeset
   274
  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
   275
  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
   276
  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
   277
  goals.
761
04320c295500 res_inst_tac: added comments
lcp
parents: 670
diff changeset
   278
*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
fun res_inst_tac sinsts rule i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
    compose_inst_tac sinsts (false, rule, nprems_of rule) i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   282
(*eresolve elimination version*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
fun eres_inst_tac sinsts rule i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
    compose_inst_tac sinsts (true, rule, nprems_of rule) i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   286
(*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
   287
  increment revcut_rl instead.*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
fun make_elim_preserve rl = 
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   289
  let val {maxidx,...} = rep_thm rl
6390
5d58c100ca3f qualify Theory.sign_of etc.;
wenzelm
parents: 5974
diff changeset
   290
      fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT));
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   291
      val revcut_rl' = 
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   292
	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   293
			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
      val arg = (false, rl, nprems_of rl)
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   295
      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
  in  th  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
  handle Bind => raise THM("make_elim_preserve", 1, [rl]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   299
(*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
   300
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   302
(*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
   303
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
   304
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   305
(*dresolve tactic applies a RULE to replace an assumption*)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
1951
f2b8005bdc6e Declared thin_tac
paulson
parents: 1801
diff changeset
   308
(*Deletion of an assumption*)
f2b8005bdc6e Declared thin_tac
paulson
parents: 1801
diff changeset
   309
fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
f2b8005bdc6e Declared thin_tac
paulson
parents: 1801
diff changeset
   310
270
d506ea00c825 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents: 230
diff changeset
   311
(*** Applications of cut_rl ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
(*Used by metacut_tac*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
fun bires_cut_tac arg i =
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   315
    resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   316
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
(*The conclusion of the rule gets assumed in subgoal i,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
  while subgoal i+1,... are the premises of the rule.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
fun metacut_tac rule = bires_cut_tac [(false,rule)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
(*Recognizes theorems that are not rules, but simple propositions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   322
fun is_fact rl =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
    case prems_of rl of
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   324
	[] => true  |  _::_ => false;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   326
(*"Cut" all facts from theorem list into the goal as assumptions. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
fun cut_facts_tac ths i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
    EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
(*Introduce the given proposition as a lemma and subgoal*)
4178
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   331
fun subgoal_tac sprop i st = 
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   332
  let val st'    = Seq.hd (res_inst_tac [("psi", sprop)] cut_rl i st)
4178
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   333
      val concl' = Logic.strip_assums_concl (List.nth(prems_of st', i))
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   334
  in  
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   335
      if null (term_tvars concl') then ()
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   336
      else warning"Type variables in new subgoal: add a type constraint?";
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   337
      Seq.single st'
4178
e64ff1c1bc70 subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents: 3991
diff changeset
   338
  end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
439
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
   340
(*Introduce a list of lemmas and subgoals*)
ad3f46c13f1e Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
lcp
parents: 270
diff changeset
   341
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
   342
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   343
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   344
(**** Indexing and filtering of theorems ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   345
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   346
(*Returns the list of potentially resolvable theorems for the goal "prem",
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   347
	using the predicate  could(subgoal,concl).
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   348
  Resulting list is no longer than "limit"*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   349
fun filter_thms could (limit, prem, ths) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   350
  let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   351
      fun filtr (limit, []) = []
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   352
	| filtr (limit, th::ths) =
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   353
	    if limit=0 then  []
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   354
	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   355
	    else filtr(limit,ths)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   356
  in  filtr(limit,ths)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   357
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   358
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   359
(*** biresolution and resolution using nets ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   360
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   361
(** To preserve the order of the rules, tag them with increasing integers **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   362
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   363
(*insert tags*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   364
fun taglist k [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   365
  | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   366
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   367
(*remove tags and suppress duplicates -- list is assumed sorted!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   368
fun untaglist [] = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   369
  | untaglist [(k:int,x)] = [x]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   370
  | untaglist ((k,x) :: (rest as (k',x')::_)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
      if k=k' then untaglist rest
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
      else    x :: untaglist rest;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
(*return list elements in original order*)
4438
ecfeff48bf0c adapted to new sort function;
wenzelm
parents: 4270
diff changeset
   375
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls); 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
(*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
   378
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
    if eres then 
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   380
	case prems_of th of
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   381
	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   382
	  | [] => error"insert_tagged_brl: elimination rule with no premises"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
    else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   385
(*build a pair of nets for biresolution*)
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   386
fun build_netpair netpair brls = 
1077
c2df11ae8b55 Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents: 952
diff changeset
   387
    foldr insert_tagged_brl (taglist 1 brls, netpair);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
1801
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   389
(*delete one kbrl from the pair of nets;
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   390
  we don't know the value of k, so we use 0 and ignore it in the comparison*)
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   391
local
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   392
  fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   393
in
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   394
fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   395
    if eres then 
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   396
	case prems_of th of
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   397
	    prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
2814
a318f7f3a65c delete_tagged_brl just ignores non-elimination rules instead of complaining
paulson
parents: 2688
diff changeset
   398
	  | []      => (inet,enet)     (*no major premise: ignore*)
1801
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   399
    else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   400
end;
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   401
927a31ba4346 Added delete function for brls
paulson
parents: 1501
diff changeset
   402
3706
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   403
(*biresolution using a pair of nets rather than rules.  
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   404
    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
   405
    boolean "match" indicates matching or unification.*)
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   406
fun biresolution_from_nets_tac order match (inet,enet) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   407
  SUBGOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   408
    (fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   409
      let val hyps = Logic.strip_assums_hyp prem
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   410
          and concl = Logic.strip_assums_concl prem 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   411
          val kbrls = Net.unify_term inet concl @
2672
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2580
diff changeset
   412
                      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
   413
      in PRIMSEQ (biresolution match (order kbrls) i) end);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   414
3706
e57b5902822f Generalized and exported biresolution_from_nets_tac to allow the declaration
paulson
parents: 3575
diff changeset
   415
(*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
   416
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
   417
val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   419
(*fast versions using nets internally*)
670
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   420
val net_biresolve_tac =
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   421
    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
   422
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   423
val net_bimatch_tac =
ff4c6691de9d Pure/tactic/build_netpair: now takes two arguments
lcp
parents: 439
diff changeset
   424
    bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   426
(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
(*insert one tagged rl into the net*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   429
fun insert_krl (krl as (k,th), net) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
    Net.insert_term ((concl_of th, krl), net, K false);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   432
(*build a net of rules for resolution*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
fun build_net rls = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   434
    foldr insert_krl (taglist 1 rls, Net.empty);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   435
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   437
fun filt_resolution_from_net_tac match pred net =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
  SUBGOAL
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
    (fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   440
      let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
      in 
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   442
	 if pred krls  
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
         then PRIMSEQ
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   444
		(biresolution match (map (pair false) (orderlist krls)) i)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
         else no_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   446
      end);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   448
(*Resolve the subgoal using the rules (making a net) unless too flexible,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   449
   which means more than maxr rules are unifiable.      *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   450
fun filt_resolve_tac rules maxr = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   451
    let fun pred krls = length krls <= maxr
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   452
    in  filt_resolution_from_net_tac false pred (build_net rules)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
(*versions taking pre-built nets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   455
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
val match_from_net_tac = filt_resolution_from_net_tac true (K true);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   457
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
(*fast versions using nets internally*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
val net_resolve_tac = resolve_from_net_tac o build_net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
val net_match_tac = match_from_net_tac o build_net;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   461
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   463
(*** For Natural Deduction using (bires_flg, rule) pairs ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
(*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
   466
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
   467
  | subgoals_of_brl (false,rule) = nprems_of rule;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   468
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
(*Less-than test: for sorting to minimize number of new subgoals*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   470
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   471
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   472
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   473
(*** Meta-Rewriting Tactics ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   474
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   475
fun result1 tacf mss thm =
4270
957c887b89b5 changed Sequence interface (now Seq, in seq.ML);
wenzelm
parents: 4213
diff changeset
   476
  apsome fst (Seq.pull (tacf mss thm));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
3575
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   478
val simple_prover =
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   479
  result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   480
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   481
val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   482
val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   483
4e9beacb5339 improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents: 3554
diff changeset
   484
2145
5e8db0bc195e asm_rewrite_goal_tac now calls SELECT_GOAL.
paulson
parents: 2043
diff changeset
   485
(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
5e8db0bc195e asm_rewrite_goal_tac now calls SELECT_GOAL.
paulson
parents: 2043
diff changeset
   486
fun asm_rewrite_goal_tac mode prover_tac mss =
5e8db0bc195e asm_rewrite_goal_tac now calls SELECT_GOAL.
paulson
parents: 2043
diff changeset
   487
      SELECT_GOAL 
5e8db0bc195e asm_rewrite_goal_tac now calls SELECT_GOAL.
paulson
parents: 2043
diff changeset
   488
        (PRIMITIVE
5e8db0bc195e asm_rewrite_goal_tac now calls SELECT_GOAL.
paulson
parents: 2043
diff changeset
   489
	   (rewrite_goal_rule mode (result1 prover_tac) mss 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   490
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   491
(*Rewrite throughout proof state. *)
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   492
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   493
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   494
(*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
   495
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   496
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
   497
fun rewtac def = rewrite_goals_tac [def];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   498
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   499
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   500
(*** 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
   501
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   502
(*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
   503
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
   504
  | 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
   505
  | term_depth _ = 0;
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   506
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   507
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
   508
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   509
(*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
   510
  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
   511
fun sort_lhs_depths defs =
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   512
  let val keylist = make_keylist (term_depth o lhs_of_thm) defs
4438
ecfeff48bf0c adapted to new sort function;
wenzelm
parents: 4270
diff changeset
   513
      val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
69
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   514
  in  map (keyfilter keylist) keys  end;
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   515
7596
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
   516
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
   517
7596
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
   518
fun fold_rule defs thm = foldl (fn (th, ds) => rewrite_rule ds th) (thm, rev_defs defs);
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
   519
fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
c97c3ad15d2e added fold_rule;
wenzelm
parents: 7491
diff changeset
   520
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
   521
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   522
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   523
(*** Renaming of parameters in a subgoal
e7588b53d6b0 tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents: 0
diff changeset
   524
     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
   525
     separated by blanks ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   526
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   527
(*Calling this will generate the warning "Same as previous level" since
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   528
  it affects nothing but the names of bound variables!*)
9535
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   529
fun rename_params_tac xs i =
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   530
  (if !Logic.auto_rename
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   531
    then (warning "Resetting Logic.auto_rename"; 
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   532
	Logic.auto_rename := false)
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   533
   else (); PRIMITIVE (rename_params_rule (xs, i)));
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   534
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
fun rename_tac str i = 
9535
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   536
  let val cs = Symbol.explode str in  
4693
2e47ea2c6109 adapted to baroque chars;
wenzelm
parents: 4611
diff changeset
   537
  case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
9535
a60b0be5ee96 added rename_params_tac;
wenzelm
parents: 8977
diff changeset
   538
      [] => rename_params_tac (scanwords Symbol.is_letdig cs) i
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   539
    | c::_ => error ("Illegal character: " ^ c)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   540
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   541
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   542
(*Rename recent parameters using names generated from a and the suffixes,
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   543
  provided the string a, which represents a term, is an identifier. *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   544
fun rename_last_tac a sufs i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   545
  let val names = map (curry op^ a) sufs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   546
  in  if Syntax.is_identifier a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   547
      then PRIMITIVE (rename_params_rule (names,i))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   548
      else all_tac
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   549
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   550
2043
8de7a0ab463b prune_params_tac no longer rewrites main goal
paulson
parents: 2029
diff changeset
   551
(*Prunes all redundant parameters from the proof state by rewriting.
8de7a0ab463b prune_params_tac no longer rewrites main goal
paulson
parents: 2029
diff changeset
   552
  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
   553
    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
   554
val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   555
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   556
(*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
   557
  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
   558
fun rotate_tac 0 i = all_tac
85d7e800d754 Replaced "flat" by the Basis Library function List.concat
paulson
parents: 2580
diff changeset
   559
  | rotate_tac k i = PRIMITIVE (rotate_rule k i);
1209
03dc596b3a18 added rotate_tac.
nipkow
parents: 1077
diff changeset
   560
7248
322151fe6f02 new primitive rule permute_prems to underlie defer_tac and rotate_prems
paulson
parents: 6979
diff changeset
   561
(*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
   562
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
   563
5974
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   564
(* remove premises that do not satisfy p; fails if all prems satisfy p *)
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   565
fun filter_prems_tac p =
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   566
  let fun Then None tac = Some tac
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   567
        | Then (Some tac) tac' = Some(tac THEN' tac');
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   568
      fun thins ((tac,n),H) =
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   569
        if p H then (tac,n+1)
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   570
        else (Then tac (rotate_tac n THEN' etac thin_rl),0);
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   571
  in SUBGOAL(fn (subg,n) =>
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   572
       let val Hs = Logic.strip_assums_hyp subg
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   573
       in case fst(foldl thins ((None,0),Hs)) of
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   574
            None => no_tac | Some tac => tac n
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   575
       end)
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   576
  end;
6acf3ff0f486 Added filter_prems_tac
nipkow
parents: 5956
diff changeset
   577
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   578
end;
1501
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   579
bb7f99a0a6f0 Elimination of fully-functorial style.
paulson
parents: 1460
diff changeset
   580
open Tactic;