src/HOL/Tools/inductive_package.ML
changeset 28839 32d498cf7595
parent 28791 cc16be808796
child 28941 128459bd72d2
equal deleted inserted replaced
28838:d5db6dfcb34a 28839:32d498cf7595
    31   val get_monos: Proof.context -> thm list
    31   val get_monos: Proof.context -> thm list
    32   val mk_cases: Proof.context -> term -> thm
    32   val mk_cases: Proof.context -> term -> thm
    33   val inductive_forall_name: string
    33   val inductive_forall_name: string
    34   val inductive_forall_def: thm
    34   val inductive_forall_def: thm
    35   val rulify: thm -> thm
    35   val rulify: thm -> thm
    36   val inductive_cases: (Attrib.binding * string list) list -> Proof.context ->
    36   val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
    37     thm list list * local_theory
    37     thm list list * local_theory
    38   val inductive_cases_i: (Attrib.binding * term list) list -> Proof.context ->
    38   val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
    39     thm list list * local_theory
    39     thm list list * local_theory
    40   type inductive_flags
    40   type inductive_flags
    41   val add_inductive_i:
    41   val add_inductive_i:
    42     inductive_flags -> ((Name.binding * typ) * mixfix) list ->
    42     inductive_flags -> ((Name.binding * typ) * mixfix) list ->
    43     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
    43     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
   751     val raw_induct = zero_var_indexes
   751     val raw_induct = zero_var_indexes
   752       (if no_ind then Drule.asm_rl else
   752       (if no_ind then Drule.asm_rl else
   753        if coind then
   753        if coind then
   754          singleton (ProofContext.export
   754          singleton (ProofContext.export
   755            (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
   755            (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
   756            (rotate_prems ~1 (ObjectLogic.rulify (rule_by_tactic
   756            (rotate_prems ~1 (ObjectLogic.rulify
   757              (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN
   757              (fold_rule rec_preds_defs
   758                fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct)))))
   758                (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq]
       
   759                 (mono RS (fp_def RS def_coinduct))))))
   759        else
   760        else
   760          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   761          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
   761            rec_preds_defs ctxt1);
   762            rec_preds_defs ctxt1);
   762 
   763 
   763     val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind
   764     val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind