src/Pure/section_utils.ML
author paulson
Tue, 22 Jul 1997 11:14:18 +0200
changeset 3538 ed9de44032e0
parent 3536 8fb4150e2ad3
child 3934 a9c8960e4da6
permissions -rw-r--r--
Removal of the tactical STATE
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
     1
(*  Title: 	Pure/section-utils
579
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
     2
    ID:         $Id$
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
579
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
     5
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
     6
Utilities for writing new theory sections
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
     7
*)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
     8
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
     9
fun ap t u = t$u;
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    10
fun app t (u1,u2) = t $ u1 $ u2;
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    11
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    12
(*Make distinct individual variables a1, a2, a3, ..., an. *)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    13
fun mk_frees a [] = []
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    14
  | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    15
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    16
(*Make a definition lhs==rhs*)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    17
fun mk_defpair (lhs, rhs) = 
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    18
  let val Const(name, _) = head_of lhs
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    19
  in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    20
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    21
fun get_def thy s = get_axiom thy (s^"_def");
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    22
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    23
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    24
(*Read an assumption in the given theory*)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    25
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    26
1390
bf523422a3df Commented and renamed vars in readtm
paulson
parents: 654
diff changeset
    27
(*Read a term from string "b", with expected type T*)
bf523422a3df Commented and renamed vars in readtm
paulson
parents: 654
diff changeset
    28
fun readtm sign T b = 
bf523422a3df Commented and renamed vars in readtm
paulson
parents: 654
diff changeset
    29
    read_cterm sign (b,T) |> term_of
3536
8fb4150e2ad3 tuned error propagation msg;
wenzelm
parents: 2863
diff changeset
    30
    handle ERROR => error ("The error(s) above occurred for " ^ b);
579
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    31
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    32
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    33
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    34
  | tryres (th, []) = raise THM("tryres", 0, [th]);
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    35
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    36
fun gen_make_elim elim_rls rl = 
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    37
      standard (tryres (rl, elim_rls @ [revcut_rl]));
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    38
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    39
(** String manipulation **)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    40
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    41
(*Skipping initial blanks, find the first identifier*)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    42
fun scan_to_id s = 
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    43
    s |> explode |> take_prefix is_blank |> #2 |> Scanner.scan_id |> #1
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    44
    handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s);
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    45
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    46
fun is_backslash c = c = "\\";
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    47
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    48
(*Apply string escapes to a quoted string; see Def of Standard ML, page 3
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    49
  Does not handle the \ddd form;  no error checking*)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    50
fun escape [] = []
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    51
  | escape cs = (case take_prefix (not o is_backslash) cs of
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    52
	 (front, []) => front
579
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    53
       | (front, _::"n"::rest) => front @ ("\n" :: escape rest)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    54
       | (front, _::"t"::rest) => front @ ("\t" :: escape rest)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    55
       | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    56
       | (front, _::"\""::rest) => front @ ("\"" :: escape rest)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    57
       | (front, _::"\\"::rest) => front @ ("\\" :: escape rest)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    58
       | (front, b::c::rest) => 
1460
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    59
	   if is_blank c   (*remove any further blanks and the following \ *)
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    60
	   then front @ escape (tl (snd (take_prefix is_blank rest)))
5a6f2aabd538 inserted tabs again
clasohm
parents: 1458
diff changeset
    61
	   else error ("Unrecognized string escape: " ^ implode(b::c::rest)));
579
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    62
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    63
(*Remove the first and last charaters -- presumed to be quotes*)
08f465e23dc5 new file of useful things for writing theory sections
lcp
parents:
diff changeset
    64
val trim = implode o escape o rev o tl o rev o tl o explode;
654
65435e2c6512 added require_thy;
wenzelm
parents: 613
diff changeset
    65
65435e2c6512 added require_thy;
wenzelm
parents: 613
diff changeset
    66
65435e2c6512 added require_thy;
wenzelm
parents: 613
diff changeset
    67
(*Check for some named theory*)
65435e2c6512 added require_thy;
wenzelm
parents: 613
diff changeset
    68
fun require_thy thy name sect =
65435e2c6512 added require_thy;
wenzelm
parents: 613
diff changeset
    69
  if exists (equal name o !) (stamps_of_thy thy) then ()
2863
d97f5f424b97 Made the error message more explicit
paulson
parents: 1460
diff changeset
    70
  else error ("Need theory " ^ quote name ^ " as an ancestor for " ^ sect);