recdef adapted to RecdefPackage.add_recdef;
authorwenzelm
Thu Apr 22 12:49:34 1999 +0200 (1999-04-22)
changeset 6477e36581d04eee
parent 6476 92d142e58a5b
child 6478 48f90bc10cf5
recdef adapted to RecdefPackage.add_recdef;
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Thu Apr 22 12:49:00 1999 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Apr 22 12:49:34 1999 +0200
     1.3 @@ -38,6 +38,7 @@
     1.4    >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
     1.5  
     1.6  
     1.7 +
     1.8  (** (co)inductive **)
     1.9  
    1.10  fun inductive_decl coind =
    1.11 @@ -80,6 +81,7 @@
    1.12    end;
    1.13  
    1.14  
    1.15 +
    1.16  (** datatype **)
    1.17  
    1.18  local
    1.19 @@ -188,6 +190,7 @@
    1.20  end;
    1.21  
    1.22  
    1.23 +
    1.24  (** primrec **)
    1.25  
    1.26  fun mk_primrec_decl (alt_name, eqns) =
    1.27 @@ -205,36 +208,35 @@
    1.28    (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
    1.29  
    1.30  
    1.31 -(** rec: interface to Slind's TFL **)
    1.32  
    1.33 +(** recdef: interface to Slind's TFL **)
    1.34  
    1.35  (*fname: name of function being defined; rel: well-founded relation*)
    1.36 -fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
    1.37 -  let val fid = strip_quotes fname
    1.38 -      val intrnl_name = fid ^ "_Intrnl"
    1.39 +fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
    1.40 +  let
    1.41 +    val fid = strip_quotes fname;
    1.42 +    val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.43 +    val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms);
    1.44    in
    1.45 -	 (";\n\n\
    1.46 -          \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
    1.47 -          \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
    1.48 -	                 quote fid ^ " " ^ 
    1.49 -	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
    1.50 -          \val thy = thy"
    1.51 -         ,
    1.52 -          "structure " ^ fid ^ " =\n\
    1.53 -          \  struct\n\
    1.54 -          \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
    1.55 -          \  val {rules, induct, tcs} = \n\
    1.56 -          \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
    1.57 -          \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
    1.58 -          \  end;\n\
    1.59 -          \val pats_" ^ intrnl_name ^ " = ();\n")
    1.60 +    ";\n\n\
    1.61 +    \local\n\
    1.62 +    \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
    1.63 +    axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
    1.64 +    \in\n\
    1.65 +    \structure " ^ fid ^ " =\n\
    1.66 +    \struct\n\
    1.67 +    \  val {rules, induct, tcs} = result;\n\
    1.68 +    \end;\n\
    1.69 +    \val thy = thy;\n\
    1.70 +    \end;\n\
    1.71 +    \val thy = thy\n"
    1.72    end;
    1.73  
    1.74 -val rec_decl = 
    1.75 -    (name -- string -- 
    1.76 -     optional ("congs" $$-- string >> strip_quotes) "[]" -- 
    1.77 -     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
    1.78 -     repeat1 string >> mk_rec_decl) ;
    1.79 +val recdef_decl =
    1.80 +  (name -- string --
    1.81 +    optional ("congs" $$-- list1 name) [] --
    1.82 +    optional ("simpset" $$-- string >> strip_quotes) "simpset()" --
    1.83 +    repeat1 string >> mk_recdef_decl);
    1.84  
    1.85  
    1.86  
    1.87 @@ -252,6 +254,6 @@
    1.88    section "datatype" "" datatype_decl,
    1.89    section "rep_datatype" "" rep_datatype_decl,
    1.90    section "primrec" "" primrec_decl,
    1.91 -  ("recdef", rec_decl)];
    1.92 +  section "recdef" "" recdef_decl];
    1.93  
    1.94  end;