# HG changeset patch
# User clasohm
# Date 824212644 -3600
# Node ID e936723cb94dd9c7db3645ccfb9f9c006f4b4061
# Parent  4e617b8f97abb844197b37c651d407baf07b6352
added dest_comb, dest_abs and mk_prop for manipulating cterms

diff -r 4e617b8f97ab -r e936723cb94d src/Pure/thm.ML
--- 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*)