src/HOL/thy_syntax.ML
changeset 3194 36bfceef1800
parent 2930 602cdeabb89b
child 3308 da002cef7090
     1.1 --- a/src/HOL/thy_syntax.ML	Thu May 15 12:45:42 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu May 15 12:53:12 1997 +0200
     1.3 @@ -47,10 +47,10 @@
     1.4        let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
     1.5            and srec_tms = mk_list recs
     1.6            and sintrs   = mk_big_list (map snd ipairs)
     1.7 -          val stri_name = big_rec_name ^ "_Intrnl"
     1.8 +          val intrnl_name = big_rec_name ^ "_Intrnl"
     1.9        in
    1.10           (";\n\n\
    1.11 -          \structure " ^ stri_name ^ " =\n\
    1.12 +          \structure " ^ intrnl_name ^ " =\n\
    1.13            \  struct\n\
    1.14            \  val _ = writeln \"" ^ co ^
    1.15                       "Inductive definition " ^ big_rec_name ^ "\"\n\
    1.16 @@ -60,15 +60,15 @@
    1.17                             ^ sintrs ^ "\n\
    1.18            \  end;\n\n\
    1.19            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
    1.20 -             stri_name ^ ".rec_tms, " ^
    1.21 -             stri_name ^ ".intr_tms)"
    1.22 +             intrnl_name ^ ".rec_tms, " ^
    1.23 +             intrnl_name ^ ".intr_tms)"
    1.24           ,
    1.25            "structure " ^ big_rec_name ^ " =\n\
    1.26            \ let\n\
    1.27            \  val _ = writeln \"Proofs for " ^ co ^ 
    1.28                       "Inductive definition " ^ big_rec_name ^ "\"\n\
    1.29            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    1.30 -          \\t  (open " ^ stri_name ^ "\n\
    1.31 +          \\t  (open " ^ intrnl_name ^ "\n\
    1.32            \\t   val thy\t\t= thy\n\
    1.33            \\t   val monos\t\t= " ^ monos ^ "\n\
    1.34            \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
    1.35 @@ -78,7 +78,7 @@
    1.36            \  open Result\n\
    1.37            \  end\n\
    1.38            \ end;\n\n\
    1.39 -          \structure " ^ stri_name ^ " = struct end;\n\n"
    1.40 +          \structure " ^ intrnl_name ^ " = struct end;\n\n"
    1.41           )
    1.42        end
    1.43      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    1.44 @@ -114,7 +114,7 @@
    1.45      end;
    1.46  
    1.47    fun mk_rules tname cons pre = " map (get_axiom thy) " ^
    1.48 -    mk_list (map (fn ((s, _), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
    1.49 +    mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
    1.50  
    1.51    (*generate string for calling add_datatype and build_record*)
    1.52    fun mk_params ((ts, tname), cons) =
    1.53 @@ -225,19 +225,25 @@
    1.54  (** rec: interface to Slind's TFL **)
    1.55  
    1.56  
    1.57 +(*fname: name of function being defined; rel: well-founded relation*)
    1.58  fun mk_rec_decl ((fname, rel), axms) =
    1.59    let val fid = trim fname
    1.60 +      val intrnl_name = fid ^ "_Intrnl"
    1.61    in
    1.62  	 (";\n\n\
    1.63 -          \structure " ^ fid ^ " =\n\
    1.64 -          \  struct\n\
    1.65 -          \  val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
    1.66 -          \  val {induct,eqns,thy,tcs} = Tfl.RfuncStringList " ^ 
    1.67 -	                 rel ^ "\n" ^ mk_big_list axms ^ " thy;\n\
    1.68 -          \  end;\n\n\
    1.69 +          \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
    1.70 +          \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
    1.71 +	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
    1.72            \val thy = thy"
    1.73           ,
    1.74 -	 "")
    1.75 +          "structure " ^ fid ^ " =\n\
    1.76 +          \  struct\n\
    1.77 +          \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
    1.78 +          \  val {rules, induct, tcs} = \n\
    1.79 +          \    \t Tfl.simplify_defn(thy, (\"" ^ fid ^ 
    1.80 +					  "\", pats_" ^ intrnl_name ^ "))\n\
    1.81 +          \  end;\n\
    1.82 +          \val pats_" ^ intrnl_name ^ " = ();\n")
    1.83    end;
    1.84  
    1.85  val rec_decl = (name -- string -- repeat1 string >> mk_rec_decl) ;