--- a/src/Pure/thm.ML Tue Feb 13 11:36:15 1996 +0100
+++ b/src/Pure/thm.ML Tue Feb 13 12:57:24 1996 +0100
@@ -23,13 +23,18 @@
(*certified terms*)
type cterm
- val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
+ exception CTERM of string
+ val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ,
+ maxidx: int}
val term_of : cterm -> term
val cterm_of : Sign.sg -> term -> cterm
val read_cterm : Sign.sg -> string * typ -> cterm
val read_cterms : Sign.sg -> string list * typ list -> cterm list
val cterm_fun : (term -> term) -> (cterm -> cterm)
val dest_cimplies : cterm -> cterm * cterm
+ val dest_comb : cterm -> cterm * cterm
+ val dest_abs : cterm -> cterm * cterm
+ val mk_prop : cterm -> cterm
val read_def_cterm :
Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
string list -> bool -> string * typ -> cterm * (indexname * typ) list
@@ -205,6 +210,39 @@
Cterm{sign=sign, T=T, maxidx=maxidx, t=B})
| dest_cimplies ct = raise TERM ("dest_cimplies", [term_of ct]);
+exception CTERM of string;
+
+(*Destruct application in cterms*)
+fun dest_comb (Cterm{sign, T, maxidx, t = A $ B}) =
+ let val typeA = fastype_of A;
+ val typeB =
+ case typeA of Type("fun",[S,T]) => S
+ | _ => error "Function type expected in dest_comb";
+ in
+ (Cterm {sign=sign, maxidx=maxidx, t=A, T=typeA},
+ Cterm {sign=sign, maxidx=maxidx, t=B, T=typeB})
+ end
+ | dest_comb _ = raise CTERM "dest_comb";
+
+(*Destruct abstraction in cterms*)
+fun dest_abs (Cterm{sign, T, maxidx, t = tm as Abs(s,ty,M)}) =
+ let fun mk_var{Name,Ty} = Free(Name,Ty);
+ val v = mk_var{Name = s, Ty = ty};
+ val ty2 =
+ case T of Type("fun",[_,S]) => S
+ | _ => error "Function type expected in dest_abs";
+ in (Cterm{sign = sign, T = ty, maxidx = maxidx, t = v},
+ Cterm{sign = sign, T = ty2, maxidx = maxidx, t = betapply (tm,v)})
+ end
+ | dest_abs _ = raise CTERM "dest_abs";
+
+(*Convert cterm of type "o" to "prop" by using Trueprop*)
+fun mk_prop (ct as Cterm{sign, T, maxidx, t = Const("Trueprop",_) $ _}) = ct
+ | mk_prop (Cterm{sign, T, maxidx, t}) =
+ if T = Type("o",[]) then
+ Cterm{sign = sign, T = Type("prop",[]), maxidx = maxidx,
+ t = Const("Trueprop", Type("o",[]) --> Type("prop",[])) $ t}
+ else error "Type o expected in mk_prop";
(** read cterms **) (*exception ERROR*)