# HG changeset patch # User wenzelm # Date 924778174 -7200 # Node ID e36581d04eee59c51f4eadace672cb3e4e74a611 # Parent 92d142e58a5bc7e14704c423a3a3eddc3a3861f0 recdef adapted to RecdefPackage.add_recdef; diff -r 92d142e58a5b -r e36581d04eee src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Thu Apr 22 12:49:00 1999 +0200 +++ b/src/HOL/thy_syntax.ML Thu Apr 22 12:49:34 1999 +0200 @@ -38,6 +38,7 @@ >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); + (** (co)inductive **) fun inductive_decl coind = @@ -80,6 +81,7 @@ end; + (** datatype **) local @@ -188,6 +190,7 @@ end; + (** primrec **) fun mk_primrec_decl (alt_name, eqns) = @@ -205,36 +208,35 @@ (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl; -(** rec: interface to Slind's TFL **) +(** recdef: interface to Slind's TFL **) (*fname: name of function being defined; rel: well-founded relation*) -fun mk_rec_decl ((((fname, rel), congs), ss), axms) = - let val fid = strip_quotes fname - val intrnl_name = fid ^ "_Intrnl" +fun mk_recdef_decl ((((fname, rel), congs), ss), axms) = + let + val fid = strip_quotes fname; + val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs); + val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms); in - (";\n\n\ - \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\ - \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ - quote fid ^ " " ^ - rel ^ "\n" ^ mk_big_list axms ^ ";\n\ - \val thy = thy" - , - "structure " ^ fid ^ " =\n\ - \ struct\n\ - \ val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\ - \ val {rules, induct, tcs} = \n\ - \ \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\ - \ \t\t (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\ - \ end;\n\ - \val pats_" ^ intrnl_name ^ " = ();\n") + ";\n\n\ + \local\n\ + \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^ + axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\ + \in\n\ + \structure " ^ fid ^ " =\n\ + \struct\n\ + \ val {rules, induct, tcs} = result;\n\ + \end;\n\ + \val thy = thy;\n\ + \end;\n\ + \val thy = thy\n" end; -val rec_decl = - (name -- string -- - optional ("congs" $$-- string >> strip_quotes) "[]" -- - optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- - repeat1 string >> mk_rec_decl) ; +val recdef_decl = + (name -- string -- + optional ("congs" $$-- list1 name) [] -- + optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- + repeat1 string >> mk_recdef_decl); @@ -252,6 +254,6 @@ section "datatype" "" datatype_decl, section "rep_datatype" "" rep_datatype_decl, section "primrec" "" primrec_decl, - ("recdef", rec_decl)]; + section "recdef" "" recdef_decl]; end;