src/HOL/Tools/recdef_package.ML
author wenzelm
Fri Jan 11 00:28:24 2002 +0100 (2002-01-11)
changeset 12708 31672377dadc
parent 12694 9950c1ce9d24
child 12755 a906a8b364f1
permissions -rw-r--r--
clarified IsarThy.apply_theorems_i;
     1 (*  Title:      HOL/Tools/recdef_package.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Wrapper module for Konrad Slind's TFL package.
     7 *)
     8 
     9 signature RECDEF_PACKAGE =
    10 sig
    11   val quiet_mode: bool ref
    12   val print_recdefs: theory -> unit
    13   val get_recdef: theory -> string
    14     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
    15   val simp_add_global: theory attribute
    16   val simp_del_global: theory attribute
    17   val cong_add_global: theory attribute
    18   val cong_del_global: theory attribute
    19   val wf_add_global: theory attribute
    20   val wf_del_global: theory attribute
    21   val simp_add_local: Proof.context attribute
    22   val simp_del_local: Proof.context attribute
    23   val cong_add_local: Proof.context attribute
    24   val cong_del_local: Proof.context attribute
    25   val wf_add_local: Proof.context attribute
    26   val wf_del_local: Proof.context attribute
    27   val add_recdef: bool -> xstring -> string -> ((bstring * string) * Args.src list) list ->
    28     Args.src option -> theory -> theory
    29       * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    30   val add_recdef_i: bool -> xstring -> term -> ((bstring * term) * theory attribute list) list ->
    31     theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    32   val add_recdef_old: xstring -> string -> ((bstring * string) * Args.src list) list ->
    33     simpset * thm list -> theory ->
    34     theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    35   val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
    36     -> theory -> theory * {induct_rules: thm}
    37   val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
    38     -> theory -> theory * {induct_rules: thm}
    39   val recdef_tc: bstring * Args.src list -> xstring -> int option
    40     -> bool -> theory -> ProofHistory.T
    41   val recdef_tc_i: bstring * theory attribute list -> string -> int option
    42     -> bool -> theory -> ProofHistory.T
    43   val setup: (theory -> theory) list
    44 end;
    45 
    46 structure RecdefPackage: RECDEF_PACKAGE =
    47 struct
    48 
    49 
    50 val quiet_mode = Tfl.quiet_mode;
    51 val message = Tfl.message;
    52 
    53 
    54 (** recdef hints **)
    55 
    56 (* type hints *)
    57 
    58 type hints = {simps: thm list, congs: (string * thm) list, wfs: thm list};
    59 
    60 fun mk_hints (simps, congs, wfs) = {simps = simps, congs = congs, wfs = wfs}: hints;
    61 fun map_hints f ({simps, congs, wfs}: hints) = mk_hints (f (simps, congs, wfs));
    62 
    63 fun map_simps f = map_hints (fn (simps, congs, wfs) => (f simps, congs, wfs));
    64 fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
    65 fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
    66 
    67 fun pretty_hints ({simps, congs, wfs}: hints) =
    68  [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps),
    69   Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map #2 congs)),
    70   Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)];
    71 
    72 
    73 (* congruence rules *)
    74 
    75 local
    76 
    77 val cong_head =
    78   fst o Term.dest_Const o Term.head_of o fst o Logic.dest_equals o Thm.concl_of;
    79 
    80 fun prep_cong raw_thm =
    81   let val thm = safe_mk_meta_eq raw_thm in (cong_head thm, thm) end;
    82 
    83 in
    84 
    85 fun add_cong raw_thm congs =
    86   let val (c, thm) = prep_cong raw_thm
    87   in overwrite_warn (congs, (c, thm)) ("Overwriting recdef congruence rule for " ^ quote c) end;
    88 
    89 fun del_cong raw_thm congs =
    90   let
    91     val (c, thm) = prep_cong raw_thm;
    92     val (del, rest) = Library.partition (Library.equal c o fst) congs;
    93   in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
    94 
    95 val add_congs = curry (foldr (uncurry add_cong));
    96 
    97 end;
    98 
    99 
   100 
   101 (** global and local recdef data **)
   102 
   103 (* theory data kind 'HOL/recdef' *)
   104 
   105 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
   106 
   107 structure GlobalRecdefArgs =
   108 struct
   109   val name = "HOL/recdef";
   110   type T = recdef_info Symtab.table * hints;
   111 
   112   val empty = (Symtab.empty, mk_hints ([], [], [])): T;
   113   val copy = I;
   114   val prep_ext = I;
   115   fun merge
   116    ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
   117     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) =
   118       (Symtab.merge (K true) (tab1, tab2),
   119         mk_hints (Drule.merge_rules (simps1, simps2),
   120           Library.merge_alists congs1 congs2,
   121           Drule.merge_rules (wfs1, wfs2)));
   122 
   123   fun print sg (tab, hints) =
   124    (Pretty.strs ("recdefs:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)) ::
   125      pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
   126 end;
   127 
   128 structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);
   129 val print_recdefs = GlobalRecdefData.print;
   130 
   131 
   132 fun get_recdef thy name = Symtab.lookup (#1 (GlobalRecdefData.get thy), name);
   133 
   134 fun put_recdef name info thy =
   135   let
   136     val (tab, hints) = GlobalRecdefData.get thy;
   137     val tab' = Symtab.update_new ((name, info), tab)
   138       handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
   139   in GlobalRecdefData.put (tab', hints) thy end;
   140 
   141 val get_global_hints = #2 o GlobalRecdefData.get;
   142 val map_global_hints = GlobalRecdefData.map o apsnd;
   143 
   144 
   145 (* proof data kind 'HOL/recdef' *)
   146 
   147 structure LocalRecdefArgs =
   148 struct
   149   val name = "HOL/recdef";
   150   type T = hints;
   151   val init = get_global_hints;
   152   fun print _ hints = pretty_hints hints |> Pretty.chunks |> Pretty.writeln;
   153 end;
   154 
   155 structure LocalRecdefData = ProofDataFun(LocalRecdefArgs);
   156 val get_local_hints = LocalRecdefData.get;
   157 val map_local_hints = LocalRecdefData.map;
   158 
   159 
   160 (* attributes *)
   161 
   162 local
   163 
   164 fun global_local f g =
   165  (fn (thy, thm) => (map_global_hints (f (g thm)) thy, thm),
   166   fn (ctxt, thm) => (map_local_hints (f (g thm)) ctxt, thm));
   167 
   168 fun mk_attr (add1, add2) (del1, del2) =
   169  (Attrib.add_del_args add1 del1, Attrib.add_del_args add2 del2);
   170 
   171 in
   172 
   173 val (simp_add_global, simp_add_local) = global_local map_simps Drule.add_rule;
   174 val (simp_del_global, simp_del_local) = global_local map_simps Drule.del_rule;
   175 val (cong_add_global, cong_add_local) = global_local map_congs add_cong;
   176 val (cong_del_global, cong_del_local) = global_local map_congs del_cong;
   177 val (wf_add_global, wf_add_local) = global_local map_wfs Drule.add_rule;
   178 val (wf_del_global, wf_del_local) = global_local map_wfs Drule.del_rule;
   179 
   180 val simp_attr = mk_attr (simp_add_global, simp_add_local) (simp_del_global, simp_del_local);
   181 val cong_attr = mk_attr (cong_add_global, cong_add_local) (cong_del_global, cong_del_local);
   182 val wf_attr = mk_attr (wf_add_global, wf_add_local) (wf_del_global, wf_del_local);
   183 
   184 end;
   185 
   186 
   187 (* modifiers *)
   188 
   189 val recdef_simpN = "recdef_simp";
   190 val recdef_congN = "recdef_cong";
   191 val recdef_wfN = "recdef_wf";
   192 
   193 val recdef_modifiers =
   194  [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
   195   Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
   196   Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
   197   Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local),
   198   Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add_local),
   199   Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del_local),
   200   Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local),
   201   Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add_local),
   202   Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del_local)] @
   203   Clasimp.clasimp_modifiers;
   204 
   205 
   206 
   207 (** prepare_hints(_i) **)
   208 
   209 fun prepare_hints thy opt_src =
   210   let
   211     val ctxt0 = ProofContext.init thy;
   212     val ctxt =
   213       (case opt_src of
   214         None => ctxt0
   215       | Some src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
   216     val {simps, congs, wfs} = get_local_hints ctxt;
   217     val cs = Classical.get_local_claset ctxt;
   218     val ss = Simplifier.get_local_simpset ctxt addsimps simps;
   219   in (cs, ss, map #2 congs, wfs) end;
   220 
   221 fun prepare_hints_i thy () =
   222   let val {simps, congs, wfs} = get_global_hints thy
   223   in (Classical.claset_of thy, Simplifier.simpset_of thy addsimps simps, map #2 congs, wfs) end;
   224 
   225 
   226 
   227 (** add_recdef(_i) **)
   228 
   229 fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
   230 
   231 fun gen_add_recdef tfl_fn prep_att prep_hints strict raw_name R eq_srcs hints thy =
   232   let
   233     val _ = requires_recdef thy;
   234 
   235     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
   236     val bname = Sign.base_name name;
   237     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
   238 
   239     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
   240     val eq_atts = map (map (prep_att thy)) raw_eq_atts;
   241 
   242     val (cs, ss, congs, wfs) = prep_hints thy hints;
   243     val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn strict thy cs ss congs wfs name R eqs;
   244     val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
   245     val simp_att = if null tcs then
   246       [Simplifier.simp_add_global, RecfunCodegen.add] else [];
   247 
   248     val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
   249     val (thy, (simps' :: rules', [induct'])) =
   250       thy
   251       |> Theory.add_path bname
   252       |> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   253       |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
   254     val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
   255     val thy =
   256       thy
   257       |> put_recdef name result
   258       |> Theory.parent_path;
   259   in (thy, result) end;
   260 
   261 val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints;
   262 fun add_recdef_i x y z w = gen_add_recdef Tfl.define_i (K I) prepare_hints_i x y z w ();
   263 
   264 
   265 (* add_recdef_old -- legacy interface *)
   266 
   267 fun prepare_hints_old thy (ss, thms) =
   268   let val {simps, congs, wfs} = get_global_hints thy
   269   in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs thms congs), wfs) end;
   270 
   271 val add_recdef_old = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints_old false;
   272 
   273 
   274 
   275 (** defer_recdef(_i) **)
   276 
   277 fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy =
   278   let
   279     val name = Sign.intern_const (Theory.sign_of thy) raw_name;
   280     val bname = Sign.base_name name;
   281 
   282     val _ = requires_recdef thy;
   283     val _ = message ("Deferred recursive function " ^ quote name ^ " ...");
   284 
   285     val (thy1, congs) = thy |> app_thms raw_congs;
   286     val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
   287     val (thy3, [induct_rules']) =
   288       thy2
   289       |> Theory.add_path bname
   290       |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
   291       |>> Theory.parent_path;
   292   in (thy3, {induct_rules = induct_rules'}) end;
   293 
   294 val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems;
   295 val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i;
   296 
   297 
   298 
   299 (** recdef_tc(_i) **)
   300 
   301 fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int thy =
   302   let
   303     val name = prep_name (Theory.sign_of thy) raw_name;
   304     val atts = map (prep_att thy) raw_atts;
   305     val tcs =
   306       (case get_recdef thy name of
   307         None => error ("No recdef definition of constant: " ^ quote name)
   308       | Some {tcs, ...} => tcs);
   309     val i = if_none opt_i 1;
   310     val tc = Library.nth_elem (i - 1, tcs) handle Library.LIST _ =>
   311       error ("No termination condition #" ^ string_of_int i ^
   312         " in recdef definition of " ^ quote name);
   313   in
   314     thy |> IsarThy.theorem_i Drule.internalK
   315       (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
   316   end;
   317 
   318 val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
   319 val recdef_tc_i = gen_recdef_tc (K I) (K I);
   320 
   321 
   322 
   323 (** package setup **)
   324 
   325 (* setup theory *)
   326 
   327 val setup =
   328  [GlobalRecdefData.init, LocalRecdefData.init,
   329   Attrib.add_attributes
   330    [(recdef_simpN, simp_attr, "declaration of recdef simp rule"),
   331     (recdef_congN, cong_attr, "declaration of recdef cong rule"),
   332     (recdef_wfN, wf_attr, "declaration of recdef wf rule")]];
   333 
   334 
   335 (* outer syntax *)
   336 
   337 local structure P = OuterParse and K = OuterSyntax.Keyword in
   338 
   339 val hints =
   340   P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
   341 
   342 val recdef_decl =
   343   Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
   344   P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment)
   345     -- Scan.option hints
   346   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
   347 
   348 val recdefP =
   349   OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
   350     (recdef_decl >> Toplevel.theory);
   351 
   352 
   353 val defer_recdef_decl =
   354   P.name -- Scan.repeat1 P.prop --
   355   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) []
   356   >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   357 
   358 val defer_recdefP =
   359   OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
   360     (defer_recdef_decl >> Toplevel.theory);
   361 
   362 
   363 val recdef_tc_decl =
   364   P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
   365     --| P.marg_comment;
   366 
   367 fun mk_recdef_tc ((thm_name, name), i) = recdef_tc thm_name name i;
   368 
   369 val recdef_tcP =
   370   OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal
   371     (recdef_tc_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_recdef_tc)));
   372 
   373 
   374 val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"];
   375 val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP, recdef_tcP];
   376 
   377 end;
   378 
   379 
   380 end;