Simplified syntax of primrec definitions.
authorberghofe
Fri Jul 05 14:22:59 1996 +0200 (1996-07-05)
changeset 1845afa622bc829d
parent 1844 791e79473966
child 1846 763f08fb194f
Simplified syntax of primrec definitions.
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Jun 28 15:30:55 1996 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri Jul 05 14:22:59 1996 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  
     1.5  (** primrec **)
     1.6  
     1.7 -fun mk_primrec_decl ((fname, tname), axms) =
     1.8 +fun mk_primrec_decl_1 ((fname, tname), axms) =
     1.9    let
    1.10      (*Isolate type name from the structure's identifier it may be stored in*)
    1.11      val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
    1.12 @@ -188,8 +188,25 @@
    1.13        ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
    1.14    end;
    1.15  
    1.16 +fun mk_primrec_decl_2 ((fname, tname), axms) =
    1.17 +  let
    1.18 +    (*Isolate type name from the structure's identifier it may be stored in*)
    1.19 +    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
    1.20 +
    1.21 +    fun mk_prove eqn =
    1.22 +      "prove_goalw thy [get_def thy "
    1.23 +      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
    1.24 +      \(fn _ => [Simp_tac 1])";
    1.25 +
    1.26 +    val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
    1.27 +  in ("|> " ^ tname ^ "_add_primrec " ^ axs,
    1.28 +      "val dummy = Addsimps " ^
    1.29 +      brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
    1.30 +  end;
    1.31 +
    1.32  val primrec_decl =
    1.33 -  name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
    1.34 +  (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
    1.35 +  (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
    1.36  
    1.37  
    1.38