# HG changeset patch # User lcp # Date 758897168 -3600 # Node ID 4002c4cd450c0e579b53956b21ae7bf57a50bc61 # Parent 4f43430f226ea44ca5181855cb72b9e497504f09 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. diff -r 4f43430f226e -r 4002c4cd450c src/Pure/drule.ML --- 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; diff -r 4f43430f226e -r 4002c4cd450c src/Pure/sign.ML --- 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; diff -r 4f43430f226e -r 4002c4cd450c src/Pure/thm.ML --- 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}