src/HOL/Tools/primrec_package.ML
changeset 25604 6c1714b9b805
parent 25570 fdfbbb92dadf
child 26129 14f6dbb195c4
equal deleted inserted replaced
25603:4b7a58fc168c 25604:6c1714b9b805
   202             if tnames' subset (map (#1 o snd) (#descr dt)) then
   202             if tnames' subset (map (#1 o snd) (#descr dt)) then
   203               (tname, dt)::(find_dts dt_info tnames' tnames)
   203               (tname, dt)::(find_dts dt_info tnames' tnames)
   204             else find_dts dt_info tnames' tnames);
   204             else find_dts dt_info tnames' tnames);
   205 
   205 
   206 
   206 
   207 (* adapted induction rule *)
       
   208 
       
   209 fun prepare_induct ({descr, induction, ...}: datatype_info) eqns =
       
   210   let
       
   211     fun constrs_of (_, (_, _, cs)) =
       
   212       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;
       
   213     val params_of = these o AList.lookup (op =) (List.concat (map constrs_of eqns));
       
   214   in
       
   215     induction
       
   216     |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
       
   217     |> RuleCases.save induction
       
   218   end;
       
   219 
       
   220 
       
   221 (* primrec definition *)
   207 (* primrec definition *)
   222 
   208 
   223 local
   209 local
   224 
   210 
   225 fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
   211 fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
   265     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
   251     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
   266     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
   252     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
   267     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
   253     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
   268     |-> (fn simps' => LocalTheory.note Thm.theoremK
   254     |-> (fn simps' => LocalTheory.note Thm.theoremK
   269           ((qualify "simps", simp_atts), maps snd simps'))
   255           ((qualify "simps", simp_atts), maps snd simps'))
   270     ||>> LocalTheory.note Thm.theoremK
   256     |>> snd
   271           ((qualify "induct", []), [prepare_induct (#2 (hd dts)) eqns])
       
   272     |>> (snd o fst)
       
   273   end handle PrimrecError (msg, some_eqn) =>
   257   end handle PrimrecError (msg, some_eqn) =>
   274     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
   258     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
   275      of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
   259      of SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
   276       | NONE => ""));
   260       | NONE => ""));
   277 
   261