src/HOL/Tools/datatype_package.ML
changeset 14174 f3cafd2929d5
parent 13641 63d1790a43ed
child 14412 109cc0dc706b
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Aug 29 13:18:45 2003 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Aug 29 15:19:02 2003 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun gen_induct_tac (varss, opt_rule) i state =
     1.8 +fun gen_induct_tac inst_tac (varss, opt_rule) i state =
     1.9    let
    1.10      val (_, _, Bi, _) = Thm.dest_state (state, i);
    1.11      val {sign, ...} = Thm.rep_thm state;
    1.12 @@ -203,33 +203,39 @@
    1.13      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.14      val insts = flat (map prep_inst (concls ~~ varss)) handle LIST _ =>
    1.15        error (rule_name ^ " has different numbers of variables");
    1.16 -  in occs_in_prems (Tactic.res_inst_tac insts rule) (map #2 insts) i state end;
    1.17 +  in occs_in_prems (inst_tac insts rule) (map #2 insts) i state end;
    1.18  
    1.19 -fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
    1.20 +fun induct_tac s =
    1.21 +  gen_induct_tac Tactic.res_inst_tac
    1.22 +    (map (Library.single o Some) (Syntax.read_idents s), None);
    1.23  
    1.24  fun induct_thm_tac th s =
    1.25 -  gen_induct_tac ([map Some (Syntax.read_idents s)], Some th);
    1.26 +  gen_induct_tac Tactic.res_inst_tac
    1.27 +    ([map Some (Syntax.read_idents s)], Some th);
    1.28  
    1.29  end;
    1.30  
    1.31  
    1.32  (* generic case tactic for datatypes *)
    1.33  
    1.34 -fun case_inst_tac t rule i state =
    1.35 +fun case_inst_tac inst_tac t rule i state =
    1.36    let
    1.37      val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    1.38        (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
    1.39      val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)));
    1.40 -  in Tactic.res_inst_tac [(exh_vname, t)] rule i state end;
    1.41 +  in inst_tac [(exh_vname, t)] rule i state end;
    1.42  
    1.43 -fun gen_case_tac (t, Some rule) i state = case_inst_tac t rule i state
    1.44 -  | gen_case_tac (t, None) i state =
    1.45 +fun gen_case_tac inst_tac (t, Some rule) i state =
    1.46 +      case_inst_tac inst_tac t rule i state
    1.47 +  | gen_case_tac inst_tac (t, None) i state =
    1.48        let val tn = infer_tname state i t in
    1.49 -        if tn = HOLogic.boolN then Tactic.res_inst_tac [("P", t)] case_split_thm i state
    1.50 -        else case_inst_tac t (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn)) i state
    1.51 +        if tn = HOLogic.boolN then inst_tac [("P", t)] case_split_thm i state
    1.52 +        else case_inst_tac inst_tac t
    1.53 +               (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn))
    1.54 +               i state
    1.55        end;
    1.56  
    1.57 -fun case_tac t = gen_case_tac (t, None);
    1.58 +fun case_tac t = gen_case_tac Tactic.res_inst_tac (t, None);
    1.59  
    1.60  
    1.61  
    1.62 @@ -242,13 +248,23 @@
    1.63  
    1.64  val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
    1.65  
    1.66 +fun mk_ixn (vars, s) = (fst (Term.dest_Var (Syntax.read_var ("?" ^ vars))), s)
    1.67 +  handle _ => error (vars ^ " not a variable name");
    1.68 +fun inst_tac ctxt sinsts =
    1.69 +  Method.bires_inst_tac false ctxt (map mk_ixn sinsts);
    1.70 +
    1.71 +fun induct_meth ctxt (varss, opt_rule) =
    1.72 +  gen_induct_tac (inst_tac ctxt) (varss, opt_rule);
    1.73 +fun case_meth ctxt (varss, opt_rule) =
    1.74 +  gen_case_tac (inst_tac ctxt) (varss, opt_rule);
    1.75 +
    1.76  in
    1.77  
    1.78  val tactic_emulations =
    1.79 - [("induct_tac", Method.goal_args' (varss -- opt_rule) gen_induct_tac,
    1.80 -    "induct_tac emulation (dynamic instantiation!)"),
    1.81 -  ("case_tac", Method.goal_args' (Scan.lift Args.name -- opt_rule) gen_case_tac,
    1.82 -    "case_tac emulation (dynamic instantiation!)")];
    1.83 + [("induct_tac", Method.goal_args_ctxt' (varss -- opt_rule) induct_meth,
    1.84 +    "induct_tac emulation (dynamic instantiation)"),
    1.85 +  ("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) case_meth,
    1.86 +    "case_tac emulation (dynamic instantiation)")];
    1.87  
    1.88  end;
    1.89