diff options
Diffstat (limited to 'tactics/elim.ml')
-rw-r--r-- | tactics/elim.ml | 64 |
1 files changed, 32 insertions, 32 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index fa4a7caa..cac200f5 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: elim.ml 11739 2009-01-02 19:33:19Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -28,12 +28,12 @@ open Genarg open Tacexpr let introElimAssumsThen tac ba = - let nassums = - List.fold_left - (fun acc b -> if b then acc+2 else acc+1) - 0 ba.branchsign - in - let introElimAssums = tclDO nassums intro in + let nassums = + List.fold_left + (fun acc b -> if b then acc+2 else acc+1) + 0 ba.branchsign + in + let introElimAssums = tclDO nassums intro in (tclTHEN introElimAssums (elim_on_ba tac ba)) let introCaseAssumsThen tac ba = @@ -41,12 +41,12 @@ let introCaseAssumsThen tac ba = List.flatten (List.map (function b -> if b then [false;true] else [false]) ba.branchsign) - in + in let n1 = List.length case_thin_sign in let n2 = List.length ba.branchnames in let (l1,l2),l3 = if n1 < n2 then list_chop n1 ba.branchnames, [] - else + else (ba.branchnames, []), if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in let introCaseAssums = @@ -75,9 +75,9 @@ let elimHypThen tac id gl = elimination_then tac ([],[]) (mkVar id) gl let rec general_decompose_on_hyp recognizer = - ifOnHyp recognizer (general_decompose recognizer) (fun _ -> tclIDTAC) + ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> tclIDTAC) -and general_decompose recognizer id = +and general_decompose_aux recognizer id = elimHypThen (introElimAssumsThen (fun bas -> @@ -93,12 +93,12 @@ and general_decompose recognizer id = let tmphyp_name = id_of_string "_TmpHyp" let up_to_delta = ref false (* true *) -let general_decompose recognizer c gl = - let typc = pf_type_of gl c in - tclTHENSV (cut typc) +let general_decompose recognizer c gl = + let typc = pf_type_of gl c in + tclTHENSV (cut typc) [| tclTHEN (intro_using tmphyp_name) - (onLastHyp - (ifOnHyp recognizer (general_decompose recognizer) + (onLastHypId + (ifOnHyp recognizer (general_decompose_aux recognizer) (fun id -> clear [id]))); exact_no_check c |] gl @@ -110,7 +110,7 @@ let head_in gls indl t = else extract_mrectype t in List.mem ity indl with Not_found -> false - + let inductive_of = function | IndRef ity -> ity | r -> @@ -118,34 +118,34 @@ let inductive_of = function (Printer.pr_global r ++ str " is not an inductive type.") let decompose_these c l gls = - let indl = (*List.map inductive_of*) l in + let indl = (*List.map inductive_of*) l in general_decompose (fun (_,t) -> head_in gls indl t) c gls let decompose_nonrec c gls = - general_decompose + general_decompose (fun (_,t) -> is_non_recursive_type t) c gls -let decompose_and c gls = - general_decompose +let decompose_and c gls = + general_decompose (fun (_,t) -> is_record t) c gls -let decompose_or c gls = - general_decompose +let decompose_or c gls = + general_decompose (fun (_,t) -> is_disjunction t) c gls let inj_open c = (Evd.empty,c) let h_decompose l c = - Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l) + Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) let h_decompose_or c = - Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c) + Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) let h_decompose_and c = - Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c) + Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) (* The tactic Double performs a double induction *) @@ -153,17 +153,17 @@ let simple_elimination c gls = simple_elimination_then (fun _ -> tclIDTAC) c gls let induction_trailer abs_i abs_j bargs = - tclTHEN + tclTHEN (tclDO (abs_j - abs_i) intro) - (onLastHyp + (onLastHypId (fun id gls -> let idty = pf_type_of gls (mkVar id) in let fvty = global_vars (pf_env gls) idty in let possible_bring_hyps = - (List.tl (nLastHyps (abs_j - abs_i) gls)) @ bargs.assums + (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums in let (hyps,_) = - List.fold_left + List.fold_left (fun (bring_ids,leave_ids) (cid,_,cidty as d) -> if not (List.mem cid leave_ids) then (d::bring_ids,leave_ids) @@ -172,7 +172,7 @@ let induction_trailer abs_i abs_j bargs = in let ids = List.rev (ids_of_named_context hyps) in (tclTHENSEQ - [bring_hyps hyps; tclTRY (clear ids); + [bring_hyps hyps; tclTRY (clear ids); simple_elimination (mkVar id)]) gls)) @@ -184,7 +184,7 @@ let double_ind h1 h2 gls = if abs_i > abs_j then (abs_j,abs_i) else error "Both hypotheses are the same." in (tclTHEN (tclDO abs_i intro) - (onLastHyp + (onLastHypId (fun id -> elimination_then (introElimAssumsThen (induction_trailer abs_i abs_j)) |