src/HOL/thy_syntax.ML
changeset 2922 580647a879cf
parent 1845 afa622bc829d
child 2930 602cdeabb89b
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Apr 09 12:31:11 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Apr 09 12:32:04 1997 +0200
     1.3 @@ -120,7 +120,8 @@
     1.4    fun mk_params ((ts, tname), cons) =
     1.5     ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
     1.6      ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
     1.7 -    \val thy = thy",
     1.8 +    \val thy = thy"
     1.9 +    ,
    1.10      "structure " ^ tname ^ " =\n\
    1.11      \struct\n\
    1.12      \ val inject = map (get_axiom thy) " ^
    1.13 @@ -172,6 +173,7 @@
    1.14  
    1.15  (** primrec **)
    1.16  
    1.17 +(*recursion equations have user-supplied names*)
    1.18  fun mk_primrec_decl_1 ((fname, tname), axms) =
    1.19    let
    1.20      (*Isolate type name from the structure's identifier it may be stored in*)
    1.21 @@ -184,10 +186,13 @@
    1.22        \  (fn _ => [Simp_tac 1]));";
    1.23  
    1.24      val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
    1.25 -  in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
    1.26 +  in ("|> " ^ tname ^ "_add_primrec " ^ axs
    1.27 +      , 
    1.28 +      cat_lines (map mk_prove axms)
    1.29        ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
    1.30    end;
    1.31  
    1.32 +(*recursion equations have no names*)
    1.33  fun mk_primrec_decl_2 ((fname, tname), axms) =
    1.34    let
    1.35      (*Isolate type name from the structure's identifier it may be stored in*)
    1.36 @@ -199,17 +204,44 @@
    1.37        \(fn _ => [Simp_tac 1])";
    1.38  
    1.39      val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
    1.40 -  in ("|> " ^ tname ^ "_add_primrec " ^ axs,
    1.41 +  in ("|> " ^ tname ^ "_add_primrec " ^ axs
    1.42 +      ,
    1.43        "val dummy = Addsimps " ^
    1.44        brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
    1.45    end;
    1.46  
    1.47 +(*function name, argument type and either (name,axiom) pairs or just axioms*)
    1.48  val primrec_decl =
    1.49    (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
    1.50    (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
    1.51  
    1.52  
    1.53  
    1.54 +
    1.55 +(** rec: interface to Slind's TFL **)
    1.56 +
    1.57 +
    1.58 +fun mk_rec_decl ((fname, rel), axms) =
    1.59 +  let val fid = trim fname
    1.60 +  in
    1.61 +	 (";\n\n\
    1.62 +          \structure " ^ fid ^ " =\n\
    1.63 +          \  struct\n\
    1.64 +          \  val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
    1.65 +          \  val {induct,eqns,thy,tcs} = Tfl.RfuncStringList " ^ 
    1.66 +	                 rel ^ "\n" ^ mk_big_list axms ^ " thy;\n\
    1.67 +          \  end;\n\n\
    1.68 +          \val thy = thy"
    1.69 +         ,
    1.70 +	 "")
    1.71 +  end;
    1.72 +
    1.73 +val rec_decl = (name -- string -- repeat1 string >> mk_rec_decl) ;
    1.74 +
    1.75 +
    1.76 +
    1.77 +
    1.78 +
    1.79  (** sections **)
    1.80  
    1.81  val user_keywords = ["intrs", "monos", "con_defs", "|"];
    1.82 @@ -219,7 +251,8 @@
    1.83    ("inductive", inductive_decl ""),
    1.84    ("coinductive", inductive_decl "Co"),
    1.85    ("datatype", datatype_decl),
    1.86 -  ("primrec", primrec_decl)];
    1.87 +  ("primrec", primrec_decl),
    1.88 +  ("recdef", rec_decl)];
    1.89  
    1.90  
    1.91  end;