--- 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;