Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field
of a theorem to be regarded as a cterm -- avoids expensive calls to
cterm_of.
--- a/src/Pure/drule.ML Tue Jan 18 07:53:35 1994 +0100
+++ b/src/Pure/drule.ML Tue Jan 18 13:46:08 1994 +0100
@@ -14,40 +14,50 @@
local open Thm in
val asm_rl: thm
val assume_ax: theory -> string -> thm
+ val cterm_fun: (term -> term) -> (cterm -> cterm)
val COMP: thm * thm -> thm
val compose: thm * int * thm -> thm list
- val cterm_instantiate: (Sign.cterm*Sign.cterm)list -> thm -> thm
+ val cterm_instantiate: (cterm*cterm)list -> thm -> thm
val cut_rl: thm
- val equal_abs_elim: Sign.cterm -> thm -> thm
- val equal_abs_elim_list: Sign.cterm list -> thm -> thm
+ val equal_abs_elim: cterm -> thm -> thm
+ val equal_abs_elim_list: cterm list -> thm -> thm
val eq_sg: Sign.sg * Sign.sg -> bool
val eq_thm: thm * thm -> bool
val eq_thm_sg: thm * thm -> bool
- val flexpair_abs_elim_list: Sign.cterm list -> thm -> thm
- val forall_intr_list: Sign.cterm list -> thm -> thm
+ val flexpair_abs_elim_list: cterm list -> thm -> thm
+ val forall_intr_list: cterm list -> thm -> thm
val forall_intr_frees: thm -> thm
- val forall_elim_list: Sign.cterm list -> thm -> thm
+ val forall_elim_list: cterm list -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
- val implies_intr_list: Sign.cterm list -> thm -> thm
+ val implies_intr_list: cterm list -> thm -> thm
val MRL: thm list list * thm list -> thm list
val MRS: thm list * thm -> thm
- val print_cterm: Sign.cterm -> unit
- val print_ctyp: Sign.ctyp -> unit
+ val pprint_cterm: cterm -> pprint_args -> unit
+ val pprint_ctyp: ctyp -> pprint_args -> unit
+ val pprint_sg: Sign.sg -> pprint_args -> unit
+ val pprint_theory: theory -> pprint_args -> unit
+ val pprint_thm: thm -> pprint_args -> unit
+ val pretty_thm: thm -> Sign.Syntax.Pretty.T
+ val print_cterm: cterm -> unit
+ val print_ctyp: ctyp -> unit
val print_goals: int -> thm -> unit
val print_goals_ref: (int -> thm -> unit) ref
val print_sg: Sign.sg -> unit
val print_theory: theory -> unit
- val pprint_sg: Sign.sg -> pprint_args -> unit
- val pprint_theory: theory -> pprint_args -> unit
- val pretty_thm: thm -> Sign.Syntax.Pretty.T
val print_thm: thm -> unit
val prth: thm -> thm
val prthq: thm Sequence.seq -> thm Sequence.seq
val prths: thm list -> thm list
+ val read_ctyp: Sign.sg -> string -> ctyp
val read_instantiate: (string*string)list -> thm -> thm
val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
+ val read_insts:
+ Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
+ -> (indexname -> typ option) * (indexname -> sort option)
+ -> (string*string)list
+ -> (indexname*ctyp)list * (cterm*cterm)list
val reflexive_thm: thm
val revcut_rl: thm
val rewrite_goal_rule: bool*bool -> (meta_simpset -> thm -> thm option)
@@ -61,9 +71,10 @@
val show_hyps: bool ref
val size_of_thm: thm -> int
val standard: thm -> thm
+ val string_of_cterm: cterm -> string
+ val string_of_ctyp: ctyp -> string
val string_of_thm: thm -> string
val symmetric_thm: thm
- val pprint_thm: thm -> pprint_args -> unit
val transitive_thm: thm
val triv_forall_equality: thm
val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
@@ -82,6 +93,145 @@
(**** More derived rules and operations on theorems ****)
+fun cterm_fun f ct =
+ let val {sign,t,...} = rep_cterm ct in cterm_of sign (f t) end;
+
+fun read_ctyp sign = ctyp_of sign o Sign.read_typ(sign, K None);
+
+
+(** reading of instantiations **)
+
+fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
+ | _ => error("Lexical error in variable name " ^ quote (implode cs));
+
+fun absent ixn =
+ error("No such variable in term: " ^ Syntax.string_of_vname ixn);
+
+fun inst_failure ixn =
+ error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
+
+fun read_insts sign (rtypes,rsorts) (types,sorts) insts =
+let val {tsig,...} = Sign.rep_sg sign
+ fun split([],tvs,vs) = (tvs,vs)
+ | split((sv,st)::l,tvs,vs) = (case explode sv of
+ "'"::cs => split(l,(indexname cs,st)::tvs,vs)
+ | cs => split(l,tvs,(indexname cs,st)::vs));
+ val (tvs,vs) = split(insts,[],[]);
+ fun readT((a,i),st) =
+ let val ixn = ("'" ^ a,i);
+ val S = case rsorts ixn of Some S => S | None => absent ixn;
+ val T = Sign.read_typ (sign,sorts) st;
+ in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
+ else inst_failure ixn
+ end
+ val tye = map readT tvs;
+ fun add_cterm ((cts,tye), (ixn,st)) =
+ let val T = case rtypes ixn of
+ Some T => typ_subst_TVars tye T
+ | None => absent ixn;
+ val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
+ val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
+ in ((cv,ct)::cts,tye2 @ tye) end
+ val (cterms,tye') = foldl add_cterm (([],tye), vs);
+in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
+
+
+(*** Printing of theorems ***)
+
+(*If false, hypotheses are printed as dots*)
+val show_hyps = ref true;
+
+fun pretty_thm th =
+let val {sign, hyps, prop,...} = rep_thm th
+ val hsymbs = if null hyps then []
+ else if !show_hyps then
+ [Pretty.brk 2,
+ Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)]
+ else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @
+ [Pretty.str"]"];
+in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end;
+
+val string_of_thm = Pretty.string_of o pretty_thm;
+
+val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
+
+
+(** Top-level commands for printing theorems **)
+val print_thm = writeln o string_of_thm;
+
+fun prth th = (print_thm th; th);
+
+(*Print and return a sequence of theorems, separated by blank lines. *)
+fun prthq thseq =
+ (Sequence.prints (fn _ => print_thm) 100000 thseq;
+ thseq);
+
+(*Print and return a list of theorems, separated by blank lines. *)
+fun prths ths = (print_list_ln print_thm ths; ths);
+
+(*Other printing commands*)
+fun pprint_ctyp cT =
+ let val {sign,T} = rep_ctyp cT in Sign.pprint_typ sign T end;
+
+fun string_of_ctyp cT =
+ let val {sign,T} = rep_ctyp cT in Sign.string_of_typ sign T end;
+
+val print_ctyp = writeln o string_of_ctyp;
+
+fun pprint_cterm ct =
+ let val {sign,t,...} = rep_cterm ct in Sign.pprint_term sign t end;
+
+fun string_of_cterm ct =
+ let val {sign,t,...} = rep_cterm ct in Sign.string_of_term sign t end;
+
+val print_cterm = writeln o string_of_cterm;
+
+fun pretty_sg sg =
+ Pretty.lst ("{", "}") (map (Pretty.str o !) (#stamps (Sign.rep_sg sg)));
+
+val pprint_sg = Pretty.pprint o pretty_sg;
+
+val pprint_theory = pprint_sg o sign_of;
+
+val print_sg = writeln o Pretty.string_of o pretty_sg;
+val print_theory = print_sg o sign_of;
+
+
+(** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
+
+fun prettyprints es = writeln(Pretty.string_of(Pretty.blk(0,es)));
+
+fun print_goals maxgoals th : unit =
+let val {sign, hyps, prop,...} = rep_thm th;
+ fun printgoals (_, []) = ()
+ | printgoals (n, A::As) =
+ let val prettyn = Pretty.str(" " ^ string_of_int n ^ ". ");
+ val prettyA = Sign.pretty_term sign A
+ in prettyprints[prettyn,prettyA];
+ printgoals (n+1,As)
+ end;
+ fun prettypair(t,u) =
+ Pretty.blk(0, [Sign.pretty_term sign t, Pretty.str" =?=", Pretty.brk 1,
+ Sign.pretty_term sign u]);
+ fun printff [] = ()
+ | printff tpairs =
+ writeln("\nFlex-flex pairs:\n" ^
+ Pretty.string_of(Pretty.lst("","") (map prettypair tpairs)))
+ val (tpairs,As,B) = Logic.strip_horn(prop);
+ val ngoals = length As
+in
+ writeln (Sign.string_of_term sign B);
+ if ngoals=0 then writeln"No subgoals!"
+ else if ngoals>maxgoals
+ then (printgoals (1, take(maxgoals,As));
+ writeln("A total of " ^ string_of_int ngoals ^ " subgoals..."))
+ else printgoals (1, As);
+ printff tpairs
+end;
+
+(*"hook" for user interfaces: allows print_goals to be replaced*)
+val print_goals_ref = ref print_goals;
+
(*** Find the type (sort) associated with a (T)Var or (T)Free in a term
Used for establishing default types (of variables) and sorts (of
type variables) when reading another term.
@@ -111,7 +261,7 @@
fun forall_intr_frees th =
let val {prop,sign,...} = rep_thm th
in forall_intr_list
- (map (Sign.cterm_of sign) (sort atless (term_frees prop)))
+ (map (cterm_of sign) (sort atless (term_frees prop)))
th
end;
@@ -121,7 +271,7 @@
let val {prop,sign,...} = rep_thm th
in case prop of
Const("all",_) $ Abs(a,T,_) =>
- forall_elim (Sign.cterm_of sign (Var((a,i), T))) th
+ forall_elim (cterm_of sign (Var((a,i), T))) th
| _ => raise THM("forall_elim_var", i, [th])
end;
@@ -147,12 +297,12 @@
val inrs = add_term_tvars(prop,[]);
val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
- val ctye = map (fn (v,T) => (v,Sign.ctyp_of sign T)) tye;
+ val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
fun varpairs([],[]) = []
| varpairs((var as Var(v,T)) :: vars, b::bs) =
let val T' = typ_subst_TVars tye T
- in (Sign.cterm_of sign (Var(v,T')),
- Sign.cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
+ in (cterm_of sign (Var(v,T')),
+ cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
end
| varpairs _ = raise TERM("varpairs", []);
in instantiate (ctye, varpairs(vars,rev bs)) th end;
@@ -173,9 +323,9 @@
[ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ] *)
fun assume_ax thy sP =
let val sign = sign_of thy
- val prop = Logic.close_form (Sign.term_of (Sign.read_cterm sign
+ val prop = Logic.close_form (term_of (read_cterm sign
(sP, propT)))
- in forall_elim_vars 0 (assume (Sign.cterm_of sign prop)) end;
+ in forall_elim_vars 0 (assume (cterm_of sign prop)) end;
(*Resolution: exactly one resolvent must be produced.*)
fun tha RSN (i,thb) =
@@ -223,8 +373,7 @@
(*Instantiate theorem th, reading instantiations under signature sg*)
fun read_instantiate_sg sg sinsts th =
let val ts = types_sorts th;
- val instpair = Sign.read_insts sg ts ts sinsts
- in instantiate instpair th end;
+ in instantiate (read_insts sg ts ts sinsts) th end;
(*Instantiate theorem th, reading instantiations under theory of th*)
fun read_instantiate sinsts th =
@@ -235,8 +384,8 @@
Instantiates distinct Vars by terms, inferring type instantiations. *)
local
fun add_types ((ct,cu), (sign,tye)) =
- let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct
- and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu
+ let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
+ and {sign=signu, t=u, T= U, ...} = rep_cterm cu
val sign' = Sign.merge(sign, Sign.merge(signt, signu))
val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye)
handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
@@ -246,8 +395,8 @@
let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[]))
val tsig = #tsig(Sign.rep_sg sign);
fun instT(ct,cu) = let val inst = subst_TVars tye
- in (Sign.cfun inst ct, Sign.cfun inst cu) end
- fun ctyp2 (ix,T) = (ix, Sign.ctyp_of sign T)
+ in (cterm_fun inst ct, cterm_fun inst cu) end
+ fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
in instantiate (map ctyp2 tye, map instT ctpairs0) th end
handle TERM _ =>
raise THM("cterm_instantiate: incompatible signatures",0,[th])
@@ -255,88 +404,6 @@
end;
-(*** Printing of theorems ***)
-
-(*If false, hypotheses are printed as dots*)
-val show_hyps = ref true;
-
-fun pretty_thm th =
-let val {sign, hyps, prop,...} = rep_thm th
- val hsymbs = if null hyps then []
- else if !show_hyps then
- [Pretty.brk 2,
- Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)]
- else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @
- [Pretty.str"]"];
-in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end;
-
-val string_of_thm = Pretty.string_of o pretty_thm;
-
-val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
-
-
-(** Top-level commands for printing theorems **)
-val print_thm = writeln o string_of_thm;
-
-fun prth th = (print_thm th; th);
-
-(*Print and return a sequence of theorems, separated by blank lines. *)
-fun prthq thseq =
- (Sequence.prints (fn _ => print_thm) 100000 thseq;
- thseq);
-
-(*Print and return a list of theorems, separated by blank lines. *)
-fun prths ths = (print_list_ln print_thm ths; ths);
-
-(*Other printing commands*)
-val print_cterm = writeln o Sign.string_of_cterm;
-val print_ctyp = writeln o Sign.string_of_ctyp;
-fun pretty_sg sg =
- Pretty.lst ("{", "}") (map (Pretty.str o !) (#stamps (Sign.rep_sg sg)));
-
-val pprint_sg = Pretty.pprint o pretty_sg;
-
-val pprint_theory = pprint_sg o sign_of;
-
-val print_sg = writeln o Pretty.string_of o pretty_sg;
-val print_theory = print_sg o sign_of;
-
-
-(** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
-
-fun prettyprints es = writeln(Pretty.string_of(Pretty.blk(0,es)));
-
-fun print_goals maxgoals th : unit =
-let val {sign, hyps, prop,...} = rep_thm th;
- fun printgoals (_, []) = ()
- | printgoals (n, A::As) =
- let val prettyn = Pretty.str(" " ^ string_of_int n ^ ". ");
- val prettyA = Sign.pretty_term sign A
- in prettyprints[prettyn,prettyA];
- printgoals (n+1,As)
- end;
- fun prettypair(t,u) =
- Pretty.blk(0, [Sign.pretty_term sign t, Pretty.str" =?=", Pretty.brk 1,
- Sign.pretty_term sign u]);
- fun printff [] = ()
- | printff tpairs =
- writeln("\nFlex-flex pairs:\n" ^
- Pretty.string_of(Pretty.lst("","") (map prettypair tpairs)))
- val (tpairs,As,B) = Logic.strip_horn(prop);
- val ngoals = length As
-in
- writeln (Sign.string_of_term sign B);
- if ngoals=0 then writeln"No subgoals!"
- else if ngoals>maxgoals
- then (printgoals (1, take(maxgoals,As));
- writeln("A total of " ^ string_of_int ngoals ^ " subgoals..."))
- else printgoals (1, As);
- printff tpairs
-end;
-
-(*"hook" for user interfaces: allows print_goals to be replaced*)
-val print_goals_ref = ref print_goals;
-
(** theorem equality test is exported and used by BEST_FIRST **)
(*equality of signatures means exact identity -- by ref equality*)
@@ -363,42 +430,40 @@
val reflexive_thm =
- let val cx = Sign.cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),["logic"])))
+ let val cx = cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),["logic"])))
in Thm.reflexive cx end;
val symmetric_thm =
- let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT)
+ let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
val transitive_thm =
- let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT)
- val yz = Sign.read_cterm Sign.pure ("y::'a::logic == z",propT)
+ let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
+ val yz = read_cterm Sign.pure ("y::'a::logic == z",propT)
val xythm = Thm.assume xy and yzthm = Thm.assume yz
in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
-(** Below, a "conversion" has type sign->term->thm **)
+(** Below, a "conversion" has type cterm -> thm **)
+
+val refl_cimplies = reflexive (cterm_of Sign.pure implies);
(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
(*Do not rewrite flex-flex pairs*)
-fun goals_conv pred cv sign =
- let val triv = reflexive o Sign.fake_cterm_of sign
- fun gconv i t =
- let val (A,B) = Logic.dest_implies t
- val (thA,j) = case A of
- Const("=?=",_)$_$_ => (triv A,i)
- | _ => (if pred i then cv sign A else triv A, i+1)
- in combination (combination (triv implies) thA) (gconv j B) end
- handle TERM _ => triv t
+fun goals_conv pred cv =
+ let fun gconv i ct =
+ let val (A,B) = Thm.dest_cimplies ct
+ val (thA,j) = case term_of A of
+ Const("=?=",_)$_$_ => (reflexive A, i)
+ | _ => (if pred i then cv A else reflexive A, i+1)
+ in combination (combination refl_cimplies thA) (gconv j B) end
+ handle TERM _ => reflexive ct
in gconv 1 end;
(*Use a conversion to transform a theorem*)
-fun fconv_rule cv th =
- let val {sign,prop,...} = rep_thm th
- in equal_elim (cv sign prop) th end;
+fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
(*rewriting conversion*)
-fun rew_conv mode prover mss sign t =
- rewrite_cterm mode mss prover (Sign.fake_cterm_of sign t);
+fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
(*Rewrite a theorem*)
fun rewrite_rule thms =
@@ -420,11 +485,11 @@
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
fun equal_abs_elim ca eqth =
- let val {sign=signa, t=a, ...} = Sign.rep_cterm ca
+ let val {sign=signa, t=a, ...} = rep_cterm ca
and combth = combination eqth (reflexive ca)
val {sign,prop,...} = rep_thm eqth
val (abst,absu) = Logic.dest_equals prop
- val cterm = Sign.cterm_of (Sign.merge (sign,signa))
+ val cterm = cterm_of (Sign.merge (sign,signa))
in transitive (symmetric (beta_conversion (cterm (abst$a))))
(transitive combth (beta_conversion (cterm (absu$a))))
end
@@ -439,7 +504,7 @@
fun err th = raise THM("flexpair_inst: ", 0, [th])
fun flexpair_inst def th =
let val {prop = Const _ $ t $ u, sign,...} = rep_thm th
- val cterm = Sign.cterm_of sign
+ val cterm = cterm_of sign
fun cvar a = cterm(Var((a,0),alpha))
val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)]
def
@@ -459,17 +524,17 @@
(*** Some useful meta-theorems ***)
(*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = trivial(Sign.read_cterm Sign.pure ("PROP ?psi",propT));
+val asm_rl = trivial(read_cterm Sign.pure ("PROP ?psi",propT));
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
-val cut_rl = trivial(Sign.read_cterm Sign.pure
+val cut_rl = trivial(read_cterm Sign.pure
("PROP ?psi ==> PROP ?theta", propT));
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
[| PROP V; PROP V ==> PROP W |] ==> PROP W *)
val revcut_rl =
- let val V = Sign.read_cterm Sign.pure ("PROP V", propT)
- and VW = Sign.read_cterm Sign.pure ("PROP V ==> PROP W", propT);
+ let val V = read_cterm Sign.pure ("PROP V", propT)
+ and VW = read_cterm Sign.pure ("PROP V ==> PROP W", propT);
in standard (implies_intr V
(implies_intr VW
(implies_elim (assume VW) (assume V))))
@@ -477,9 +542,9 @@
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
val triv_forall_equality =
- let val V = Sign.read_cterm Sign.pure ("PROP V", propT)
- and QV = Sign.read_cterm Sign.pure ("!!x::'a. PROP V", propT)
- and x = Sign.read_cterm Sign.pure ("x", TFree("'a",["logic"]));
+ let val V = read_cterm Sign.pure ("PROP V", propT)
+ and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT)
+ and x = read_cterm Sign.pure ("x", TFree("'a",["logic"]));
in standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
(implies_intr V (forall_intr x (assume V))))
end;
--- a/src/Pure/sign.ML Tue Jan 18 07:53:35 1994 +0100
+++ b/src/Pure/sign.ML Tue Jan 18 13:46:08 1994 +0100
@@ -1,10 +1,9 @@
(* Title: Pure/sign.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
-The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
-typs under a signature).
+The abstract types "sg" of signatures
*)
signature SIGN =
@@ -14,11 +13,6 @@
structure Syntax: SYNTAX
sharing Symtab = Type.Symtab
type sg
- type cterm
- type ctyp
- val cfun: (term -> term) -> (cterm -> cterm)
- val cterm_of: sg -> term -> cterm
- val ctyp_of: sg -> typ -> ctyp
val extend: sg -> string ->
(class * class list) list * class list *
(string list * int) list *
@@ -27,32 +21,18 @@
(string list * string)list * Syntax.sext option -> sg
val merge: sg * sg -> sg
val pure: sg
- val read_cterm: sg -> string * typ -> cterm
- val read_ctyp: sg -> string -> ctyp
- val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
- -> (indexname -> typ option) * (indexname -> sort option)
- -> (string*string)list
- -> (indexname*ctyp)list * (cterm*cterm)list
val read_typ: sg * (indexname -> sort option) -> string -> typ
- val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
- val rep_ctyp: ctyp -> {T: typ, sign: sg}
val rep_sg: sg -> {tsig: Type.type_sig,
const_tab: typ Symtab.table,
syn: Syntax.syntax,
stamps: string ref list}
- val string_of_cterm: cterm -> string
- val string_of_ctyp: ctyp -> string
- val pprint_cterm: cterm -> pprint_args -> unit
- val pprint_ctyp: ctyp -> pprint_args -> unit
val string_of_term: sg -> term -> string
val string_of_typ: sg -> typ -> string
val subsig: sg * sg -> bool
val pprint_term: sg -> term -> pprint_args -> unit
val pprint_typ: sg -> typ -> pprint_args -> unit
- val term_of: cterm -> term
- val typ_of: ctyp -> typ
val pretty_term: sg -> term -> Syntax.Pretty.T
-val fake_cterm_of: sg -> term -> cterm
+ val term_errors: sg -> term -> string list
end;
functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
@@ -90,20 +70,20 @@
(*Check a term for errors. Are all constants and types valid in signature?
Does not check that term is well-typed!*)
fun term_errors (sign as Sg{tsig,const_tab,...}) =
-let val showtyp = string_of_typ sign
- fun terrs (Const (a,T), errs) =
- if valid_const tsig const_tab (a,T)
- then Type.type_errors tsig (T,errs)
- else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
- | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
- | terrs (Var ((a,i),T), errs) =
- if i>=0 then Type.type_errors tsig (T,errs)
- else ("Negative index for Var: " ^ a) :: errs
- | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
- | terrs (Abs (_,T,t), errs) =
- Type.type_errors tsig (T,terrs(t,errs))
- | terrs (f$t, errs) = terrs(f, terrs (t,errs))
-in terrs end;
+ let val showtyp = string_of_typ sign
+ fun terrs (Const (a,T), errs) =
+ if valid_const tsig const_tab (a,T)
+ then Type.type_errors tsig (T,errs)
+ else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
+ | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
+ | terrs (Var ((a,i),T), errs) =
+ if i>=0 then Type.type_errors tsig (T,errs)
+ else ("Negative index for Var: " ^ a) :: errs
+ | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
+ | terrs (Abs (_,T,t), errs) =
+ Type.type_errors tsig (T,terrs(t,errs))
+ | terrs (f$t, errs) = terrs(f, terrs (t,errs))
+ in fn t => terrs(t,[]) end;
@@ -238,44 +218,12 @@
-(**** CERTIFIED TYPES ****)
-
-
-(*Certified typs under a signature*)
-datatype ctyp = Ctyp of {sign: sg, T: typ};
-
-fun rep_ctyp(Ctyp ctyp) = ctyp;
-
-fun typ_of (Ctyp{sign,T}) = T;
-
-fun ctyp_of (sign as Sg{tsig,...}) T =
- case Type.type_errors tsig (T,[]) of
- [] => Ctyp{sign= sign,T= T}
- | errs => error (cat_lines ("Error in type:" :: errs));
-
fun read_typ(Sg{tsig,syn,...}, defS) s =
let val term = Syntax.read syn Syntax.typeT s;
val S0 = Type.defaultS tsig;
fun defS0 s = case defS s of Some S => S | None => S0;
in Syntax.typ_of_term defS0 term end;
-fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
-
-fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;
-
-fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;
-
-
-(**** CERTIFIED TERMS ****)
-
-(*Certified terms under a signature, with checked typ and maxidx of Vars*)
-datatype cterm = Cterm of {sign: sg, t: term, T: typ, maxidx: int};
-
-fun rep_cterm (Cterm args) = args;
-
-(*Return the underlying term*)
-fun term_of (Cterm{sign,t,T,maxidx}) = t;
-
(** pretty printing of terms **)
fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
@@ -284,78 +232,5 @@
fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
-fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;
-
-fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;
-
-(*Create a cterm by checking a "raw" term with respect to a signature*)
-fun cterm_of sign t =
- case term_errors sign (t,[]) of
- [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
- | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
-
-(*The only use is a horrible hack in the simplifier!*)
-fun fake_cterm_of sign t =
- Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
-
-fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
-
-(*Lexing, parsing, polymorphic typechecking of a term.*)
-fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
- (a,T) =
- let val showtyp = string_of_typ sign
- and showterm = string_of_term sign
- fun termerr [] = ""
- | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
- | termerr ts = "\nInvolving these terms:\n" ^
- cat_lines (map showterm ts)
- val t = Syntax.read syn T a;
- val (t',tye) = Type.infer_types (tsig, const_tab, types,
- sorts, showtyp, T, t)
- handle TYPE (msg, Ts, ts) =>
- error ("Type checking error: " ^ msg ^ "\n" ^
- cat_lines (map showtyp Ts) ^ termerr ts)
- in (cterm_of sign t', tye)
- end
- handle TERM (msg, _) => error ("Error: " ^ msg);
-
-
-fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
-
-(** reading of instantiations **)
-
-fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
- | _ => error("Lexical error in variable name " ^ quote (implode cs));
-
-fun absent ixn =
- error("No such variable in term: " ^ Syntax.string_of_vname ixn);
-
-fun inst_failure ixn =
- error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
-
-fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
-let fun split([],tvs,vs) = (tvs,vs)
- | split((sv,st)::l,tvs,vs) = (case explode sv of
- "'"::cs => split(l,(indexname cs,st)::tvs,vs)
- | cs => split(l,tvs,(indexname cs,st)::vs));
- val (tvs,vs) = split(insts,[],[]);
- fun readT((a,i),st) =
- let val ixn = ("'" ^ a,i);
- val S = case rsorts ixn of Some S => S | None => absent ixn;
- val T = read_typ (sign,sorts) st;
- in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
- else inst_failure ixn
- end
- val tye = map readT tvs;
- fun add_cterm ((cts,tye), (ixn,st)) =
- let val T = case rtypes ixn of
- Some T => typ_subst_TVars tye T
- | None => absent ixn;
- val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
- val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
- in ((cv,ct)::cts,tye2 @ tye) end
- val (cterms,tye') = foldl add_cterm (([],tye), vs);
-in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
-
end;
--- a/src/Pure/thm.ML Tue Jan 18 07:53:35 1994 +0100
+++ b/src/Pure/thm.ML Tue Jan 18 13:46:08 1994 +0100
@@ -1,9 +1,12 @@
(* Title: thm
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
+ Copyright 1994 University of Cambridge
+
+NO REP_CTERM!!
The abstract types "theory" and "thm"
+Also "cterm" / "ctyp" (certified terms / typs under a signature).
*)
signature THM =
@@ -11,25 +14,38 @@
structure Envir : ENVIR
structure Sequence : SEQUENCE
structure Sign : SIGN
+ type cterm
+ type ctyp
type meta_simpset
type theory
type thm
exception THM of string * int * thm list
exception THEORY of string * theory list
exception SIMPLIFIER of string * thm
- val abstract_rule: string -> Sign.cterm -> thm -> thm
+ (*Certified terms/types; previously in sign.ML*)
+ val cterm_of: Sign.sg -> term -> cterm
+ val ctyp_of: Sign.sg -> typ -> ctyp
+ val read_cterm: Sign.sg -> string * typ -> cterm
+ val rep_cterm: cterm -> {T: typ, t: term, sign: Sign.sg, maxidx: int}
+ val rep_ctyp: ctyp -> {T: typ, sign: Sign.sg}
+ val term_of: cterm -> term
+ val typ_of: ctyp -> typ
+ (*End of cterm/ctyp functions*)
+ val abstract_rule: string -> cterm -> thm -> thm
val add_congs: meta_simpset * thm list -> meta_simpset
val add_prems: meta_simpset * thm list -> meta_simpset
val add_simps: meta_simpset * thm list -> meta_simpset
- val assume: Sign.cterm -> thm
+ val assume: cterm -> thm
val assumption: int -> thm -> thm Sequence.seq
val axioms_of: theory -> (string * thm) list
- val beta_conversion: Sign.cterm -> thm
+ val beta_conversion: cterm -> thm
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Sequence.seq
val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq
val combination: thm -> thm -> thm
val concl_of: thm -> term
+ val cprop_of: thm -> cterm
val del_simps: meta_simpset * thm list -> meta_simpset
+ val dest_cimplies: cterm -> cterm*cterm
val dest_state: thm * int -> (term*term)list * term list * term * term
val empty_mss: meta_simpset
val eq_assumption: int -> thm -> thm
@@ -45,14 +61,14 @@
val extensional: thm -> thm
val flexflex_rule: thm -> thm Sequence.seq
val flexpair_def: thm
- val forall_elim: Sign.cterm -> thm -> thm
- val forall_intr: Sign.cterm -> thm -> thm
+ val forall_elim: cterm -> thm -> thm
+ val forall_intr: cterm -> thm -> thm
val freezeT: thm -> thm
val get_axiom: theory -> string -> thm
val implies_elim: thm -> thm -> thm
- val implies_intr: Sign.cterm -> thm -> thm
+ val implies_intr: cterm -> thm -> thm
val implies_intr_hyps: thm -> thm
- val instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list
+ val instantiate: (indexname*ctyp)list * (cterm*cterm)list
-> thm -> thm
val lift_rule: (thm * int) -> thm -> thm
val merge_theories: theory * theory -> theory
@@ -63,12 +79,15 @@
val prems_of: thm -> term list
val prems_of_mss: meta_simpset -> thm list
val pure_thy: theory
- val reflexive: Sign.cterm -> thm
+ val read_def_cterm :
+ Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
+ string * typ -> cterm * (indexname * typ) list
+ val reflexive: cterm -> thm
val rename_params_rule: string list * int -> thm -> thm
val rep_thm: thm -> {prop: term, hyps: term list, maxidx: int, sign: Sign.sg}
val rewrite_cterm:
bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option)
- -> Sign.cterm -> thm
+ -> cterm -> thm
val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
val sign_of: theory -> Sign.sg
val syn_of: theory -> Sign.Syntax.syntax
@@ -78,7 +97,7 @@
val tpairs_of: thm -> (term*term)list
val trace_simp: bool ref
val transitive: thm -> thm -> thm
- val trivial: Sign.cterm -> thm
+ val trivial: cterm -> thm
val varifyT: thm -> thm
end;
@@ -87,7 +106,7 @@
functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN
and Net:NET
sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)
- (*: THM*) = (* FIXME *)
+ : THM =
struct
structure Sequence = Unify.Sequence;
structure Envir = Unify.Envir;
@@ -97,7 +116,67 @@
structure Symtab = Sign.Symtab;
-(*Meta-theorems*)
+(** Certified Types **)
+
+
+(*Certified typs under a signature*)
+datatype ctyp = Ctyp of {sign: Sign.sg, T: typ};
+
+fun rep_ctyp(Ctyp ctyp) = ctyp;
+fun typ_of (Ctyp{sign,T}) = T;
+
+fun ctyp_of sign T =
+ case Type.type_errors (#tsig(Sign.rep_sg sign)) (T,[]) of
+ [] => Ctyp{sign= sign,T= T}
+ | errs => error (cat_lines ("Error in type:" :: errs));
+
+(** Certified Terms **)
+
+(*Certified terms under a signature, with checked typ and maxidx of Vars*)
+datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int};
+
+fun rep_cterm (Cterm args) = args;
+
+(*Return the underlying term*)
+fun term_of (Cterm{t,...}) = t;
+
+(*Create a cterm by checking a "raw" term with respect to a signature*)
+fun cterm_of sign t =
+ case Sign.term_errors sign t of
+ [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
+ | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
+
+(*dest_implies for cterms. Note T=prop below*)
+fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>",_) $ A $ B}) =
+ (Cterm{sign=sign, T=T, maxidx=maxidx, t=A},
+ Cterm{sign=sign, T=T, maxidx=maxidx, t=B})
+ | dest_cimplies ct = raise TERM("dest_cimplies", [term_of ct]);
+
+(** Reading of cterms -- needed twice below! **)
+
+(*Lexing, parsing, polymorphic typechecking of a term.*)
+fun read_def_cterm (sign, types, sorts) (a,T) =
+ let val {tsig, const_tab, syn,...} = Sign.rep_sg sign
+ val showtyp = Sign.string_of_typ sign
+ and showterm = Sign.string_of_term sign
+ fun termerr [] = ""
+ | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
+ | termerr ts = "\nInvolving these terms:\n" ^
+ cat_lines (map showterm ts)
+ val t = Syntax.read syn T a;
+ val (t',tye) = Type.infer_types (tsig, const_tab, types,
+ sorts, showtyp, T, t)
+ handle TYPE (msg, Ts, ts) =>
+ error ("Type checking error: " ^ msg ^ "\n" ^
+ cat_lines (map showtyp Ts) ^ termerr ts)
+ in (cterm_of sign t', tye)
+ end
+ handle TERM (msg, _) => error ("Error: " ^ msg);
+
+fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
+
+(**** META-THEOREMS ****)
+
datatype thm = Thm of
{sign: Sign.sg, maxidx: int, hyps: term list, prop: term};
@@ -120,6 +199,10 @@
(*maps object-rule to conclusion *)
fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop;
+(*The statement of any Thm is a Cterm*)
+fun cprop_of (Thm{sign,maxidx,hyps,prop}) =
+ Cterm{sign=sign, maxidx=maxidx, T=propT, t=prop};
+
(*Stamps associated with a signature*)
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
@@ -168,7 +251,7 @@
(*The assumption rule A|-A in a theory *)
fun assume ct : thm =
- let val {sign, t=prop, T, maxidx} = Sign.rep_cterm ct
+ let val {sign, t=prop, T, maxidx} = rep_cterm ct
in if T<>propT then
raise THM("assume: assumptions must have type prop", 0, [])
else if maxidx <> ~1 then
@@ -182,7 +265,7 @@
-------
A ==> B *)
fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =
- let val {sign=signA, t=A, T, maxidx=maxidxA} = Sign.rep_cterm cA
+ let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA
in if T<>propT then
raise THM("implies_intr: assumptions must have type prop", 0, [thB])
else Thm{sign= Sign.merge (sign,signA), maxidx= max[maxidxA, maxidx],
@@ -215,7 +298,7 @@
------
!!x.A *)
fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =
- let val x = Sign.term_of cx;
+ let val x = term_of cx;
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,
prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
in case x of
@@ -232,7 +315,7 @@
--------
A[t/x] *)
fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =
- let val {sign=signt, t, T, maxidx=maxt} = Sign.rep_cterm ct
+ let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
in case prop of
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
if T<>qary then
@@ -251,13 +334,13 @@
(*Definition of the relation =?= *)
val flexpair_def =
Thm{sign= Sign.pure, hyps= [], maxidx= 0,
- prop= Sign.term_of
- (Sign.read_cterm Sign.pure
+ prop= term_of
+ (read_cterm Sign.pure
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
(*The reflexivity rule: maps t to the theorem t==t *)
fun reflexive ct =
- let val {sign, t, T, maxidx} = Sign.rep_cterm ct
+ let val {sign, t, T, maxidx} = rep_cterm ct
in Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}
end;
@@ -289,7 +372,7 @@
(*Beta-conversion: maps (%(x)t)(u) to the theorem (%(x)t)(u) == t[u/x] *)
fun beta_conversion ct =
- let val {sign, t, T, maxidx} = Sign.rep_cterm ct
+ let val {sign, t, T, maxidx} = rep_cterm ct
in case t of
Abs(_,_,bodt) $ u =>
Thm{sign= sign, hyps= [],
@@ -326,7 +409,7 @@
----------------
%(x)t == %(x)u *)
fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =
- let val x = Sign.term_of cx;
+ let val x = term_of cx;
val (t,u) = Logic.dest_equals prop
handle TERM _ =>
raise THM("abstract_rule: premise not an equality", 0, [th])
@@ -431,14 +514,14 @@
(*For instantiate: process pair of cterms, merge theories*)
fun add_ctpair ((ct,cu), (sign,tpairs)) =
- let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct
- and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu
+ let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
+ and {sign=signu, t=u, T= U, ...} = rep_cterm cu
in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
else raise TYPE("add_ctpair", [T,U], [t,u])
end;
fun add_ctyp ((v,ctyp), (sign',vTs)) =
- let val {T,sign} = Sign.rep_ctyp ctyp
+ let val {T,sign} = rep_ctyp ctyp
in (Sign.merge(sign,sign'), (v,T)::vTs) end;
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
@@ -475,7 +558,7 @@
(*The trivial implication A==>A, justified by assume and forall rules.
A can contain Vars, not so for assume! *)
fun trivial ct : thm =
- let val {sign, t=A, T, maxidx} = Sign.rep_cterm ct
+ let val {sign, t=A, T, maxidx} = rep_cterm ct
in if T<>propT then
raise THM("trivial: the term must have type prop", 0, [])
else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
@@ -756,7 +839,7 @@
(*Converts Frees to Vars: axioms can be written without question marks*)
fun prepare_axiom sign sP =
- Logic.varify (Sign.term_of (Sign.read_cterm sign (sP,propT)));
+ Logic.varify (term_of (read_cterm sign (sP,propT)));
(*Read an axiom for a new theory*)
fun read_ax sign (a, sP) : string*thm =
@@ -803,11 +886,11 @@
exception SIMPLIFIER of string * thm;
-fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t));
+fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
val trace_simp = ref false;
-fun trace_term a sg t = if !trace_simp then prtm a sg t else ();
+fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
@@ -1010,7 +1093,7 @@
(*** FIXME: check that #primes(mss) does not "occur" in ct alread ***)
fun rewrite_cterm mode mss prover ct =
- let val {sign, t, T, maxidx} = Sign.rep_cterm ct;
+ let val {sign, t, T, maxidx} = rep_cterm ct;
val (hyps,u) = bottomc (mode,prover,sign) mss ([],t);
val prop = Logic.mk_equals(t,u)
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop}