src/HOL/Tools/datatype_package.ML
changeset 8279 3453f73fad71
parent 8100 6186ee807f2e
child 8306 9855f1801d2b
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Feb 22 21:48:24 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Feb 22 21:48:50 2000 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4  sig
     1.5    val induct_tac : string -> int -> tactic
     1.6    val exhaust_tac : string -> int -> tactic
     1.7 +  val cases_tac : string -> int -> tactic
     1.8    val distinct_simproc : simproc
     1.9  end;
    1.10  
    1.11 @@ -70,6 +71,7 @@
    1.12    val constrs_of : theory -> string -> term list option
    1.13    val constrs_of_sg : Sign.sg -> string -> term list option
    1.14    val case_const_of : theory -> string -> term option
    1.15 +  val cases_of: Sign.sg -> string -> thm
    1.16    val setup: (theory -> theory) list
    1.17  end;
    1.18  
    1.19 @@ -128,6 +130,9 @@
    1.20  
    1.21  val constrs_of = constrs_of_sg o Theory.sign_of;
    1.22  
    1.23 +val exhaustion_of = #exhaustion oo datatype_info_sg_err
    1.24 +fun cases_of sg name = if name = HOLogic.boolN then case_split_thm else exhaustion_of sg name;
    1.25 +
    1.26  fun case_const_of thy tname = (case datatype_info thy tname of
    1.27     Some {case_name, ...} => Some (Const (case_name, the (Sign.const_type
    1.28       (Theory.sign_of thy) case_name)))
    1.29 @@ -142,9 +147,10 @@
    1.30       | _ => error ("Cannot determine type of " ^ quote var)
    1.31    end;
    1.32  
    1.33 -fun infer_tname state sign i aterm =
    1.34 +fun infer_tname state i aterm =
    1.35    let
    1.36 -    val (_, _, Bi, _) = dest_state (state, i)
    1.37 +    val sign = Thm.sign_of_thm state;
    1.38 +    val (_, _, Bi, _) = Thm.dest_state (state, i)
    1.39      val params = Logic.strip_params Bi;   (*params of subgoal i*)
    1.40      val params = rev (rename_wrt_term Bi params);   (*as they are printed*)
    1.41      val (types, sorts) = types_sorts state;
    1.42 @@ -184,19 +190,20 @@
    1.43      occs_in_prems (res_inst_tac insts induction) vars i state
    1.44    end;
    1.45  
    1.46 +
    1.47  (* generic exhaustion tactic for datatypes *)
    1.48  
    1.49 -fun exhaust_tac aterm i state =
    1.50 +fun gen_exhaust_tac get_rule aterm i state =
    1.51    let
    1.52 -    val {sign, ...} = rep_thm state;
    1.53 -    val tn = infer_tname state sign i aterm;
    1.54 -    val {exhaustion, ...} = datatype_info_sg_err sign tn;
    1.55 +    val rule = get_rule (Thm.sign_of_thm state) (infer_tname state i aterm);
    1.56      val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    1.57 -      (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
    1.58 +      (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
    1.59      val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
    1.60 -  in
    1.61 -    res_inst_tac [(exh_vname, aterm)] exhaustion i state
    1.62 -  end;
    1.63 +  in res_inst_tac [(exh_vname, aterm)] rule i state end;
    1.64 +
    1.65 +val exhaust_tac = gen_exhaust_tac exhaustion_of;
    1.66 +val cases_tac = gen_exhaust_tac cases_of;
    1.67 +
    1.68  
    1.69  
    1.70  (**** simplification procedure for showing distinctness of constructors ****)