Now for recdefs that omit the WF relation
authorpaulson
Fri Apr 23 12:22:30 1999 +0200 (1999-04-23)
changeset 6497120ca2bb27e1
parent 6496 a185927883e5
child 6498 1ebbe18fe236
Now for recdefs that omit the WF relation
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Apr 23 12:20:22 1999 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Apr 23 12:22:30 1999 +0200
     1.3 @@ -208,11 +208,12 @@
     1.4    (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
     1.5  
     1.6  
     1.7 +(*** recdef: interface to Slind's TFL ***)
     1.8  
     1.9 -(** recdef: interface to Slind's TFL **)
    1.10 +(** TFL with explicit WF relations **)
    1.11  
    1.12  (*fname: name of function being defined; rel: well-founded relation*)
    1.13 -fun mk_recdef_decl ((((fname, rel), congs), ss), axms) =
    1.14 +fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
    1.15    let
    1.16      val fid = strip_quotes fname;
    1.17      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.18 @@ -232,11 +233,42 @@
    1.19      \val thy = thy\n"
    1.20    end;
    1.21  
    1.22 -val recdef_decl =
    1.23 -  (name -- string --
    1.24 -    optional ("congs" $$-- list1 name) [] --
    1.25 -    optional ("simpset" $$-- string >> strip_quotes) "simpset()" --
    1.26 -    repeat1 string >> mk_recdef_decl);
    1.27 +
    1.28 +(** TFL with no WF relation supplied **)
    1.29 +
    1.30 +(*fname: name of function being defined; rel: well-founded relation*)
    1.31 +fun mk_rec_deferred_decl (((fname, congs), ss), axms) =
    1.32 +  let val fid = strip_quotes fname
    1.33 +      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
    1.34 +  in
    1.35 +      ";\n\n\
    1.36 +       \local\n\
    1.37 +       \val (thy, induct_rules) = Tfl.function thy " ^ 
    1.38 +          quote fid ^ " " ^ 
    1.39 +	  " (" ^ congs_text ^ ")\n" 
    1.40 +	  ^ mk_big_list axms ^ ";\n\
    1.41 +       \in\n\
    1.42 +       \structure " ^ fid ^ " =\n\
    1.43 +       \struct\n\
    1.44 +       \  val induct_rules = induct_rules \n\
    1.45 +       \end;\n\
    1.46 +       \val thy = thy;\nend;\n\
    1.47 +       \val thy = thy\n"
    1.48 +  end;
    1.49 +
    1.50 +
    1.51 +(*parses either a standard or a deferred recdef; the latter has no WF
    1.52 +  relation given*)
    1.53 +val recdef_decl = 
    1.54 +    (name -- string -- 
    1.55 +     optional ("congs" $$-- list1 name) [] -- 
    1.56 +     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
    1.57 +     repeat1 string >> mk_rec_decl)
    1.58 +    ||
    1.59 +    (name --$$ "??" --
    1.60 +     optional ("congs" $$-- list1 name) [] -- 
    1.61 +     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
    1.62 +     repeat1 string >> mk_rec_deferred_decl) ;
    1.63  
    1.64  
    1.65  
    1.66 @@ -246,14 +278,14 @@
    1.67  
    1.68  val _ = ThySyn.add_syntax
    1.69   ["intrs", "monos", "con_defs", "congs", "simpset", "|",
    1.70 -  "and", "distinct", "inject", "induct"]
    1.71 +  "and", "distinct", "inject", "induct", "??"]
    1.72   [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
    1.73    section "record" "|> RecordPackage.add_record" record_decl,
    1.74 -  section "inductive" "" (inductive_decl false),
    1.75 -  section "coinductive" "" (inductive_decl true),
    1.76 -  section "datatype" "" datatype_decl,
    1.77 +  section "inductive" 	"" (inductive_decl false),
    1.78 +  section "coinductive"	"" (inductive_decl true),
    1.79 +  section "datatype" 	"" datatype_decl,
    1.80    section "rep_datatype" "" rep_datatype_decl,
    1.81 -  section "primrec" "" primrec_decl,
    1.82 -  section "recdef" "" recdef_decl];
    1.83 +  section "primrec" 	"" primrec_decl,
    1.84 +  section "recdef" 	"" recdef_decl];
    1.85  
    1.86  end;