src/Pure/tactic.ML
changeset 31945 d5f186aa0bed
parent 31794 71af1fd6a5e4
child 32971 55ba9b6648ef
     1.1 --- a/src/Pure/tactic.ML	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -105,24 +105,24 @@
     1.4       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
     1.5  
     1.6  (*Solve subgoal i by assumption*)
     1.7 -fun assume_tac i = PRIMSEQ (assumption i);
     1.8 +fun assume_tac i = PRIMSEQ (Thm.assumption i);
     1.9  
    1.10  (*Solve subgoal i by assumption, using no unification*)
    1.11 -fun eq_assume_tac i = PRIMITIVE (eq_assumption i);
    1.12 +fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
    1.13  
    1.14  
    1.15  (** Resolution/matching tactics **)
    1.16  
    1.17  (*The composition rule/state: no lifting or var renaming.
    1.18 -  The arg = (bires_flg, orule, m) ;  see bicompose for explanation.*)
    1.19 -fun compose_tac arg i = PRIMSEQ (bicompose false arg i);
    1.20 +  The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
    1.21 +fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
    1.22  
    1.23  (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
    1.24    like [| P&Q; P==>R |] ==> R *)
    1.25  fun make_elim rl = zero_var_indexes (rl RS revcut_rl);
    1.26  
    1.27  (*Attack subgoal i by resolution, using flags to indicate elimination rules*)
    1.28 -fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i);
    1.29 +fun biresolve_tac brules i = PRIMSEQ (Thm.biresolution false brules i);
    1.30  
    1.31  (*Resolution: the simple case, works for introduction rules*)
    1.32  fun resolve_tac rules = biresolve_tac (map (pair false) rules);
    1.33 @@ -152,7 +152,7 @@
    1.34  fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
    1.35  
    1.36  (*Matching tactics -- as above, but forbid updating of state*)
    1.37 -fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i);
    1.38 +fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution true brules i);
    1.39  fun match_tac rules  = bimatch_tac (map (pair false) rules);
    1.40  fun ematch_tac rules = bimatch_tac (map (pair true) rules);
    1.41  fun dmatch_tac rls   = ematch_tac (map make_elim rls);
    1.42 @@ -295,7 +295,7 @@
    1.43        let val hyps = Logic.strip_assums_hyp prem
    1.44            and concl = Logic.strip_assums_concl prem
    1.45            val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
    1.46 -      in PRIMSEQ (biresolution match (order kbrls) i) end);
    1.47 +      in PRIMSEQ (Thm.biresolution match (order kbrls) i) end);
    1.48  
    1.49  (*versions taking pre-built nets.  No filtering of brls*)
    1.50  val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
    1.51 @@ -326,7 +326,7 @@
    1.52        in
    1.53           if pred krls
    1.54           then PRIMSEQ
    1.55 -                (biresolution match (map (pair false) (order_list krls)) i)
    1.56 +                (Thm.biresolution match (map (pair false) (order_list krls)) i)
    1.57           else no_tac
    1.58        end);
    1.59  
    1.60 @@ -359,15 +359,15 @@
    1.61  fun rename_tac xs i =
    1.62    case Library.find_first (not o Syntax.is_identifier) xs of
    1.63        SOME x => error ("Not an identifier: " ^ x)
    1.64 -    | NONE => PRIMITIVE (rename_params_rule (xs, i));
    1.65 +    | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));
    1.66  
    1.67  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
    1.68    right to left if n is positive, and from left to right if n is negative.*)
    1.69  fun rotate_tac 0 i = all_tac
    1.70 -  | rotate_tac k i = PRIMITIVE (rotate_rule k i);
    1.71 +  | rotate_tac k i = PRIMITIVE (Thm.rotate_rule k i);
    1.72  
    1.73  (*Rotates the given subgoal to be the last.*)
    1.74 -fun defer_tac i = PRIMITIVE (permute_prems (i-1) 1);
    1.75 +fun defer_tac i = PRIMITIVE (Thm.permute_prems (i - 1) 1);
    1.76  
    1.77  (* remove premises that do not satisfy p; fails if all prems satisfy p *)
    1.78  fun filter_prems_tac p =