raplaced "intrs" by "intrs" (new-style only);
authorwenzelm
Mon Aug 14 18:14:54 2000 +0200 (2000-08-14)
changeset 959865ee72db0236
parent 9597 938a99cc55f7
child 9599 48d438b316c9
raplaced "intrs" by "intrs" (new-style only);
improved new-style interface to mk_cases;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Aug 14 18:13:42 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Aug 14 18:14:54 2000 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5                  Stefan Berghofer,   TU Muenchen
     1.6      Copyright   1994  University of Cambridge
     1.7 -                1998  TU Muenchen     
     1.8 +                1998  TU Muenchen
     1.9  
    1.10  (Co)Inductive Definition module for HOL.
    1.11  
    1.12 @@ -49,9 +49,9 @@
    1.13        (xstring * Args.src list) list -> theory -> theory *
    1.14        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.15         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    1.16 -  val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
    1.17 +  val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    1.18      -> theory -> theory
    1.19 -  val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
    1.20 +  val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    1.21      -> theory -> theory
    1.22    val setup: (theory -> theory) list
    1.23  end;
    1.24 @@ -59,6 +59,7 @@
    1.25  structure InductivePackage: INDUCTIVE_PACKAGE =
    1.26  struct
    1.27  
    1.28 +
    1.29  (*** theory data ***)
    1.30  
    1.31  (* data kind 'HOL/inductive' *)
    1.32 @@ -92,6 +93,11 @@
    1.33  
    1.34  fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
    1.35  
    1.36 +fun the_inductive thy name =
    1.37 +  (case get_inductive thy name of
    1.38 +    None => error ("Unknown (co)inductive set " ^ quote name)
    1.39 +  | Some info => info);
    1.40 +
    1.41  fun put_inductives names info thy =
    1.42    let
    1.43      fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
    1.44 @@ -291,7 +297,7 @@
    1.45    in
    1.46      map mk_elim (cs ~~ cTs)
    1.47    end;
    1.48 -        
    1.49 +
    1.50  
    1.51  
    1.52  (** premises and conclusions of induction rules **)
    1.53 @@ -331,7 +337,7 @@
    1.54          fun mk_prem (s, prems) = (case subst s of
    1.55                (_, Some (t, u)) => t :: u :: prems
    1.56              | (t, _) => t :: prems);
    1.57 -          
    1.58 +
    1.59          val Const ("op :", _) $ t $ u =
    1.60            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
    1.61  
    1.62 @@ -472,47 +478,48 @@
    1.63  (** derivation of simplified elimination rules **)
    1.64  
    1.65  (*Applies freeness of the given constructors, which *must* be unfolded by
    1.66 -  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
    1.67 +  the given defs.  Cannot simply use the local con_defs because con_defs=[]
    1.68    for inference systems.
    1.69   *)
    1.70  
    1.71  (*cprop should have the form t:Si where Si is an inductive set*)
    1.72 -fun mk_cases_i solved elims ss cprop =
    1.73 +
    1.74 +val mk_cases_err = "mk_cases: proposition not of form 't : S_i'";
    1.75 +
    1.76 +fun mk_cases_i elims ss cprop =
    1.77    let
    1.78      val prem = Thm.assume cprop;
    1.79 -    val tac = TRYALL (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
    1.80 +    val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac;
    1.81      fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
    1.82    in
    1.83      (case get_first (try mk_elim) elims of
    1.84        Some r => r
    1.85      | None => error (Pretty.string_of (Pretty.block
    1.86 -        [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
    1.87 -          Display.pretty_cterm cprop])))
    1.88 +        [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
    1.89    end;
    1.90  
    1.91  fun mk_cases elims s =
    1.92 -  mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
    1.93 +  mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
    1.94 +
    1.95 +fun smart_mk_cases thy ss cprop =
    1.96 +  let
    1.97 +    val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
    1.98 +      (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
    1.99 +    val (_, {elims, ...}) = the_inductive thy c;
   1.100 +  in mk_cases_i elims ss cprop end;
   1.101  
   1.102  
   1.103  (* inductive_cases(_i) *)
   1.104  
   1.105  fun gen_inductive_cases prep_att prep_const prep_prop
   1.106 -    ((((name, raw_atts), raw_set), raw_props), comment) thy =
   1.107 -  let val sign = Theory.sign_of thy;
   1.108 -  in (case get_inductive thy (prep_const sign raw_set) of
   1.109 -      None => error ("Unknown (co)inductive set " ^ quote name)
   1.110 -    | Some (_, {elims, ...}) =>
   1.111 -        let
   1.112 -          val atts = map (prep_att thy) raw_atts;
   1.113 -          val cprops = map
   1.114 -            (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   1.115 -          val thms = map
   1.116 -            (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
   1.117 -        in
   1.118 -          thy |> IsarThy.have_theorems_i
   1.119 -            [(((name, atts), map Thm.no_attributes thms), comment)]
   1.120 -        end)
   1.121 -  end;
   1.122 +    (((name, raw_atts), raw_props), comment) thy =
   1.123 +  let
   1.124 +    val ss = Simplifier.simpset_of thy;
   1.125 +    val sign = Theory.sign_of thy;
   1.126 +    val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   1.127 +    val atts = map (prep_att thy) raw_atts;
   1.128 +    val thms = map (smart_mk_cases thy ss) cprops;
   1.129 +  in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end;
   1.130  
   1.131  val inductive_cases =
   1.132    gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
   1.133 @@ -520,6 +527,18 @@
   1.134  val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
   1.135  
   1.136  
   1.137 +(* mk_cases_meth *)
   1.138 +
   1.139 +fun mk_cases_meth (ctxt, raw_props) =
   1.140 +  let
   1.141 +    val thy = ProofContext.theory_of ctxt;
   1.142 +    val ss = Simplifier.get_local_simpset ctxt;
   1.143 +    val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
   1.144 +  in Method.erule (map (smart_mk_cases thy ss) cprops) end;
   1.145 +
   1.146 +val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   1.147 +
   1.148 +
   1.149  
   1.150  (** prove induction rule **)
   1.151  
   1.152 @@ -662,7 +681,7 @@
   1.153      val mono = prove_mono setT fp_fun monos thy'
   1.154  
   1.155    in
   1.156 -    (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) 
   1.157 +    (thy', mono, fp_def, rec_sets_defs, rec_const, sumT)
   1.158    end;
   1.159  
   1.160  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   1.161 @@ -693,7 +712,7 @@
   1.162  
   1.163      val (thy'', [intrs']) =
   1.164        thy'
   1.165 -      |> PureThy.add_thmss [(("intrs", intrs), atts)]
   1.166 +      |> PureThy.add_thmss [(("intros", intrs), atts)]
   1.167        |>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts))
   1.168        |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
   1.169        |>> (if no_ind then I else #1 o PureThy.add_thms
   1.170 @@ -728,16 +747,14 @@
   1.171      val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
   1.172      val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   1.173      val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   1.174 -    
   1.175 -    val thy'' =
   1.176 +
   1.177 +    val (thy'', [intrs, raw_elims]) =
   1.178        thy'
   1.179 -      |> (#1 o PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])])
   1.180 -      |> (if coind then I else
   1.181 +      |> PureThy.add_axiomss_i [(("intros", intr_ts), atts), (("raw_elims", elim_ts), [])]
   1.182 +      |>> (if coind then I else
   1.183              #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   1.184  
   1.185 -    val intrs = PureThy.get_thms thy'' "intrs";
   1.186 -    val elims = map2 (fn (th, cases) => RuleCases.name cases th)
   1.187 -      (PureThy.get_thms thy'' "raw_elims", elim_cases);
   1.188 +    val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases);
   1.189      val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct";
   1.190      val induct = if coind orelse length cs > 1 then raw_induct
   1.191        else standard (raw_induct RSN (2, rev_mp));
   1.192 @@ -828,6 +845,8 @@
   1.193  
   1.194  val setup =
   1.195   [InductiveData.init,
   1.196 +  Method.add_methods [("mk_cases_tac", mk_cases_meth oo mk_cases_args,
   1.197 +    "dynamic case analysis on sets")],
   1.198    Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
   1.199  
   1.200  
   1.201 @@ -840,7 +859,7 @@
   1.202  
   1.203  fun ind_decl coind =
   1.204    (Scan.repeat1 P.term --| P.marg_comment) --
   1.205 -  (P.$$$ "intrs" |--
   1.206 +  (P.$$$ "intros" |--
   1.207      P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   1.208    Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   1.209    Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   1.210 @@ -854,14 +873,14 @@
   1.211  
   1.212  
   1.213  val ind_cases =
   1.214 -  P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
   1.215 +  P.opt_thm_name "=" -- Scan.repeat1 P.prop -- P.marg_comment
   1.216    >> (Toplevel.theory o inductive_cases);
   1.217  
   1.218  val inductive_casesP =
   1.219 -  OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
   1.220 -    K.thy_decl ind_cases;
   1.221 +  OuterSyntax.improper_command "inductive_cases"
   1.222 +    "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   1.223  
   1.224 -val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
   1.225 +val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs", "of"];
   1.226  val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   1.227  
   1.228  end;