Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
authorlcp
Tue Jan 18 13:46:08 1994 +0100 (1994-01-18)
changeset 2294002c4cd450c
parent 228 4f43430f226e
child 230 ec8a2b6aa8a7
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.
src/Pure/drule.ML
src/Pure/sign.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/drule.ML	Tue Jan 18 07:53:35 1994 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Jan 18 13:46:08 1994 +0100
     1.3 @@ -14,40 +14,50 @@
     1.4    local open Thm  in
     1.5    val asm_rl: thm
     1.6    val assume_ax: theory -> string -> thm
     1.7 +  val cterm_fun: (term -> term) -> (cterm -> cterm)
     1.8    val COMP: thm * thm -> thm
     1.9    val compose: thm * int * thm -> thm list
    1.10 -  val cterm_instantiate: (Sign.cterm*Sign.cterm)list -> thm -> thm
    1.11 +  val cterm_instantiate: (cterm*cterm)list -> thm -> thm
    1.12    val cut_rl: thm
    1.13 -  val equal_abs_elim: Sign.cterm  -> thm -> thm
    1.14 -  val equal_abs_elim_list: Sign.cterm list -> thm -> thm
    1.15 +  val equal_abs_elim: cterm  -> thm -> thm
    1.16 +  val equal_abs_elim_list: cterm list -> thm -> thm
    1.17    val eq_sg: Sign.sg * Sign.sg -> bool
    1.18    val eq_thm: thm * thm -> bool
    1.19    val eq_thm_sg: thm * thm -> bool
    1.20 -  val flexpair_abs_elim_list: Sign.cterm list -> thm -> thm
    1.21 -  val forall_intr_list: Sign.cterm list -> thm -> thm
    1.22 +  val flexpair_abs_elim_list: cterm list -> thm -> thm
    1.23 +  val forall_intr_list: cterm list -> thm -> thm
    1.24    val forall_intr_frees: thm -> thm
    1.25 -  val forall_elim_list: Sign.cterm list -> thm -> thm
    1.26 +  val forall_elim_list: cterm list -> thm -> thm
    1.27    val forall_elim_var: int -> thm -> thm
    1.28    val forall_elim_vars: int -> thm -> thm
    1.29    val implies_elim_list: thm -> thm list -> thm
    1.30 -  val implies_intr_list: Sign.cterm list -> thm -> thm
    1.31 +  val implies_intr_list: cterm list -> thm -> thm
    1.32    val MRL: thm list list * thm list -> thm list
    1.33    val MRS: thm list * thm -> thm
    1.34 -  val print_cterm: Sign.cterm -> unit
    1.35 -  val print_ctyp: Sign.ctyp -> unit
    1.36 +  val pprint_cterm: cterm -> pprint_args -> unit
    1.37 +  val pprint_ctyp: ctyp -> pprint_args -> unit
    1.38 +  val pprint_sg: Sign.sg -> pprint_args -> unit
    1.39 +  val pprint_theory: theory -> pprint_args -> unit
    1.40 +  val pprint_thm: thm -> pprint_args -> unit
    1.41 +  val pretty_thm: thm -> Sign.Syntax.Pretty.T
    1.42 +  val print_cterm: cterm -> unit
    1.43 +  val print_ctyp: ctyp -> unit
    1.44    val print_goals: int -> thm -> unit
    1.45    val print_goals_ref: (int -> thm -> unit) ref
    1.46    val print_sg: Sign.sg -> unit
    1.47    val print_theory: theory -> unit
    1.48 -  val pprint_sg: Sign.sg -> pprint_args -> unit
    1.49 -  val pprint_theory: theory -> pprint_args -> unit
    1.50 -  val pretty_thm: thm -> Sign.Syntax.Pretty.T
    1.51    val print_thm: thm -> unit
    1.52    val prth: thm -> thm
    1.53    val prthq: thm Sequence.seq -> thm Sequence.seq
    1.54    val prths: thm list -> thm list
    1.55 +  val read_ctyp: Sign.sg -> string -> ctyp
    1.56    val read_instantiate: (string*string)list -> thm -> thm
    1.57    val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    1.58 +  val read_insts: 
    1.59 +          Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
    1.60 +                  -> (indexname -> typ option) * (indexname -> sort option)
    1.61 +                  -> (string*string)list
    1.62 +                  -> (indexname*ctyp)list * (cterm*cterm)list
    1.63    val reflexive_thm: thm
    1.64    val revcut_rl: thm
    1.65    val rewrite_goal_rule: bool*bool -> (meta_simpset -> thm -> thm option)
    1.66 @@ -61,9 +71,10 @@
    1.67    val show_hyps: bool ref
    1.68    val size_of_thm: thm -> int
    1.69    val standard: thm -> thm
    1.70 +  val string_of_cterm: cterm -> string
    1.71 +  val string_of_ctyp: ctyp -> string
    1.72    val string_of_thm: thm -> string
    1.73    val symmetric_thm: thm
    1.74 -  val pprint_thm: thm -> pprint_args -> unit
    1.75    val transitive_thm: thm
    1.76    val triv_forall_equality: thm
    1.77    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    1.78 @@ -82,6 +93,145 @@
    1.79  
    1.80  (**** More derived rules and operations on theorems ****)
    1.81  
    1.82 +fun cterm_fun f ct =
    1.83 + let val {sign,t,...} = rep_cterm ct in cterm_of sign (f t) end;
    1.84 +
    1.85 +fun read_ctyp sign = ctyp_of sign o Sign.read_typ(sign, K None);
    1.86 +
    1.87 +
    1.88 +(** reading of instantiations **)
    1.89 +
    1.90 +fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
    1.91 +        | _ => error("Lexical error in variable name " ^ quote (implode cs));
    1.92 +
    1.93 +fun absent ixn =
    1.94 +  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
    1.95 +
    1.96 +fun inst_failure ixn =
    1.97 +  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
    1.98 +
    1.99 +fun read_insts sign (rtypes,rsorts) (types,sorts) insts =
   1.100 +let val {tsig,...} = Sign.rep_sg sign
   1.101 +    fun split([],tvs,vs) = (tvs,vs)
   1.102 +      | split((sv,st)::l,tvs,vs) = (case explode sv of
   1.103 +                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   1.104 +                | cs => split(l,tvs,(indexname cs,st)::vs));
   1.105 +    val (tvs,vs) = split(insts,[],[]);
   1.106 +    fun readT((a,i),st) =
   1.107 +        let val ixn = ("'" ^ a,i);
   1.108 +            val S = case rsorts ixn of Some S => S | None => absent ixn;
   1.109 +            val T = Sign.read_typ (sign,sorts) st;
   1.110 +        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   1.111 +           else inst_failure ixn
   1.112 +        end
   1.113 +    val tye = map readT tvs;
   1.114 +    fun add_cterm ((cts,tye), (ixn,st)) =
   1.115 +        let val T = case rtypes ixn of
   1.116 +                      Some T => typ_subst_TVars tye T
   1.117 +                    | None => absent ixn;
   1.118 +            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   1.119 +            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   1.120 +        in ((cv,ct)::cts,tye2 @ tye) end
   1.121 +    val (cterms,tye') = foldl add_cterm (([],tye), vs);
   1.122 +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   1.123 +
   1.124 +
   1.125 +(*** Printing of theorems ***)
   1.126 +
   1.127 +(*If false, hypotheses are printed as dots*)
   1.128 +val show_hyps = ref true;
   1.129 +
   1.130 +fun pretty_thm th =
   1.131 +let val {sign, hyps, prop,...} = rep_thm th
   1.132 +    val hsymbs = if null hyps then []
   1.133 +		 else if !show_hyps then
   1.134 +		      [Pretty.brk 2,
   1.135 +		       Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)]
   1.136 +		 else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @
   1.137 +		      [Pretty.str"]"];
   1.138 +in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end;
   1.139 +
   1.140 +val string_of_thm = Pretty.string_of o pretty_thm;
   1.141 +
   1.142 +val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
   1.143 +
   1.144 +
   1.145 +(** Top-level commands for printing theorems **)
   1.146 +val print_thm = writeln o string_of_thm;
   1.147 +
   1.148 +fun prth th = (print_thm th; th);
   1.149 +
   1.150 +(*Print and return a sequence of theorems, separated by blank lines. *)
   1.151 +fun prthq thseq =
   1.152 +    (Sequence.prints (fn _ => print_thm) 100000 thseq;
   1.153 +     thseq);
   1.154 +
   1.155 +(*Print and return a list of theorems, separated by blank lines. *)
   1.156 +fun prths ths = (print_list_ln print_thm ths; ths);
   1.157 +
   1.158 +(*Other printing commands*)
   1.159 +fun pprint_ctyp cT = 
   1.160 + let val {sign,T} = rep_ctyp cT in  Sign.pprint_typ sign T  end;
   1.161 +
   1.162 +fun string_of_ctyp cT = 
   1.163 + let val {sign,T} = rep_ctyp cT in  Sign.string_of_typ sign T  end;
   1.164 +
   1.165 +val print_ctyp = writeln o string_of_ctyp;
   1.166 +
   1.167 +fun pprint_cterm ct = 
   1.168 + let val {sign,t,...} = rep_cterm ct in  Sign.pprint_term sign t  end;
   1.169 +
   1.170 +fun string_of_cterm ct = 
   1.171 + let val {sign,t,...} = rep_cterm ct in  Sign.string_of_term sign t  end;
   1.172 +
   1.173 +val print_cterm = writeln o string_of_cterm;
   1.174 +
   1.175 +fun pretty_sg sg = 
   1.176 +  Pretty.lst ("{", "}") (map (Pretty.str o !) (#stamps (Sign.rep_sg sg)));
   1.177 +
   1.178 +val pprint_sg = Pretty.pprint o pretty_sg;
   1.179 +
   1.180 +val pprint_theory = pprint_sg o sign_of;
   1.181 +
   1.182 +val print_sg = writeln o Pretty.string_of o pretty_sg;
   1.183 +val print_theory = print_sg o sign_of;
   1.184 +
   1.185 +
   1.186 +(** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
   1.187 +
   1.188 +fun prettyprints es = writeln(Pretty.string_of(Pretty.blk(0,es)));
   1.189 +
   1.190 +fun print_goals maxgoals th : unit =
   1.191 +let val {sign, hyps, prop,...} = rep_thm th;
   1.192 +    fun printgoals (_, []) = ()
   1.193 +      | printgoals (n, A::As) =
   1.194 +	let val prettyn = Pretty.str(" " ^ string_of_int n ^ ". ");
   1.195 +	    val prettyA = Sign.pretty_term sign A
   1.196 +	in prettyprints[prettyn,prettyA]; 
   1.197 +           printgoals (n+1,As) 
   1.198 +        end;
   1.199 +    fun prettypair(t,u) =
   1.200 +        Pretty.blk(0, [Sign.pretty_term sign t, Pretty.str" =?=", Pretty.brk 1,
   1.201 +		       Sign.pretty_term sign u]);
   1.202 +    fun printff [] = ()
   1.203 +      | printff tpairs =
   1.204 +	 writeln("\nFlex-flex pairs:\n" ^
   1.205 +		 Pretty.string_of(Pretty.lst("","") (map prettypair tpairs)))
   1.206 +    val (tpairs,As,B) = Logic.strip_horn(prop);
   1.207 +    val ngoals = length As
   1.208 +in 
   1.209 +   writeln (Sign.string_of_term sign B);
   1.210 +   if ngoals=0 then writeln"No subgoals!"
   1.211 +   else if ngoals>maxgoals 
   1.212 +        then (printgoals (1, take(maxgoals,As));
   1.213 +	      writeln("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   1.214 +        else printgoals (1, As);
   1.215 +   printff tpairs
   1.216 +end;
   1.217 +
   1.218 +(*"hook" for user interfaces: allows print_goals to be replaced*)
   1.219 +val print_goals_ref = ref print_goals;
   1.220 +
   1.221  (*** Find the type (sort) associated with a (T)Var or (T)Free in a term 
   1.222       Used for establishing default types (of variables) and sorts (of
   1.223       type variables) when reading another term.
   1.224 @@ -111,7 +261,7 @@
   1.225  fun forall_intr_frees th =
   1.226      let val {prop,sign,...} = rep_thm th
   1.227      in  forall_intr_list
   1.228 -         (map (Sign.cterm_of sign) (sort atless (term_frees prop))) 
   1.229 +         (map (cterm_of sign) (sort atless (term_frees prop))) 
   1.230           th
   1.231      end;
   1.232  
   1.233 @@ -121,7 +271,7 @@
   1.234      let val {prop,sign,...} = rep_thm th
   1.235      in case prop of
   1.236  	  Const("all",_) $ Abs(a,T,_) =>
   1.237 -	      forall_elim (Sign.cterm_of sign (Var((a,i), T)))  th
   1.238 +	      forall_elim (cterm_of sign (Var((a,i), T)))  th
   1.239  	| _ => raise THM("forall_elim_var", i, [th])
   1.240      end;
   1.241  
   1.242 @@ -147,12 +297,12 @@
   1.243  	val inrs = add_term_tvars(prop,[]);
   1.244  	val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs));
   1.245  	val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms')
   1.246 -	val ctye = map (fn (v,T) => (v,Sign.ctyp_of sign T)) tye;
   1.247 +	val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye;
   1.248  	fun varpairs([],[]) = []
   1.249  	  | varpairs((var as Var(v,T)) :: vars, b::bs) =
   1.250  		let val T' = typ_subst_TVars tye T
   1.251 -		in (Sign.cterm_of sign (Var(v,T')),
   1.252 -		    Sign.cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
   1.253 +		in (cterm_of sign (Var(v,T')),
   1.254 +		    cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
   1.255  		end
   1.256  	  | varpairs _ = raise TERM("varpairs", []);
   1.257      in instantiate (ctye, varpairs(vars,rev bs)) th end;
   1.258 @@ -173,9 +323,9 @@
   1.259  	     [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
   1.260  fun assume_ax thy sP =
   1.261      let val sign = sign_of thy
   1.262 -	val prop = Logic.close_form (Sign.term_of (Sign.read_cterm sign
   1.263 +	val prop = Logic.close_form (term_of (read_cterm sign
   1.264  			 (sP, propT)))
   1.265 -    in forall_elim_vars 0 (assume (Sign.cterm_of sign prop))  end;
   1.266 +    in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
   1.267  
   1.268  (*Resolution: exactly one resolvent must be produced.*) 
   1.269  fun tha RSN (i,thb) =
   1.270 @@ -223,8 +373,7 @@
   1.271  (*Instantiate theorem th, reading instantiations under signature sg*)
   1.272  fun read_instantiate_sg sg sinsts th =
   1.273      let val ts = types_sorts th;
   1.274 -        val instpair = Sign.read_insts sg ts ts sinsts
   1.275 -    in  instantiate instpair th  end;
   1.276 +    in  instantiate (read_insts sg ts ts sinsts) th  end;
   1.277  
   1.278  (*Instantiate theorem th, reading instantiations under theory of th*)
   1.279  fun read_instantiate sinsts th =
   1.280 @@ -235,8 +384,8 @@
   1.281    Instantiates distinct Vars by terms, inferring type instantiations. *)
   1.282  local
   1.283    fun add_types ((ct,cu), (sign,tye)) =
   1.284 -    let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct
   1.285 -        and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu
   1.286 +    let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
   1.287 +        and {sign=signu, t=u, T= U, ...} = rep_cterm cu
   1.288          val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   1.289  	val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye)
   1.290  	  handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
   1.291 @@ -246,8 +395,8 @@
   1.292    let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[]))
   1.293        val tsig = #tsig(Sign.rep_sg sign);
   1.294        fun instT(ct,cu) = let val inst = subst_TVars tye
   1.295 -			 in (Sign.cfun inst ct, Sign.cfun inst cu) end
   1.296 -      fun ctyp2 (ix,T) = (ix, Sign.ctyp_of sign T)
   1.297 +			 in (cterm_fun inst ct, cterm_fun inst cu) end
   1.298 +      fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   1.299    in  instantiate (map ctyp2 tye, map instT ctpairs0) th  end
   1.300    handle TERM _ => 
   1.301             raise THM("cterm_instantiate: incompatible signatures",0,[th])
   1.302 @@ -255,88 +404,6 @@
   1.303  end;
   1.304  
   1.305  
   1.306 -(*** Printing of theorems ***)
   1.307 -
   1.308 -(*If false, hypotheses are printed as dots*)
   1.309 -val show_hyps = ref true;
   1.310 -
   1.311 -fun pretty_thm th =
   1.312 -let val {sign, hyps, prop,...} = rep_thm th
   1.313 -    val hsymbs = if null hyps then []
   1.314 -		 else if !show_hyps then
   1.315 -		      [Pretty.brk 2,
   1.316 -		       Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)]
   1.317 -		 else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @
   1.318 -		      [Pretty.str"]"];
   1.319 -in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end;
   1.320 -
   1.321 -val string_of_thm = Pretty.string_of o pretty_thm;
   1.322 -
   1.323 -val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
   1.324 -
   1.325 -
   1.326 -(** Top-level commands for printing theorems **)
   1.327 -val print_thm = writeln o string_of_thm;
   1.328 -
   1.329 -fun prth th = (print_thm th; th);
   1.330 -
   1.331 -(*Print and return a sequence of theorems, separated by blank lines. *)
   1.332 -fun prthq thseq =
   1.333 -    (Sequence.prints (fn _ => print_thm) 100000 thseq;
   1.334 -     thseq);
   1.335 -
   1.336 -(*Print and return a list of theorems, separated by blank lines. *)
   1.337 -fun prths ths = (print_list_ln print_thm ths; ths);
   1.338 -
   1.339 -(*Other printing commands*)
   1.340 -val print_cterm = writeln o Sign.string_of_cterm;
   1.341 -val print_ctyp = writeln o Sign.string_of_ctyp;
   1.342 -fun pretty_sg sg = 
   1.343 -  Pretty.lst ("{", "}") (map (Pretty.str o !) (#stamps (Sign.rep_sg sg)));
   1.344 -
   1.345 -val pprint_sg = Pretty.pprint o pretty_sg;
   1.346 -
   1.347 -val pprint_theory = pprint_sg o sign_of;
   1.348 -
   1.349 -val print_sg = writeln o Pretty.string_of o pretty_sg;
   1.350 -val print_theory = print_sg o sign_of;
   1.351 -
   1.352 -
   1.353 -(** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
   1.354 -
   1.355 -fun prettyprints es = writeln(Pretty.string_of(Pretty.blk(0,es)));
   1.356 -
   1.357 -fun print_goals maxgoals th : unit =
   1.358 -let val {sign, hyps, prop,...} = rep_thm th;
   1.359 -    fun printgoals (_, []) = ()
   1.360 -      | printgoals (n, A::As) =
   1.361 -	let val prettyn = Pretty.str(" " ^ string_of_int n ^ ". ");
   1.362 -	    val prettyA = Sign.pretty_term sign A
   1.363 -	in prettyprints[prettyn,prettyA]; 
   1.364 -           printgoals (n+1,As) 
   1.365 -        end;
   1.366 -    fun prettypair(t,u) =
   1.367 -        Pretty.blk(0, [Sign.pretty_term sign t, Pretty.str" =?=", Pretty.brk 1,
   1.368 -		       Sign.pretty_term sign u]);
   1.369 -    fun printff [] = ()
   1.370 -      | printff tpairs =
   1.371 -	 writeln("\nFlex-flex pairs:\n" ^
   1.372 -		 Pretty.string_of(Pretty.lst("","") (map prettypair tpairs)))
   1.373 -    val (tpairs,As,B) = Logic.strip_horn(prop);
   1.374 -    val ngoals = length As
   1.375 -in 
   1.376 -   writeln (Sign.string_of_term sign B);
   1.377 -   if ngoals=0 then writeln"No subgoals!"
   1.378 -   else if ngoals>maxgoals 
   1.379 -        then (printgoals (1, take(maxgoals,As));
   1.380 -	      writeln("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   1.381 -        else printgoals (1, As);
   1.382 -   printff tpairs
   1.383 -end;
   1.384 -
   1.385 -(*"hook" for user interfaces: allows print_goals to be replaced*)
   1.386 -val print_goals_ref = ref print_goals;
   1.387 -
   1.388  (** theorem equality test is exported and used by BEST_FIRST **)
   1.389  
   1.390  (*equality of signatures means exact identity -- by ref equality*)
   1.391 @@ -363,42 +430,40 @@
   1.392  
   1.393  
   1.394  val reflexive_thm =
   1.395 -  let val cx = Sign.cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),["logic"])))
   1.396 +  let val cx = cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),["logic"])))
   1.397    in Thm.reflexive cx end;
   1.398  
   1.399  val symmetric_thm =
   1.400 -  let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT)
   1.401 +  let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
   1.402    in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
   1.403  
   1.404  val transitive_thm =
   1.405 -  let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT)
   1.406 -      val yz = Sign.read_cterm Sign.pure ("y::'a::logic == z",propT)
   1.407 +  let val xy = read_cterm Sign.pure ("x::'a::logic == y",propT)
   1.408 +      val yz = read_cterm Sign.pure ("y::'a::logic == z",propT)
   1.409        val xythm = Thm.assume xy and yzthm = Thm.assume yz
   1.410    in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   1.411  
   1.412 -(** Below, a "conversion" has type sign->term->thm **)
   1.413 +(** Below, a "conversion" has type cterm -> thm **)
   1.414 +
   1.415 +val refl_cimplies = reflexive (cterm_of Sign.pure implies);
   1.416  
   1.417  (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   1.418  (*Do not rewrite flex-flex pairs*)
   1.419 -fun goals_conv pred cv sign = 
   1.420 -  let val triv = reflexive o Sign.fake_cterm_of sign
   1.421 -      fun gconv i t =
   1.422 -        let val (A,B) = Logic.dest_implies t
   1.423 -            val (thA,j) = case A of
   1.424 -                  Const("=?=",_)$_$_ => (triv A,i)
   1.425 -                | _ => (if pred i then cv sign A else triv A, i+1)
   1.426 -	in  combination (combination (triv implies) thA) (gconv j B) end
   1.427 -        handle TERM _ => triv t
   1.428 +fun goals_conv pred cv = 
   1.429 +  let fun gconv i ct =
   1.430 +        let val (A,B) = Thm.dest_cimplies ct
   1.431 +            val (thA,j) = case term_of A of
   1.432 +                  Const("=?=",_)$_$_ => (reflexive A, i)
   1.433 +                | _ => (if pred i then cv A else reflexive A, i+1)
   1.434 +	in  combination (combination refl_cimplies thA) (gconv j B) end
   1.435 +        handle TERM _ => reflexive ct
   1.436    in gconv 1 end;
   1.437  
   1.438  (*Use a conversion to transform a theorem*)
   1.439 -fun fconv_rule cv th =
   1.440 -  let val {sign,prop,...} = rep_thm th
   1.441 -  in  equal_elim (cv sign prop) th  end;
   1.442 +fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   1.443  
   1.444  (*rewriting conversion*)
   1.445 -fun rew_conv mode prover mss sign t =
   1.446 -  rewrite_cterm mode mss prover (Sign.fake_cterm_of sign t);
   1.447 +fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
   1.448  
   1.449  (*Rewrite a theorem*)
   1.450  fun rewrite_rule thms =
   1.451 @@ -420,11 +485,11 @@
   1.452  
   1.453  (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   1.454  fun equal_abs_elim ca eqth =
   1.455 -  let val {sign=signa, t=a, ...} = Sign.rep_cterm ca
   1.456 +  let val {sign=signa, t=a, ...} = rep_cterm ca
   1.457        and combth = combination eqth (reflexive ca)
   1.458        val {sign,prop,...} = rep_thm eqth
   1.459        val (abst,absu) = Logic.dest_equals prop
   1.460 -      val cterm = Sign.cterm_of (Sign.merge (sign,signa))
   1.461 +      val cterm = cterm_of (Sign.merge (sign,signa))
   1.462    in  transitive (symmetric (beta_conversion (cterm (abst$a))))
   1.463             (transitive combth (beta_conversion (cterm (absu$a))))
   1.464    end
   1.465 @@ -439,7 +504,7 @@
   1.466    fun err th = raise THM("flexpair_inst: ", 0, [th])
   1.467    fun flexpair_inst def th =
   1.468      let val {prop = Const _ $ t $ u,  sign,...} = rep_thm th
   1.469 -	val cterm = Sign.cterm_of sign
   1.470 +	val cterm = cterm_of sign
   1.471  	fun cvar a = cterm(Var((a,0),alpha))
   1.472  	val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] 
   1.473  		   def
   1.474 @@ -459,17 +524,17 @@
   1.475  (*** Some useful meta-theorems ***)
   1.476  
   1.477  (*The rule V/V, obtains assumption solving for eresolve_tac*)
   1.478 -val asm_rl = trivial(Sign.read_cterm Sign.pure ("PROP ?psi",propT));
   1.479 +val asm_rl = trivial(read_cterm Sign.pure ("PROP ?psi",propT));
   1.480  
   1.481  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   1.482 -val cut_rl = trivial(Sign.read_cterm Sign.pure 
   1.483 +val cut_rl = trivial(read_cterm Sign.pure 
   1.484  	("PROP ?psi ==> PROP ?theta", propT));
   1.485  
   1.486  (*Generalized elim rule for one conclusion; cut_rl with reversed premises: 
   1.487       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   1.488  val revcut_rl =
   1.489 -  let val V = Sign.read_cterm Sign.pure ("PROP V", propT)
   1.490 -      and VW = Sign.read_cterm Sign.pure ("PROP V ==> PROP W", propT);
   1.491 +  let val V = read_cterm Sign.pure ("PROP V", propT)
   1.492 +      and VW = read_cterm Sign.pure ("PROP V ==> PROP W", propT);
   1.493    in  standard (implies_intr V 
   1.494  		(implies_intr VW
   1.495  		 (implies_elim (assume VW) (assume V))))
   1.496 @@ -477,9 +542,9 @@
   1.497  
   1.498  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   1.499  val triv_forall_equality =
   1.500 -  let val V  = Sign.read_cterm Sign.pure ("PROP V", propT)
   1.501 -      and QV = Sign.read_cterm Sign.pure ("!!x::'a. PROP V", propT)
   1.502 -      and x  = Sign.read_cterm Sign.pure ("x", TFree("'a",["logic"]));
   1.503 +  let val V  = read_cterm Sign.pure ("PROP V", propT)
   1.504 +      and QV = read_cterm Sign.pure ("!!x::'a. PROP V", propT)
   1.505 +      and x  = read_cterm Sign.pure ("x", TFree("'a",["logic"]));
   1.506    in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   1.507  		           (implies_intr V  (forall_intr x (assume V))))
   1.508    end;
     2.1 --- a/src/Pure/sign.ML	Tue Jan 18 07:53:35 1994 +0100
     2.2 +++ b/src/Pure/sign.ML	Tue Jan 18 13:46:08 1994 +0100
     2.3 @@ -1,10 +1,9 @@
     2.4  (*  Title:      Pure/sign.ML
     2.5      ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1992  University of Cambridge
     2.8 +    Copyright   1994  University of Cambridge
     2.9  
    2.10 -The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
    2.11 -typs under a signature).
    2.12 +The abstract types "sg" of signatures
    2.13  *)
    2.14  
    2.15  signature SIGN =
    2.16 @@ -14,11 +13,6 @@
    2.17    structure Syntax: SYNTAX
    2.18    sharing Symtab = Type.Symtab
    2.19    type sg
    2.20 -  type cterm
    2.21 -  type ctyp
    2.22 -  val cfun: (term -> term) -> (cterm -> cterm)
    2.23 -  val cterm_of: sg -> term -> cterm
    2.24 -  val ctyp_of: sg -> typ -> ctyp
    2.25    val extend: sg -> string ->
    2.26          (class * class list) list * class list *
    2.27          (string list * int) list *
    2.28 @@ -27,32 +21,18 @@
    2.29          (string list * string)list * Syntax.sext option -> sg
    2.30    val merge: sg * sg -> sg
    2.31    val pure: sg
    2.32 -  val read_cterm: sg -> string * typ -> cterm
    2.33 -  val read_ctyp: sg -> string -> ctyp
    2.34 -  val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
    2.35 -                  -> (indexname -> typ option) * (indexname -> sort option)
    2.36 -                  -> (string*string)list
    2.37 -                  -> (indexname*ctyp)list * (cterm*cterm)list
    2.38    val read_typ: sg * (indexname -> sort option) -> string -> typ
    2.39 -  val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
    2.40 -  val rep_ctyp: ctyp -> {T: typ, sign: sg}
    2.41    val rep_sg: sg -> {tsig: Type.type_sig,
    2.42                       const_tab: typ Symtab.table,
    2.43                       syn: Syntax.syntax,
    2.44                       stamps: string ref list}
    2.45 -  val string_of_cterm: cterm -> string
    2.46 -  val string_of_ctyp: ctyp -> string
    2.47 -  val pprint_cterm: cterm -> pprint_args -> unit
    2.48 -  val pprint_ctyp: ctyp -> pprint_args -> unit
    2.49    val string_of_term: sg -> term -> string
    2.50    val string_of_typ: sg -> typ -> string
    2.51    val subsig: sg * sg -> bool
    2.52    val pprint_term: sg -> term -> pprint_args -> unit
    2.53    val pprint_typ: sg -> typ -> pprint_args -> unit
    2.54 -  val term_of: cterm -> term
    2.55 -  val typ_of: ctyp -> typ
    2.56    val pretty_term: sg -> term -> Syntax.Pretty.T
    2.57 -val fake_cterm_of: sg -> term -> cterm
    2.58 +  val term_errors: sg -> term -> string list
    2.59  end;
    2.60  
    2.61  functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    2.62 @@ -90,20 +70,20 @@
    2.63  (*Check a term for errors.  Are all constants and types valid in signature?
    2.64    Does not check that term is well-typed!*)
    2.65  fun term_errors (sign as Sg{tsig,const_tab,...}) =
    2.66 -let val showtyp = string_of_typ sign
    2.67 -    fun terrs (Const (a,T), errs) =
    2.68 -        if valid_const tsig const_tab (a,T)
    2.69 -        then Type.type_errors tsig (T,errs)
    2.70 -        else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    2.71 -      | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    2.72 -      | terrs (Var  ((a,i),T), errs) =
    2.73 -        if  i>=0  then  Type.type_errors tsig (T,errs)
    2.74 -        else  ("Negative index for Var: " ^ a) :: errs
    2.75 -      | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
    2.76 -      | terrs (Abs (_,T,t), errs) =
    2.77 -            Type.type_errors tsig (T,terrs(t,errs))
    2.78 -      | terrs (f$t, errs) = terrs(f, terrs (t,errs))
    2.79 -in  terrs  end;
    2.80 +  let val showtyp = string_of_typ sign
    2.81 +      fun terrs (Const (a,T), errs) =
    2.82 +	  if valid_const tsig const_tab (a,T)
    2.83 +	  then Type.type_errors tsig (T,errs)
    2.84 +	  else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    2.85 +	| terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    2.86 +	| terrs (Var  ((a,i),T), errs) =
    2.87 +	  if  i>=0  then  Type.type_errors tsig (T,errs)
    2.88 +	  else  ("Negative index for Var: " ^ a) :: errs
    2.89 +	| terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
    2.90 +	| terrs (Abs (_,T,t), errs) =
    2.91 +	      Type.type_errors tsig (T,terrs(t,errs))
    2.92 +	| terrs (f$t, errs) = terrs(f, terrs (t,errs))
    2.93 +  in  fn t => terrs(t,[])  end;
    2.94  
    2.95  
    2.96  
    2.97 @@ -238,44 +218,12 @@
    2.98  
    2.99  
   2.100  
   2.101 -(**** CERTIFIED TYPES ****)
   2.102 -
   2.103 -
   2.104 -(*Certified typs under a signature*)
   2.105 -datatype ctyp = Ctyp of {sign: sg,  T: typ};
   2.106 -
   2.107 -fun rep_ctyp(Ctyp ctyp) = ctyp;
   2.108 -
   2.109 -fun typ_of (Ctyp{sign,T}) = T;
   2.110 -
   2.111 -fun ctyp_of (sign as Sg{tsig,...}) T =
   2.112 -        case Type.type_errors tsig (T,[]) of
   2.113 -          [] => Ctyp{sign= sign,T= T}
   2.114 -        | errs =>  error (cat_lines ("Error in type:" :: errs));
   2.115 -
   2.116  fun read_typ(Sg{tsig,syn,...}, defS) s =
   2.117      let val term = Syntax.read syn Syntax.typeT s;
   2.118          val S0 = Type.defaultS tsig;
   2.119          fun defS0 s = case defS s of Some S => S | None => S0;
   2.120      in Syntax.typ_of_term defS0 term end;
   2.121  
   2.122 -fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
   2.123 -
   2.124 -fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;
   2.125 -
   2.126 -fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;
   2.127 -
   2.128 -
   2.129 -(**** CERTIFIED TERMS ****)
   2.130 -
   2.131 -(*Certified terms under a signature, with checked typ and maxidx of Vars*)
   2.132 -datatype cterm = Cterm of {sign: sg,  t: term,  T: typ,  maxidx: int};
   2.133 -
   2.134 -fun rep_cterm (Cterm args) = args;
   2.135 -
   2.136 -(*Return the underlying term*)
   2.137 -fun term_of (Cterm{sign,t,T,maxidx}) = t;
   2.138 -
   2.139  (** pretty printing of terms **)
   2.140  
   2.141  fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
   2.142 @@ -284,78 +232,5 @@
   2.143  
   2.144  fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
   2.145  
   2.146 -fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;
   2.147 -
   2.148 -fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;
   2.149 -
   2.150 -(*Create a cterm by checking a "raw" term with respect to a signature*)
   2.151 -fun cterm_of sign t =
   2.152 -  case  term_errors sign (t,[])  of
   2.153 -      [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
   2.154 -    | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
   2.155 -
   2.156 -(*The only use is a horrible hack in the simplifier!*)
   2.157 -fun fake_cterm_of sign t =
   2.158 -  Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
   2.159 -
   2.160 -fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
   2.161 -
   2.162 -(*Lexing, parsing, polymorphic typechecking of a term.*)
   2.163 -fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
   2.164 -                   (a,T) =
   2.165 -  let val showtyp = string_of_typ sign
   2.166 -      and showterm = string_of_term sign
   2.167 -      fun termerr [] = ""
   2.168 -        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
   2.169 -        | termerr ts = "\nInvolving these terms:\n" ^
   2.170 -                       cat_lines (map showterm ts)
   2.171 -      val t = Syntax.read syn T a;
   2.172 -      val (t',tye) = Type.infer_types (tsig, const_tab, types,
   2.173 -                                       sorts, showtyp, T, t)
   2.174 -                  handle TYPE (msg, Ts, ts) =>
   2.175 -          error ("Type checking error: " ^ msg ^ "\n" ^
   2.176 -                  cat_lines (map showtyp Ts) ^ termerr ts)
   2.177 -  in (cterm_of sign t', tye)
   2.178 -  end
   2.179 -  handle TERM (msg, _) => error ("Error: " ^  msg);
   2.180 -
   2.181 -
   2.182 -fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
   2.183 -
   2.184 -(** reading of instantiations **)
   2.185 -
   2.186 -fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   2.187 -        | _ => error("Lexical error in variable name " ^ quote (implode cs));
   2.188 -
   2.189 -fun absent ixn =
   2.190 -  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
   2.191 -
   2.192 -fun inst_failure ixn =
   2.193 -  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   2.194 -
   2.195 -fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
   2.196 -let fun split([],tvs,vs) = (tvs,vs)
   2.197 -      | split((sv,st)::l,tvs,vs) = (case explode sv of
   2.198 -                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   2.199 -                | cs => split(l,tvs,(indexname cs,st)::vs));
   2.200 -    val (tvs,vs) = split(insts,[],[]);
   2.201 -    fun readT((a,i),st) =
   2.202 -        let val ixn = ("'" ^ a,i);
   2.203 -            val S = case rsorts ixn of Some S => S | None => absent ixn;
   2.204 -            val T = read_typ (sign,sorts) st;
   2.205 -        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   2.206 -           else inst_failure ixn
   2.207 -        end
   2.208 -    val tye = map readT tvs;
   2.209 -    fun add_cterm ((cts,tye), (ixn,st)) =
   2.210 -        let val T = case rtypes ixn of
   2.211 -                      Some T => typ_subst_TVars tye T
   2.212 -                    | None => absent ixn;
   2.213 -            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   2.214 -            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   2.215 -        in ((cv,ct)::cts,tye2 @ tye) end
   2.216 -    val (cterms,tye') = foldl add_cterm (([],tye), vs);
   2.217 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   2.218 -
   2.219  end;
   2.220  
     3.1 --- a/src/Pure/thm.ML	Tue Jan 18 07:53:35 1994 +0100
     3.2 +++ b/src/Pure/thm.ML	Tue Jan 18 13:46:08 1994 +0100
     3.3 @@ -1,9 +1,12 @@
     3.4  (*  Title: 	thm
     3.5      ID:         $Id$
     3.6      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1991  University of Cambridge
     3.8 +    Copyright   1994  University of Cambridge
     3.9 +
    3.10 +NO REP_CTERM!!
    3.11  
    3.12  The abstract types "theory" and "thm"
    3.13 +Also "cterm" / "ctyp" (certified terms / typs under a signature).
    3.14  *)
    3.15  
    3.16  signature THM = 
    3.17 @@ -11,25 +14,38 @@
    3.18    structure Envir : ENVIR
    3.19    structure Sequence : SEQUENCE
    3.20    structure Sign : SIGN
    3.21 +  type cterm
    3.22 +  type ctyp
    3.23    type meta_simpset
    3.24    type theory
    3.25    type thm
    3.26    exception THM of string * int * thm list
    3.27    exception THEORY of string * theory list
    3.28    exception SIMPLIFIER of string * thm
    3.29 -  val abstract_rule: string -> Sign.cterm -> thm -> thm
    3.30 +  (*Certified terms/types; previously in sign.ML*)
    3.31 +  val cterm_of: Sign.sg -> term -> cterm
    3.32 +  val ctyp_of: Sign.sg -> typ -> ctyp
    3.33 +  val read_cterm: Sign.sg -> string * typ -> cterm
    3.34 +  val rep_cterm: cterm -> {T: typ, t: term, sign: Sign.sg, maxidx: int}
    3.35 +  val rep_ctyp: ctyp -> {T: typ, sign: Sign.sg}
    3.36 +  val term_of: cterm -> term
    3.37 +  val typ_of: ctyp -> typ
    3.38 +  (*End of cterm/ctyp functions*)  
    3.39 +  val abstract_rule: string -> cterm -> thm -> thm
    3.40    val add_congs: meta_simpset * thm list -> meta_simpset
    3.41    val add_prems: meta_simpset * thm list -> meta_simpset
    3.42    val add_simps: meta_simpset * thm list -> meta_simpset
    3.43 -  val assume: Sign.cterm -> thm
    3.44 +  val assume: cterm -> thm
    3.45    val assumption: int -> thm -> thm Sequence.seq   
    3.46    val axioms_of: theory -> (string * thm) list
    3.47 -  val beta_conversion: Sign.cterm -> thm   
    3.48 +  val beta_conversion: cterm -> thm   
    3.49    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Sequence.seq   
    3.50    val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq   
    3.51    val combination: thm -> thm -> thm   
    3.52    val concl_of: thm -> term   
    3.53 +  val cprop_of: thm -> cterm
    3.54    val del_simps: meta_simpset * thm list -> meta_simpset
    3.55 +  val dest_cimplies: cterm -> cterm*cterm
    3.56    val dest_state: thm * int -> (term*term)list * term list * term * term
    3.57    val empty_mss: meta_simpset
    3.58    val eq_assumption: int -> thm -> thm   
    3.59 @@ -45,14 +61,14 @@
    3.60    val extensional: thm -> thm   
    3.61    val flexflex_rule: thm -> thm Sequence.seq  
    3.62    val flexpair_def: thm 
    3.63 -  val forall_elim: Sign.cterm -> thm -> thm
    3.64 -  val forall_intr: Sign.cterm -> thm -> thm
    3.65 +  val forall_elim: cterm -> thm -> thm
    3.66 +  val forall_intr: cterm -> thm -> thm
    3.67    val freezeT: thm -> thm
    3.68    val get_axiom: theory -> string -> thm
    3.69    val implies_elim: thm -> thm -> thm
    3.70 -  val implies_intr: Sign.cterm -> thm -> thm
    3.71 +  val implies_intr: cterm -> thm -> thm
    3.72    val implies_intr_hyps: thm -> thm
    3.73 -  val instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list 
    3.74 +  val instantiate: (indexname*ctyp)list * (cterm*cterm)list 
    3.75                     -> thm -> thm
    3.76    val lift_rule: (thm * int) -> thm -> thm
    3.77    val merge_theories: theory * theory -> theory
    3.78 @@ -63,12 +79,15 @@
    3.79    val prems_of: thm -> term list
    3.80    val prems_of_mss: meta_simpset -> thm list
    3.81    val pure_thy: theory
    3.82 -  val reflexive: Sign.cterm -> thm 
    3.83 +  val read_def_cterm :
    3.84 +         Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    3.85 +         string * typ -> cterm * (indexname * typ) list
    3.86 +   val reflexive: cterm -> thm 
    3.87    val rename_params_rule: string list * int -> thm -> thm
    3.88    val rep_thm: thm -> {prop: term, hyps: term list, maxidx: int, sign: Sign.sg}
    3.89    val rewrite_cterm:
    3.90           bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option)
    3.91 -           -> Sign.cterm -> thm
    3.92 +           -> cterm -> thm
    3.93    val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
    3.94    val sign_of: theory -> Sign.sg   
    3.95    val syn_of: theory -> Sign.Syntax.syntax
    3.96 @@ -78,7 +97,7 @@
    3.97    val tpairs_of: thm -> (term*term)list
    3.98    val trace_simp: bool ref
    3.99    val transitive: thm -> thm -> thm
   3.100 -  val trivial: Sign.cterm -> thm
   3.101 +  val trivial: cterm -> thm
   3.102    val varifyT: thm -> thm
   3.103    end;
   3.104  
   3.105 @@ -87,7 +106,7 @@
   3.106  functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN
   3.107                        and Net:NET
   3.108                  sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)
   3.109 -        (*: THM*) = (* FIXME *)
   3.110 +        : THM =
   3.111  struct
   3.112  structure Sequence = Unify.Sequence;
   3.113  structure Envir = Unify.Envir;
   3.114 @@ -97,7 +116,67 @@
   3.115  structure Symtab = Sign.Symtab;
   3.116  
   3.117  
   3.118 -(*Meta-theorems*)
   3.119 +(** Certified Types **)
   3.120 +
   3.121 +
   3.122 +(*Certified typs under a signature*)
   3.123 +datatype ctyp = Ctyp of {sign: Sign.sg,  T: typ};
   3.124 +
   3.125 +fun rep_ctyp(Ctyp ctyp) = ctyp;
   3.126 +fun typ_of (Ctyp{sign,T}) = T;
   3.127 +
   3.128 +fun ctyp_of sign T =
   3.129 +    case Type.type_errors (#tsig(Sign.rep_sg sign)) (T,[]) of
   3.130 +      []   => Ctyp{sign= sign,T= T}
   3.131 +    | errs =>  error (cat_lines ("Error in type:" :: errs));
   3.132 +
   3.133 +(** Certified Terms **)
   3.134 +
   3.135 +(*Certified terms under a signature, with checked typ and maxidx of Vars*)
   3.136 +datatype cterm = Cterm of {sign: Sign.sg,  t: term,  T: typ,  maxidx: int};
   3.137 +
   3.138 +fun rep_cterm (Cterm args) = args;
   3.139 +
   3.140 +(*Return the underlying term*)
   3.141 +fun term_of (Cterm{t,...}) = t;
   3.142 +
   3.143 +(*Create a cterm by checking a "raw" term with respect to a signature*)
   3.144 +fun cterm_of sign t =
   3.145 +  case  Sign.term_errors sign t  of
   3.146 +      [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
   3.147 +    | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
   3.148 +
   3.149 +(*dest_implies for cterms.  Note T=prop below*)
   3.150 +fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>",_) $ A $ B}) = 
   3.151 +       (Cterm{sign=sign, T=T, maxidx=maxidx, t=A},
   3.152 +	Cterm{sign=sign, T=T, maxidx=maxidx, t=B})
   3.153 +  | dest_cimplies ct = raise TERM("dest_cimplies", [term_of ct]);
   3.154 +
   3.155 +(** Reading of cterms -- needed twice below! **)
   3.156 +
   3.157 +(*Lexing, parsing, polymorphic typechecking of a term.*)
   3.158 +fun read_def_cterm (sign, types, sorts) (a,T) =
   3.159 +  let val {tsig, const_tab, syn,...} = Sign.rep_sg sign
   3.160 +      val showtyp = Sign.string_of_typ sign
   3.161 +      and showterm = Sign.string_of_term sign
   3.162 +      fun termerr [] = ""
   3.163 +        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
   3.164 +        | termerr ts = "\nInvolving these terms:\n" ^
   3.165 +                       cat_lines (map showterm ts)
   3.166 +      val t = Syntax.read syn T a;
   3.167 +      val (t',tye) = Type.infer_types (tsig, const_tab, types,
   3.168 +                                       sorts, showtyp, T, t)
   3.169 +                  handle TYPE (msg, Ts, ts) =>
   3.170 +          error ("Type checking error: " ^ msg ^ "\n" ^
   3.171 +                  cat_lines (map showtyp Ts) ^ termerr ts)
   3.172 +  in (cterm_of sign t', tye)
   3.173 +  end
   3.174 +  handle TERM (msg, _) => error ("Error: " ^  msg);
   3.175 +
   3.176 +fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
   3.177 +
   3.178 +(**** META-THEOREMS ****)
   3.179 +
   3.180  datatype thm = Thm of
   3.181      {sign: Sign.sg,  maxidx: int,  hyps: term list,  prop: term};
   3.182  
   3.183 @@ -120,6 +199,10 @@
   3.184  (*maps object-rule to conclusion *)
   3.185  fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop;
   3.186  
   3.187 +(*The statement of any Thm is a Cterm*)
   3.188 +fun cprop_of (Thm{sign,maxidx,hyps,prop}) = 
   3.189 +	Cterm{sign=sign, maxidx=maxidx, T=propT, t=prop};
   3.190 +
   3.191  (*Stamps associated with a signature*)
   3.192  val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
   3.193  
   3.194 @@ -168,7 +251,7 @@
   3.195  
   3.196  (*The assumption rule A|-A in a theory  *)
   3.197  fun assume ct : thm = 
   3.198 -  let val {sign, t=prop, T, maxidx} = Sign.rep_cterm ct
   3.199 +  let val {sign, t=prop, T, maxidx} = rep_cterm ct
   3.200    in  if T<>propT then  
   3.201  	raise THM("assume: assumptions must have type prop", 0, [])
   3.202        else if maxidx <> ~1 then
   3.203 @@ -182,7 +265,7 @@
   3.204  	      -------
   3.205  	      A ==> B    *)
   3.206  fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =
   3.207 -  let val {sign=signA, t=A, T, maxidx=maxidxA} = Sign.rep_cterm cA
   3.208 +  let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA
   3.209    in  if T<>propT then
   3.210  	raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   3.211        else Thm{sign= Sign.merge (sign,signA),  maxidx= max[maxidxA, maxidx], 
   3.212 @@ -215,7 +298,7 @@
   3.213     ------
   3.214     !!x.A       *)
   3.215  fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =
   3.216 -  let val x = Sign.term_of cx;
   3.217 +  let val x = term_of cx;
   3.218        fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   3.219  	                    prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
   3.220    in  case x of
   3.221 @@ -232,7 +315,7 @@
   3.222  	     --------
   3.223  	      A[t/x]     *)
   3.224  fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =
   3.225 -  let val {sign=signt, t, T, maxidx=maxt} = Sign.rep_cterm ct
   3.226 +  let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
   3.227    in  case prop of
   3.228  	  Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   3.229  	    if T<>qary then
   3.230 @@ -251,13 +334,13 @@
   3.231  (*Definition of the relation =?= *)
   3.232  val flexpair_def =
   3.233    Thm{sign= Sign.pure, hyps= [], maxidx= 0, 
   3.234 -      prop= Sign.term_of 
   3.235 -	      (Sign.read_cterm Sign.pure 
   3.236 +      prop= term_of 
   3.237 +	      (read_cterm Sign.pure 
   3.238  	         ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
   3.239  
   3.240  (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   3.241  fun reflexive ct = 
   3.242 -  let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   3.243 +  let val {sign, t, T, maxidx} = rep_cterm ct
   3.244    in  Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}
   3.245    end;
   3.246  
   3.247 @@ -289,7 +372,7 @@
   3.248  
   3.249  (*Beta-conversion: maps (%(x)t)(u) to the theorem  (%(x)t)(u) == t[u/x]   *)
   3.250  fun beta_conversion ct = 
   3.251 -  let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   3.252 +  let val {sign, t, T, maxidx} = rep_cterm ct
   3.253    in  case t of
   3.254  	  Abs(_,_,bodt) $ u => 
   3.255  	    Thm{sign= sign,  hyps= [],  
   3.256 @@ -326,7 +409,7 @@
   3.257      ----------------
   3.258        %(x)t == %(x)u     *)
   3.259  fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =
   3.260 -  let val x = Sign.term_of cx;
   3.261 +  let val x = term_of cx;
   3.262        val (t,u) = Logic.dest_equals prop  
   3.263  	    handle TERM _ =>
   3.264  		raise THM("abstract_rule: premise not an equality", 0, [th])
   3.265 @@ -431,14 +514,14 @@
   3.266  
   3.267  (*For instantiate: process pair of cterms, merge theories*)
   3.268  fun add_ctpair ((ct,cu), (sign,tpairs)) =
   3.269 -  let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct
   3.270 -      and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu
   3.271 +  let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
   3.272 +      and {sign=signu, t=u, T= U, ...} = rep_cterm cu
   3.273    in  if T=U  then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
   3.274        else raise TYPE("add_ctpair", [T,U], [t,u])
   3.275    end;
   3.276  
   3.277  fun add_ctyp ((v,ctyp), (sign',vTs)) =
   3.278 -  let val {T,sign} = Sign.rep_ctyp ctyp
   3.279 +  let val {T,sign} = rep_ctyp ctyp
   3.280    in (Sign.merge(sign,sign'), (v,T)::vTs) end;
   3.281  
   3.282  (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   3.283 @@ -475,7 +558,7 @@
   3.284  (*The trivial implication A==>A, justified by assume and forall rules.
   3.285    A can contain Vars, not so for assume!   *)
   3.286  fun trivial ct : thm = 
   3.287 -  let val {sign, t=A, T, maxidx} = Sign.rep_cterm ct
   3.288 +  let val {sign, t=A, T, maxidx} = rep_cterm ct
   3.289    in  if T<>propT then  
   3.290  	    raise THM("trivial: the term must have type prop", 0, [])
   3.291        else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
   3.292 @@ -756,7 +839,7 @@
   3.293  
   3.294  (*Converts Frees to Vars: axioms can be written without question marks*)
   3.295  fun prepare_axiom sign sP =
   3.296 -    Logic.varify (Sign.term_of (Sign.read_cterm sign (sP,propT)));
   3.297 +    Logic.varify (term_of (read_cterm sign (sP,propT)));
   3.298  
   3.299  (*Read an axiom for a new theory*)
   3.300  fun read_ax sign (a, sP) : string*thm =
   3.301 @@ -803,11 +886,11 @@
   3.302  
   3.303  exception SIMPLIFIER of string * thm;
   3.304  
   3.305 -fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t));
   3.306 +fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
   3.307  
   3.308  val trace_simp = ref false;
   3.309  
   3.310 -fun trace_term a sg t = if !trace_simp then prtm a sg t else ();
   3.311 +fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
   3.312  
   3.313  fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
   3.314  
   3.315 @@ -1010,7 +1093,7 @@
   3.316  
   3.317  (*** FIXME: check that #primes(mss) does not "occur" in ct alread ***)
   3.318  fun rewrite_cterm mode mss prover ct =
   3.319 -  let val {sign, t, T, maxidx} = Sign.rep_cterm ct;
   3.320 +  let val {sign, t, T, maxidx} = rep_cterm ct;
   3.321        val (hyps,u) = bottomc (mode,prover,sign) mss ([],t);
   3.322        val prop = Logic.mk_equals(t,u)
   3.323    in  Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop}