src/Pure/thm.ML
changeset 229 4002c4cd450c
parent 225 76f60e6400e8
child 242 8fe3e66abf0c
     1.1 --- a/src/Pure/thm.ML	Tue Jan 18 07:53:35 1994 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Jan 18 13:46:08 1994 +0100
     1.3 @@ -1,9 +1,12 @@
     1.4  (*  Title: 	thm
     1.5      ID:         $Id$
     1.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 +    Copyright   1994  University of Cambridge
     1.9 +
    1.10 +NO REP_CTERM!!
    1.11  
    1.12  The abstract types "theory" and "thm"
    1.13 +Also "cterm" / "ctyp" (certified terms / typs under a signature).
    1.14  *)
    1.15  
    1.16  signature THM = 
    1.17 @@ -11,25 +14,38 @@
    1.18    structure Envir : ENVIR
    1.19    structure Sequence : SEQUENCE
    1.20    structure Sign : SIGN
    1.21 +  type cterm
    1.22 +  type ctyp
    1.23    type meta_simpset
    1.24    type theory
    1.25    type thm
    1.26    exception THM of string * int * thm list
    1.27    exception THEORY of string * theory list
    1.28    exception SIMPLIFIER of string * thm
    1.29 -  val abstract_rule: string -> Sign.cterm -> thm -> thm
    1.30 +  (*Certified terms/types; previously in sign.ML*)
    1.31 +  val cterm_of: Sign.sg -> term -> cterm
    1.32 +  val ctyp_of: Sign.sg -> typ -> ctyp
    1.33 +  val read_cterm: Sign.sg -> string * typ -> cterm
    1.34 +  val rep_cterm: cterm -> {T: typ, t: term, sign: Sign.sg, maxidx: int}
    1.35 +  val rep_ctyp: ctyp -> {T: typ, sign: Sign.sg}
    1.36 +  val term_of: cterm -> term
    1.37 +  val typ_of: ctyp -> typ
    1.38 +  (*End of cterm/ctyp functions*)  
    1.39 +  val abstract_rule: string -> cterm -> thm -> thm
    1.40    val add_congs: meta_simpset * thm list -> meta_simpset
    1.41    val add_prems: meta_simpset * thm list -> meta_simpset
    1.42    val add_simps: meta_simpset * thm list -> meta_simpset
    1.43 -  val assume: Sign.cterm -> thm
    1.44 +  val assume: cterm -> thm
    1.45    val assumption: int -> thm -> thm Sequence.seq   
    1.46    val axioms_of: theory -> (string * thm) list
    1.47 -  val beta_conversion: Sign.cterm -> thm   
    1.48 +  val beta_conversion: cterm -> thm   
    1.49    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Sequence.seq   
    1.50    val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq   
    1.51    val combination: thm -> thm -> thm   
    1.52    val concl_of: thm -> term   
    1.53 +  val cprop_of: thm -> cterm
    1.54    val del_simps: meta_simpset * thm list -> meta_simpset
    1.55 +  val dest_cimplies: cterm -> cterm*cterm
    1.56    val dest_state: thm * int -> (term*term)list * term list * term * term
    1.57    val empty_mss: meta_simpset
    1.58    val eq_assumption: int -> thm -> thm   
    1.59 @@ -45,14 +61,14 @@
    1.60    val extensional: thm -> thm   
    1.61    val flexflex_rule: thm -> thm Sequence.seq  
    1.62    val flexpair_def: thm 
    1.63 -  val forall_elim: Sign.cterm -> thm -> thm
    1.64 -  val forall_intr: Sign.cterm -> thm -> thm
    1.65 +  val forall_elim: cterm -> thm -> thm
    1.66 +  val forall_intr: cterm -> thm -> thm
    1.67    val freezeT: thm -> thm
    1.68    val get_axiom: theory -> string -> thm
    1.69    val implies_elim: thm -> thm -> thm
    1.70 -  val implies_intr: Sign.cterm -> thm -> thm
    1.71 +  val implies_intr: cterm -> thm -> thm
    1.72    val implies_intr_hyps: thm -> thm
    1.73 -  val instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list 
    1.74 +  val instantiate: (indexname*ctyp)list * (cterm*cterm)list 
    1.75                     -> thm -> thm
    1.76    val lift_rule: (thm * int) -> thm -> thm
    1.77    val merge_theories: theory * theory -> theory
    1.78 @@ -63,12 +79,15 @@
    1.79    val prems_of: thm -> term list
    1.80    val prems_of_mss: meta_simpset -> thm list
    1.81    val pure_thy: theory
    1.82 -  val reflexive: Sign.cterm -> thm 
    1.83 +  val read_def_cterm :
    1.84 +         Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    1.85 +         string * typ -> cterm * (indexname * typ) list
    1.86 +   val reflexive: cterm -> thm 
    1.87    val rename_params_rule: string list * int -> thm -> thm
    1.88    val rep_thm: thm -> {prop: term, hyps: term list, maxidx: int, sign: Sign.sg}
    1.89    val rewrite_cterm:
    1.90           bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option)
    1.91 -           -> Sign.cterm -> thm
    1.92 +           -> cterm -> thm
    1.93    val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
    1.94    val sign_of: theory -> Sign.sg   
    1.95    val syn_of: theory -> Sign.Syntax.syntax
    1.96 @@ -78,7 +97,7 @@
    1.97    val tpairs_of: thm -> (term*term)list
    1.98    val trace_simp: bool ref
    1.99    val transitive: thm -> thm -> thm
   1.100 -  val trivial: Sign.cterm -> thm
   1.101 +  val trivial: cterm -> thm
   1.102    val varifyT: thm -> thm
   1.103    end;
   1.104  
   1.105 @@ -87,7 +106,7 @@
   1.106  functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN
   1.107                        and Net:NET
   1.108                  sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)
   1.109 -        (*: THM*) = (* FIXME *)
   1.110 +        : THM =
   1.111  struct
   1.112  structure Sequence = Unify.Sequence;
   1.113  structure Envir = Unify.Envir;
   1.114 @@ -97,7 +116,67 @@
   1.115  structure Symtab = Sign.Symtab;
   1.116  
   1.117  
   1.118 -(*Meta-theorems*)
   1.119 +(** Certified Types **)
   1.120 +
   1.121 +
   1.122 +(*Certified typs under a signature*)
   1.123 +datatype ctyp = Ctyp of {sign: Sign.sg,  T: typ};
   1.124 +
   1.125 +fun rep_ctyp(Ctyp ctyp) = ctyp;
   1.126 +fun typ_of (Ctyp{sign,T}) = T;
   1.127 +
   1.128 +fun ctyp_of sign T =
   1.129 +    case Type.type_errors (#tsig(Sign.rep_sg sign)) (T,[]) of
   1.130 +      []   => Ctyp{sign= sign,T= T}
   1.131 +    | errs =>  error (cat_lines ("Error in type:" :: errs));
   1.132 +
   1.133 +(** Certified Terms **)
   1.134 +
   1.135 +(*Certified terms under a signature, with checked typ and maxidx of Vars*)
   1.136 +datatype cterm = Cterm of {sign: Sign.sg,  t: term,  T: typ,  maxidx: int};
   1.137 +
   1.138 +fun rep_cterm (Cterm args) = args;
   1.139 +
   1.140 +(*Return the underlying term*)
   1.141 +fun term_of (Cterm{t,...}) = t;
   1.142 +
   1.143 +(*Create a cterm by checking a "raw" term with respect to a signature*)
   1.144 +fun cterm_of sign t =
   1.145 +  case  Sign.term_errors sign t  of
   1.146 +      [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
   1.147 +    | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
   1.148 +
   1.149 +(*dest_implies for cterms.  Note T=prop below*)
   1.150 +fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>",_) $ A $ B}) = 
   1.151 +       (Cterm{sign=sign, T=T, maxidx=maxidx, t=A},
   1.152 +	Cterm{sign=sign, T=T, maxidx=maxidx, t=B})
   1.153 +  | dest_cimplies ct = raise TERM("dest_cimplies", [term_of ct]);
   1.154 +
   1.155 +(** Reading of cterms -- needed twice below! **)
   1.156 +
   1.157 +(*Lexing, parsing, polymorphic typechecking of a term.*)
   1.158 +fun read_def_cterm (sign, types, sorts) (a,T) =
   1.159 +  let val {tsig, const_tab, syn,...} = Sign.rep_sg sign
   1.160 +      val showtyp = Sign.string_of_typ sign
   1.161 +      and showterm = Sign.string_of_term sign
   1.162 +      fun termerr [] = ""
   1.163 +        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
   1.164 +        | termerr ts = "\nInvolving these terms:\n" ^
   1.165 +                       cat_lines (map showterm ts)
   1.166 +      val t = Syntax.read syn T a;
   1.167 +      val (t',tye) = Type.infer_types (tsig, const_tab, types,
   1.168 +                                       sorts, showtyp, T, t)
   1.169 +                  handle TYPE (msg, Ts, ts) =>
   1.170 +          error ("Type checking error: " ^ msg ^ "\n" ^
   1.171 +                  cat_lines (map showtyp Ts) ^ termerr ts)
   1.172 +  in (cterm_of sign t', tye)
   1.173 +  end
   1.174 +  handle TERM (msg, _) => error ("Error: " ^  msg);
   1.175 +
   1.176 +fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
   1.177 +
   1.178 +(**** META-THEOREMS ****)
   1.179 +
   1.180  datatype thm = Thm of
   1.181      {sign: Sign.sg,  maxidx: int,  hyps: term list,  prop: term};
   1.182  
   1.183 @@ -120,6 +199,10 @@
   1.184  (*maps object-rule to conclusion *)
   1.185  fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop;
   1.186  
   1.187 +(*The statement of any Thm is a Cterm*)
   1.188 +fun cprop_of (Thm{sign,maxidx,hyps,prop}) = 
   1.189 +	Cterm{sign=sign, maxidx=maxidx, T=propT, t=prop};
   1.190 +
   1.191  (*Stamps associated with a signature*)
   1.192  val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
   1.193  
   1.194 @@ -168,7 +251,7 @@
   1.195  
   1.196  (*The assumption rule A|-A in a theory  *)
   1.197  fun assume ct : thm = 
   1.198 -  let val {sign, t=prop, T, maxidx} = Sign.rep_cterm ct
   1.199 +  let val {sign, t=prop, T, maxidx} = rep_cterm ct
   1.200    in  if T<>propT then  
   1.201  	raise THM("assume: assumptions must have type prop", 0, [])
   1.202        else if maxidx <> ~1 then
   1.203 @@ -182,7 +265,7 @@
   1.204  	      -------
   1.205  	      A ==> B    *)
   1.206  fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =
   1.207 -  let val {sign=signA, t=A, T, maxidx=maxidxA} = Sign.rep_cterm cA
   1.208 +  let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA
   1.209    in  if T<>propT then
   1.210  	raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   1.211        else Thm{sign= Sign.merge (sign,signA),  maxidx= max[maxidxA, maxidx], 
   1.212 @@ -215,7 +298,7 @@
   1.213     ------
   1.214     !!x.A       *)
   1.215  fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =
   1.216 -  let val x = Sign.term_of cx;
   1.217 +  let val x = term_of cx;
   1.218        fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   1.219  	                    prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
   1.220    in  case x of
   1.221 @@ -232,7 +315,7 @@
   1.222  	     --------
   1.223  	      A[t/x]     *)
   1.224  fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =
   1.225 -  let val {sign=signt, t, T, maxidx=maxt} = Sign.rep_cterm ct
   1.226 +  let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
   1.227    in  case prop of
   1.228  	  Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   1.229  	    if T<>qary then
   1.230 @@ -251,13 +334,13 @@
   1.231  (*Definition of the relation =?= *)
   1.232  val flexpair_def =
   1.233    Thm{sign= Sign.pure, hyps= [], maxidx= 0, 
   1.234 -      prop= Sign.term_of 
   1.235 -	      (Sign.read_cterm Sign.pure 
   1.236 +      prop= term_of 
   1.237 +	      (read_cterm Sign.pure 
   1.238  	         ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
   1.239  
   1.240  (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   1.241  fun reflexive ct = 
   1.242 -  let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   1.243 +  let val {sign, t, T, maxidx} = rep_cterm ct
   1.244    in  Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}
   1.245    end;
   1.246  
   1.247 @@ -289,7 +372,7 @@
   1.248  
   1.249  (*Beta-conversion: maps (%(x)t)(u) to the theorem  (%(x)t)(u) == t[u/x]   *)
   1.250  fun beta_conversion ct = 
   1.251 -  let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   1.252 +  let val {sign, t, T, maxidx} = rep_cterm ct
   1.253    in  case t of
   1.254  	  Abs(_,_,bodt) $ u => 
   1.255  	    Thm{sign= sign,  hyps= [],  
   1.256 @@ -326,7 +409,7 @@
   1.257      ----------------
   1.258        %(x)t == %(x)u     *)
   1.259  fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =
   1.260 -  let val x = Sign.term_of cx;
   1.261 +  let val x = term_of cx;
   1.262        val (t,u) = Logic.dest_equals prop  
   1.263  	    handle TERM _ =>
   1.264  		raise THM("abstract_rule: premise not an equality", 0, [th])
   1.265 @@ -431,14 +514,14 @@
   1.266  
   1.267  (*For instantiate: process pair of cterms, merge theories*)
   1.268  fun add_ctpair ((ct,cu), (sign,tpairs)) =
   1.269 -  let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct
   1.270 -      and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu
   1.271 +  let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
   1.272 +      and {sign=signu, t=u, T= U, ...} = rep_cterm cu
   1.273    in  if T=U  then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
   1.274        else raise TYPE("add_ctpair", [T,U], [t,u])
   1.275    end;
   1.276  
   1.277  fun add_ctyp ((v,ctyp), (sign',vTs)) =
   1.278 -  let val {T,sign} = Sign.rep_ctyp ctyp
   1.279 +  let val {T,sign} = rep_ctyp ctyp
   1.280    in (Sign.merge(sign,sign'), (v,T)::vTs) end;
   1.281  
   1.282  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   1.283 @@ -475,7 +558,7 @@
   1.284  (*The trivial implication A==>A, justified by assume and forall rules.
   1.285    A can contain Vars, not so for assume!   *)
   1.286  fun trivial ct : thm = 
   1.287 -  let val {sign, t=A, T, maxidx} = Sign.rep_cterm ct
   1.288 +  let val {sign, t=A, T, maxidx} = rep_cterm ct
   1.289    in  if T<>propT then  
   1.290  	    raise THM("trivial: the term must have type prop", 0, [])
   1.291        else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
   1.292 @@ -756,7 +839,7 @@
   1.293  
   1.294  (*Converts Frees to Vars: axioms can be written without question marks*)
   1.295  fun prepare_axiom sign sP =
   1.296 -    Logic.varify (Sign.term_of (Sign.read_cterm sign (sP,propT)));
   1.297 +    Logic.varify (term_of (read_cterm sign (sP,propT)));
   1.298  
   1.299  (*Read an axiom for a new theory*)
   1.300  fun read_ax sign (a, sP) : string*thm =
   1.301 @@ -803,11 +886,11 @@
   1.302  
   1.303  exception SIMPLIFIER of string * thm;
   1.304  
   1.305 -fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t));
   1.306 +fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
   1.307  
   1.308  val trace_simp = ref false;
   1.309  
   1.310 -fun trace_term a sg t = if !trace_simp then prtm a sg t else ();
   1.311 +fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
   1.312  
   1.313  fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
   1.314  
   1.315 @@ -1010,7 +1093,7 @@
   1.316  
   1.317  (*** FIXME: check that #primes(mss) does not "occur" in ct alread ***)
   1.318  fun rewrite_cterm mode mss prover ct =
   1.319 -  let val {sign, t, T, maxidx} = Sign.rep_cterm ct;
   1.320 +  let val {sign, t, T, maxidx} = rep_cterm ct;
   1.321        val (hyps,u) = bottomc (mode,prover,sign) mss ([],t);
   1.322        val prop = Logic.mk_equals(t,u)
   1.323    in  Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop}