improved induct_tac;
authorwenzelm
Wed Apr 12 18:53:20 2000 +0200 (2000-04-12)
changeset 8689a2e82eed6454
parent 8688 63b267d41b96
child 8690 48786b52c8d8
improved induct_tac;
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Apr 12 18:53:09 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Apr 12 18:53:20 2000 +0200
     1.3 @@ -167,26 +167,39 @@
     1.4               else ();
     1.5              tacf i));
     1.6  
     1.7 +
     1.8  (* generic induction tactic for datatypes *)
     1.9  
    1.10 -fun gen_induct_tac (vars, opt_rule) i state =
    1.11 +local
    1.12 +
    1.13 +fun prep_var (Var (ixn, _), Some x) = Some (implode (tl (explode (Syntax.string_of_vname ixn))), x)
    1.14 +  | prep_var _ = None;
    1.15 +
    1.16 +fun prep_inst (concl, xs) =	(*exception LIST*)
    1.17 +  let val vs = InductMethod.vars_of concl
    1.18 +  in mapfilter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.19 +
    1.20 +in
    1.21 +
    1.22 +fun gen_induct_tac (varss, opt_rule) i state =
    1.23    let
    1.24 -    val (_, _, Bi, _) = dest_state (state, i);
    1.25 -    val {sign, ...} = rep_thm state;
    1.26 +    val (_, _, Bi, _) = Thm.dest_state (state, i);
    1.27 +    val {sign, ...} = Thm.rep_thm state;
    1.28      val (rule, rule_name) =
    1.29        (case opt_rule of
    1.30          Some r => (r, "Induction rule")
    1.31        | None =>
    1.32 -          let val tn = find_tname (hd vars) Bi
    1.33 +          let val tn = find_tname (hd (mapfilter I (flat varss))) Bi
    1.34            in (#induction (datatype_info_sg_err sign tn), "Induction rule for type " ^ tn) end);
    1.35 -    val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
    1.36 -      implode (tl (explode (Syntax.string_of_vname ixn))))
    1.37 -        (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule)));
    1.38 -    val insts = (ind_vnames ~~ vars) handle LIST _ =>
    1.39 -      error (rule_name ^ " has different number of variables");
    1.40 -  in occs_in_prems (Tactic.res_inst_tac insts rule) vars i state end;
    1.41  
    1.42 -fun induct_tac s = gen_induct_tac (Syntax.read_idents s, None);
    1.43 +    val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule));
    1.44 +    val insts = flat (map2 prep_inst (concls, varss)) handle LIST _ =>
    1.45 +      error (rule_name ^ " has different numbers of variables");
    1.46 +  in occs_in_prems (Tactic.res_inst_tac insts rule) (map #2 insts) i state end;
    1.47 +
    1.48 +fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
    1.49 +
    1.50 +end;
    1.51  
    1.52  
    1.53  (* generic case tactic for datatypes *)
    1.54 @@ -213,19 +226,21 @@
    1.55  
    1.56  local
    1.57  
    1.58 -val rule_spec = Args.$$$ "rule" -- Args.$$$ ":";
    1.59 -val opt_rule = Scan.option (Scan.lift rule_spec |-- Attrib.local_thm);
    1.60 +val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
    1.61 +val opt_rule = Scan.option (rule_spec |-- Attrib.local_thm);
    1.62 +
    1.63 +val varss = Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name_dummy)));
    1.64  
    1.65  fun tactic_syntax args tac =
    1.66 -  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (Scan.lift args -- opt_rule) >>
    1.67 +  #2 oo Method.syntax (Args.goal_spec HEADGOAL -- (args -- opt_rule) >>
    1.68      (fn (quant, x) => Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac x))));
    1.69  
    1.70  in
    1.71  
    1.72  val tactic_emulations =
    1.73 - [("induct_tac", tactic_syntax (Scan.repeat1 (Scan.unless rule_spec Args.name)) gen_induct_tac,
    1.74 + [("induct_tac", tactic_syntax varss gen_induct_tac,
    1.75      "induct_tac emulation (dynamic instantiation!)"),
    1.76 -  ("case_tac", tactic_syntax Args.name gen_case_tac,
    1.77 +  ("case_tac", tactic_syntax (Scan.lift Args.name) gen_case_tac,
    1.78      "case_tac emulation (dynamic instantiation!)")];
    1.79  
    1.80  end;