inductive_cases(_i): Isar interface to mk_cases;
authorwenzelm
Tue Jul 27 22:03:24 1999 +0200 (1999-07-27)
changeset 7107ce69de572bca
parent 7106 c47d94f61ced
child 7108 0229ce6735f6
inductive_cases(_i): Isar interface to mk_cases;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jul 27 22:00:00 1999 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jul 27 22:03:24 1999 +0200
     1.3 @@ -46,12 +46,17 @@
     1.4        (xstring * Args.src list) list -> theory -> theory *
     1.5        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
     1.6         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
     1.7 +  val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
     1.8 +    -> theory -> theory
     1.9 +  val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
    1.10 +    -> theory -> theory
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13  
    1.14  structure InductivePackage: INDUCTIVE_PACKAGE =
    1.15  struct
    1.16  
    1.17 +
    1.18  (** utilities **)
    1.19  
    1.20  (* messages *)
    1.21 @@ -96,9 +101,8 @@
    1.22  
    1.23  (* misc *)
    1.24  
    1.25 -(*For proving monotonicity of recursion operator*)
    1.26 -val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
    1.27 -                   ex_mono, Collect_mono, in_mono, vimage_mono];
    1.28 +(*for proving monotonicity of recursion operator*)
    1.29 +val default_monos = basic_monos @ [vimage_mono];
    1.30  
    1.31  val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
    1.32  
    1.33 @@ -326,7 +330,7 @@
    1.34  
    1.35      val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
    1.36        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.37 -        (fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)])
    1.38 +        (fn _ => [rtac monoI 1, REPEAT (ares_tac (default_monos @ monos) 1)])
    1.39  
    1.40    in mono end;
    1.41  
    1.42 @@ -402,16 +406,44 @@
    1.43       THEN prune_params_tac
    1.44    end;
    1.45  
    1.46 -(*String s should have the form t:Si where Si is an inductive set*)
    1.47 +(*cprop should have the form t:Si where Si is an inductive set*)
    1.48 +fun mk_cases_i elims ss cprop =
    1.49 +  let
    1.50 +    val prem = Thm.assume cprop;
    1.51 +    fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl));
    1.52 +  in
    1.53 +    (case get_first (try mk_elim) elims of
    1.54 +      Some r => r
    1.55 +    | None => error (Pretty.string_of (Pretty.block
    1.56 +        [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
    1.57 +          Display.pretty_cterm cprop])))
    1.58 +  end;
    1.59 +
    1.60  fun mk_cases elims s =
    1.61 -  let val prem = assume (read_cterm (Thm.sign_of_thm (hd elims)) (s, propT))
    1.62 -      fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl) 
    1.63 -	               |> standard
    1.64 -  in case find_first is_some (map (try mk_elim) elims) of
    1.65 -       Some (Some r) => r
    1.66 -     | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")
    1.67 +  mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
    1.68 +
    1.69 +
    1.70 +(* inductive_cases(_i) *)
    1.71 +
    1.72 +fun gen_inductive_cases prep_att prep_const prep_prop
    1.73 +    ((((name, raw_atts), raw_set), raw_props), comment) thy =
    1.74 +  let
    1.75 +    val sign = Theory.sign_of thy;
    1.76 +
    1.77 +    val atts = map (prep_att thy) raw_atts;
    1.78 +    val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
    1.79 +    val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
    1.80 +    val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops;
    1.81 +  in
    1.82 +    thy
    1.83 +    |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
    1.84    end;
    1.85  
    1.86 +val inductive_cases =
    1.87 +  gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
    1.88 +
    1.89 +val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
    1.90 +
    1.91  
    1.92  
    1.93  (** prove induction rule **)
    1.94 @@ -730,8 +762,17 @@
    1.95  val coinductiveP =
    1.96    OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
    1.97  
    1.98 +
    1.99 +val ind_cases =
   1.100 +  P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
   1.101 +  >> (Toplevel.theory o inductive_cases);
   1.102 +
   1.103 +val inductive_casesP =
   1.104 +  OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
   1.105 +    K.thy_decl ind_cases;
   1.106 +
   1.107  val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
   1.108 -val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP];
   1.109 +val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   1.110  
   1.111  end;
   1.112