src/Pure/tactic.ML
changeset 23223 7791128b39a9
parent 23178 07ba6b58b3d2
child 23492 60cf5cf30b81
     1.1 --- a/src/Pure/tactic.ML	Sun Jun 03 23:16:50 2007 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sun Jun 03 23:16:51 2007 +0200
     1.3 @@ -8,100 +8,96 @@
     1.4  
     1.5  signature BASIC_TACTIC =
     1.6  sig
     1.7 -  val ares_tac          : thm list -> int -> tactic
     1.8 -  val assume_tac        : int -> tactic
     1.9 -  val atac      : int ->tactic
    1.10 -  val bimatch_from_nets_tac:
    1.11 -      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    1.12 -  val bimatch_tac       : (bool*thm)list -> int -> tactic
    1.13 -  val biresolution_from_nets_tac:
    1.14 -        ('a list -> (bool * thm) list) ->
    1.15 -        bool -> 'a Net.net * 'a Net.net -> int -> tactic
    1.16 -  val biresolve_from_nets_tac:
    1.17 -      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    1.18 -  val biresolve_tac     : (bool*thm)list -> int -> tactic
    1.19 -  val build_net : thm list -> (int*thm) Net.net
    1.20 -  val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
    1.21 -      (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
    1.22 -  val compose_inst_tac  : (string*string)list -> (bool*thm*int) ->
    1.23 -                          int -> tactic
    1.24 -  val compose_tac       : (bool * thm * int) -> int -> tactic
    1.25 -  val cut_facts_tac     : thm list -> int -> tactic
    1.26 -  val cut_rules_tac     : thm list -> int -> tactic
    1.27 -  val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
    1.28 -  val datac             : thm -> int -> int -> tactic
    1.29 -  val defer_tac         : int -> tactic
    1.30 -  val distinct_subgoal_tac      : int -> tactic
    1.31 -  val distinct_subgoals_tac     : tactic
    1.32 -  val dmatch_tac        : thm list -> int -> tactic
    1.33 -  val dresolve_tac      : thm list -> int -> tactic
    1.34 -  val dres_inst_tac     : (string*string)list -> thm -> int -> tactic
    1.35 -  val dtac              : thm -> int ->tactic
    1.36 -  val eatac             : thm -> int -> int -> tactic
    1.37 -  val etac              : thm -> int ->tactic
    1.38 -  val eq_assume_tac     : int -> tactic
    1.39 -  val ematch_tac        : thm list -> int -> tactic
    1.40 -  val eresolve_tac      : thm list -> int -> tactic
    1.41 -  val eres_inst_tac     : (string*string)list -> thm -> int -> tactic
    1.42 -  val fatac             : thm -> int -> int -> tactic
    1.43 -  val filter_prems_tac  : (term -> bool) -> int -> tactic
    1.44 -  val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
    1.45 -  val filt_resolve_tac  : thm list -> int -> int -> tactic
    1.46 -  val flexflex_tac      : tactic
    1.47 -  val forward_tac       : thm list -> int -> tactic
    1.48 -  val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
    1.49 -  val ftac              : thm -> int ->tactic
    1.50 -  val insert_tagged_brl : 'a * (bool * thm) ->
    1.51 -    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    1.52 -      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.53 -  val delete_tagged_brl : bool * thm ->
    1.54 -    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    1.55 -      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.56 -  val lessb             : (bool * thm) * (bool * thm) -> bool
    1.57 -  val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
    1.58 -  val make_elim         : thm -> thm
    1.59 -  val match_from_net_tac        : (int*thm) Net.net -> int -> tactic
    1.60 -  val match_tac : thm list -> int -> tactic
    1.61 -  val metacut_tac       : thm -> int -> tactic
    1.62 -  val net_bimatch_tac   : (bool*thm) list -> int -> tactic
    1.63 -  val net_biresolve_tac : (bool*thm) list -> int -> tactic
    1.64 -  val net_match_tac     : thm list -> int -> tactic
    1.65 -  val net_resolve_tac   : thm list -> int -> tactic
    1.66 -  val rename_params_tac : string list -> int -> tactic
    1.67 -  val rename_tac        : string -> int -> tactic
    1.68 -  val rename_last_tac   : string -> string list -> int -> tactic
    1.69 -  val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
    1.70 -  val resolve_tac       : thm list -> int -> tactic
    1.71 -  val res_inst_tac      : (string*string)list -> thm -> int -> tactic
    1.72 -  val rotate_tac        : int -> int -> tactic
    1.73 -  val rtac              : thm -> int -> tactic
    1.74 -  val rule_by_tactic    : tactic -> thm -> thm
    1.75 -  val solve_tac         : thm list -> int -> tactic
    1.76 -  val subgoal_tac       : string -> int -> tactic
    1.77 -  val subgoals_tac      : string list -> int -> tactic
    1.78 -  val subgoals_of_brl   : bool * thm -> int
    1.79 -  val term_lift_inst_rule       :
    1.80 -      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm
    1.81 -      -> thm
    1.82 -  val instantiate_tac   : (string * string) list -> tactic
    1.83 -  val thin_tac          : string -> int -> tactic
    1.84 -  val trace_goalno_tac  : (int -> tactic) -> int -> tactic
    1.85 +  val trace_goalno_tac: (int -> tactic) -> int -> tactic
    1.86 +  val rule_by_tactic: tactic -> thm -> thm
    1.87 +  val assume_tac: int -> tactic
    1.88 +  val eq_assume_tac: int -> tactic
    1.89 +  val compose_tac: (bool * thm * int) -> int -> tactic
    1.90 +  val make_elim: thm -> thm
    1.91 +  val biresolve_tac: (bool * thm) list -> int -> tactic
    1.92 +  val resolve_tac: thm list -> int -> tactic
    1.93 +  val eresolve_tac: thm list -> int -> tactic
    1.94 +  val forward_tac: thm list -> int -> tactic
    1.95 +  val dresolve_tac: thm list -> int -> tactic
    1.96 +  val atac: int -> tactic
    1.97 +  val rtac: thm -> int -> tactic
    1.98 +  val dtac: thm -> int ->tactic
    1.99 +  val etac: thm -> int ->tactic
   1.100 +  val ftac: thm -> int ->tactic
   1.101 +  val datac: thm -> int -> int -> tactic
   1.102 +  val eatac: thm -> int -> int -> tactic
   1.103 +  val fatac: thm -> int -> int -> tactic
   1.104 +  val ares_tac: thm list -> int -> tactic
   1.105 +  val solve_tac: thm list -> int -> tactic
   1.106 +  val bimatch_tac: (bool * thm) list -> int -> tactic
   1.107 +  val match_tac: thm list -> int -> tactic
   1.108 +  val ematch_tac: thm list -> int -> tactic
   1.109 +  val dmatch_tac: thm list -> int -> tactic
   1.110 +  val flexflex_tac: tactic
   1.111 +  val distinct_subgoal_tac: int -> tactic
   1.112 +  val distinct_subgoals_tac: tactic
   1.113 +  val lift_inst_rule: thm * int * (string*string)list * thm -> thm
   1.114 +  val term_lift_inst_rule:
   1.115 +    thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
   1.116 +  val compose_inst_tac: (string * string) list -> (bool * thm * int) -> int -> tactic
   1.117 +  val res_inst_tac: (string * string) list -> thm -> int -> tactic
   1.118 +  val eres_inst_tac: (string * string) list -> thm -> int -> tactic
   1.119 +  val cut_inst_tac: (string * string) list -> thm -> int -> tactic
   1.120 +  val forw_inst_tac: (string * string) list -> thm -> int -> tactic
   1.121 +  val dres_inst_tac: (string * string) list -> thm -> int -> tactic
   1.122 +  val instantiate_tac: (string * string) list -> tactic
   1.123 +  val thin_tac: string -> int -> tactic
   1.124 +  val metacut_tac: thm -> int -> tactic
   1.125 +  val cut_rules_tac: thm list -> int -> tactic
   1.126 +  val cut_facts_tac: thm list -> int -> tactic
   1.127 +  val subgoal_tac: string -> int -> tactic
   1.128 +  val subgoals_tac: string list -> int -> tactic
   1.129 +  val filter_thms: (term * term -> bool) -> int * term * thm list -> thm list
   1.130 +  val biresolution_from_nets_tac: ('a list -> (bool * thm) list) ->
   1.131 +    bool -> 'a Net.net * 'a Net.net -> int -> tactic
   1.132 +  val biresolve_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
   1.133 +    int -> tactic
   1.134 +  val bimatch_from_nets_tac: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
   1.135 +    int -> tactic
   1.136 +  val net_biresolve_tac: (bool * thm) list -> int -> tactic
   1.137 +  val net_bimatch_tac: (bool * thm) list -> int -> tactic
   1.138 +  val build_net: thm list -> (int * thm) Net.net
   1.139 +  val filt_resolve_tac: thm list -> int -> int -> tactic
   1.140 +  val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
   1.141 +  val match_from_net_tac: (int * thm) Net.net -> int -> tactic
   1.142 +  val net_resolve_tac: thm list -> int -> tactic
   1.143 +  val net_match_tac: thm list -> int -> tactic
   1.144 +  val subgoals_of_brl: bool * thm -> int
   1.145 +  val lessb: (bool * thm) * (bool * thm) -> bool
   1.146 +  val rename_params_tac: string list -> int -> tactic
   1.147 +  val rename_tac: string -> int -> tactic
   1.148 +  val rename_last_tac: string -> string list -> int -> tactic
   1.149 +  val rotate_tac: int -> int -> tactic
   1.150 +  val defer_tac: int -> tactic
   1.151 +  val filter_prems_tac: (term -> bool) -> int -> tactic
   1.152  end;
   1.153  
   1.154  signature TACTIC =
   1.155  sig
   1.156    include BASIC_TACTIC
   1.157    val innermost_params: int -> thm -> (string * typ) list
   1.158 +  val lift_inst_rule': thm * int * (indexname * string) list * thm -> thm
   1.159 +  val compose_inst_tac': (indexname * string) list -> (bool * thm * int) -> int -> tactic
   1.160 +  val res_inst_tac': (indexname * string) list -> thm -> int -> tactic
   1.161 +  val eres_inst_tac': (indexname * string) list -> thm -> int -> tactic
   1.162 +  val make_elim_preserve: thm -> thm
   1.163 +  val instantiate_tac': (indexname * string) list -> tactic
   1.164    val untaglist: (int * 'a) list -> 'a list
   1.165 -  val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
   1.166    val orderlist: (int * 'a) list -> 'a list
   1.167 -  val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
   1.168 -                          int -> tactic
   1.169 -  val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
   1.170 -  val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
   1.171 -  val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
   1.172 -  val instantiate_tac'  : (indexname * string) list -> tactic
   1.173 -  val make_elim_preserve: thm -> thm
   1.174 +  val insert_tagged_brl: 'a * (bool * thm) ->
   1.175 +    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
   1.176 +      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
   1.177 +  val build_netpair: (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net ->
   1.178 +    (bool * thm) list -> (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
   1.179 +  val delete_tagged_brl: bool * thm ->
   1.180 +    ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
   1.181 +      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
   1.182 +  val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
   1.183  end;
   1.184  
   1.185  structure Tactic: TACTIC =
   1.186 @@ -137,6 +133,7 @@
   1.187  (*Solve subgoal i by assumption, using no unification*)
   1.188  fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
   1.189  
   1.190 +
   1.191  (** Resolution/matching tactics **)
   1.192  
   1.193  (*The composition rule/state: no lifting or var renaming.
   1.194 @@ -203,7 +200,7 @@
   1.195      [] => no_tac st
   1.196    | A :: Bs =>
   1.197        st |> EVERY (fold (fn (B, k) =>
   1.198 -	if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
   1.199 +        if A aconv B then cons (distinct_tac (i, k)) else I) (Bs ~~ (1 upto length Bs)) []));
   1.200  
   1.201  fun distinct_subgoals_tac state =
   1.202    let