7 *) |
7 *) |
8 |
8 |
9 signature BASIC_TACTIC = |
9 signature BASIC_TACTIC = |
10 sig |
10 sig |
11 val ares_tac : thm list -> int -> tactic |
11 val ares_tac : thm list -> int -> tactic |
12 val asm_rewrite_goal_tac: bool*bool*bool -> |
|
13 (MetaSimplifier.meta_simpset -> tactic) -> MetaSimplifier.meta_simpset -> int -> tactic |
|
14 val assume_tac : int -> tactic |
12 val assume_tac : int -> tactic |
15 val atac : int ->tactic |
13 val atac : int ->tactic |
16 val bimatch_from_nets_tac: |
14 val bimatch_from_nets_tac: |
17 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
15 (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic |
18 val bimatch_tac : (bool*thm)list -> int -> tactic |
16 val bimatch_tac : (bool*thm)list -> int -> tactic |
72 val net_biresolve_tac : (bool*thm) list -> int -> tactic |
70 val net_biresolve_tac : (bool*thm) list -> int -> tactic |
73 val net_match_tac : thm list -> int -> tactic |
71 val net_match_tac : thm list -> int -> tactic |
74 val net_resolve_tac : thm list -> int -> tactic |
72 val net_resolve_tac : thm list -> int -> tactic |
75 val norm_hhf_rule : thm -> thm |
73 val norm_hhf_rule : thm -> thm |
76 val norm_hhf_tac : int -> tactic |
74 val norm_hhf_tac : int -> tactic |
77 val PRIMITIVE : (thm -> thm) -> tactic |
|
78 val PRIMSEQ : (thm -> thm Seq.seq) -> tactic |
|
79 val prune_params_tac : tactic |
75 val prune_params_tac : tactic |
80 val rename_params_tac : string list -> int -> tactic |
76 val rename_params_tac : string list -> int -> tactic |
81 val rename_tac : string -> int -> tactic |
77 val rename_tac : string -> int -> tactic |
82 val rename_last_tac : string -> string list -> int -> tactic |
78 val rename_last_tac : string -> string list -> int -> tactic |
83 val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic |
79 val resolve_from_net_tac : (int*thm) Net.net -> int -> tactic |
135 | Some(st',_) => Thm.varifyT (thaw st') |
131 | Some(st',_) => Thm.varifyT (thaw st') |
136 end; |
132 end; |
137 |
133 |
138 (*** Basic tactics ***) |
134 (*** Basic tactics ***) |
139 |
135 |
140 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*) |
|
141 fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty; |
|
142 |
|
143 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*) |
|
144 fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); |
|
145 |
|
146 (*** The following fail if the goal number is out of range: |
136 (*** The following fail if the goal number is out of range: |
147 thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) |
137 thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) |
148 |
138 |
149 (*Solve subgoal i by assumption*) |
139 (*Solve subgoal i by assumption*) |
150 fun assume_tac i = PRIMSEQ (assumption i); |
140 fun assume_tac i = PRIMSEQ (assumption i); |
497 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; |
487 fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; |
498 |
488 |
499 |
489 |
500 (*** Meta-Rewriting Tactics ***) |
490 (*** Meta-Rewriting Tactics ***) |
501 |
491 |
502 fun result1 tacf mss thm = |
|
503 apsome fst (Seq.pull (tacf mss thm)); |
|
504 |
|
505 val simple_prover = |
492 val simple_prover = |
506 result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss))); |
493 SINGLE o (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss))); |
507 |
494 |
508 val rewrite = MetaSimplifier.rewrite_aux simple_prover; |
495 val rewrite = MetaSimplifier.rewrite_aux simple_prover; |
509 val simplify = MetaSimplifier.simplify_aux simple_prover; |
496 val simplify = MetaSimplifier.simplify_aux simple_prover; |
510 val rewrite_rule = simplify true; |
497 val rewrite_rule = simplify true; |
511 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover; |
498 val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover; |
512 |
499 |
513 (*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) |
|
514 fun asm_rewrite_goal_tac mode prover_tac mss = |
|
515 SELECT_GOAL |
|
516 (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (result1 prover_tac) mss 1)); |
|
517 |
|
518 fun rewrite_goal_tac rews = |
500 fun rewrite_goal_tac rews = |
519 asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews); |
501 MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews); |
520 |
502 |
521 (*Rewrite throughout proof state. *) |
503 (*Rewrite throughout proof state. *) |
522 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); |
504 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); |
523 |
505 |
524 (*Rewrite subgoals only, not main goal. *) |
506 (*Rewrite subgoals only, not main goal. *) |