# HG changeset patch
# User lcp
# Date 777810060 -7200
# Node ID 08f465e23dc5b40432d993fbddfd9858fb81f583
# Parent  efc648d29dd0a720d61c9a508fcf60017914a48d
new file of useful things for writing theory sections

diff -r efc648d29dd0 -r 08f465e23dc5 src/Pure/section_utils.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/section_utils.ML	Thu Aug 25 12:21:00 1994 +0200
@@ -0,0 +1,65 @@
+(*  Title: 	Pure/section-utils
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Utilities for writing new theory sections
+*)
+
+fun ap t u = t$u;
+fun app t (u1,u2) = t $ u1 $ u2;
+
+(*Make distinct individual variables a1, a2, a3, ..., an. *)
+fun mk_frees a [] = []
+  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
+
+(*Make a definition lhs==rhs*)
+fun mk_defpair (lhs, rhs) = 
+  let val Const(name, _) = head_of lhs
+  in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
+
+fun get_def thy s = get_axiom thy (s^"_def");
+
+fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
+
+
+(*Read an assumption in the given theory*)
+fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
+
+fun readtm sign T a = 
+    read_cterm sign (a,T) |> term_of
+    handle ERROR => error ("The error above occurred for " ^ a);
+
+(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
+fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
+  | tryres (th, []) = raise THM("tryres", 0, [th]);
+
+fun gen_make_elim elim_rls rl = 
+      standard (tryres (rl, elim_rls @ [revcut_rl]));
+
+(** String manipulation **)
+
+(*Skipping initial blanks, find the first identifier*)
+fun scan_to_id s = 
+    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
+    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
+
+fun is_backslash c = c = "\\";
+
+(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
+  Does not handle the \ddd form;  no error checking*)
+fun escape [] = []
+  | escape cs = (case take_prefix (not o is_backslash) cs of
+	 (front, []) => front
+       | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
+       | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
+       | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
+       | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
+       | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
+       | (front, b::c::rest) => 
+	   if is_blank c   (*remove any further blanks and the following \ *)
+	   then front @ escape (tl (snd (take_prefix is_blank rest)))
+	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
+
+(*Remove the first and last charaters -- presumed to be quotes*)
+val trim = implode o escape o rev o tl o rev o tl o explode;