# HG changeset patch
# User wenzelm
# Date 1149537261 -7200
# Node ID 06cb6743adf69d20d24b4488ca3f6a5a22b88f1d
# Parent  5fe7731d083695a7f9724e1a955babfbf398f888
support embedded terms;

diff -r 5fe7731d0836 -r 06cb6743adf6 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jun 05 21:54:20 2006 +0200
+++ b/src/Pure/drule.ML	Mon Jun 05 21:54:21 2006 +0200
@@ -121,6 +121,9 @@
   val protectD: thm
   val protect_cong: thm
   val implies_intr_protected: cterm list -> thm -> thm
+  val termI: thm
+  val mk_term: cterm -> thm
+  val dest_term: thm -> cterm
   val freeze_all: thm -> thm
   val tvars_of_terms: term list -> (indexname * sort) list
   val vars_of_terms: term list -> (indexname * typ) list
@@ -939,11 +942,12 @@
 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts);
 
 
-(** protected propositions **)
+(** protected propositions and embedded terms **)
 
 local
   val A = cert (Free ("A", propT));
   val prop_def = #1 (freeze_thaw ProtoPure.prop_def);
+  val term_def = #1 (freeze_thaw ProtoPure.term_def);
 in
   val protect = Thm.capply (cert Logic.protectC);
   val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
@@ -951,6 +955,9 @@
   val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard
       (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
+
+  val termI = store_thm "termI" (PureThy.kind_rule PureThy.internalK (standard
+      (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
 end;
 
 fun implies_intr_protected asms th =
@@ -961,6 +968,23 @@
     |> implies_intr_list asms'
   end;
 
+fun mk_term ct =
+  let
+    val {thy, T, ...} = Thm.rep_cterm ct;
+    val cert = Thm.cterm_of thy;
+    val certT = Thm.ctyp_of thy;
+    val a = certT (TVar (("'a", 0), []));
+    val x = cert (Var (("x", 0), T));
+  in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
+
+fun dest_term th =
+  let val cprop = Thm.cprop_of th in
+    if can Logic.dest_term (Thm.term_of cprop) then
+      #2 (Thm.dest_comb cprop)
+    else raise THM ("dest_term", 0, [th])
+  end;
+
+
 
 (** variations on instantiate **)
 
diff -r 5fe7731d0836 -r 06cb6743adf6 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Jun 05 21:54:20 2006 +0200
+++ b/src/Pure/logic.ML	Mon Jun 05 21:54:21 2006 +0200
@@ -48,6 +48,8 @@
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
+  val mk_term: term -> term
+  val dest_term: term -> term
   val occs: term * term -> bool
   val close_form: term -> term
   val combound: term * int * int -> term
@@ -316,7 +318,7 @@
 
 
 
-(** protected propositions **)
+(** protected propositions and embedded terms **)
 
 val protectC = Const ("prop", propT --> propT);
 fun protect t = protectC $ t;
@@ -325,6 +327,12 @@
   | unprotect t = raise TERM ("unprotect", [t]);
 
 
+fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
+
+fun dest_term (Const ("ProtoPure.term", _) $ t) = t
+  | dest_term t = raise TERM ("dest_term", [t]);
+
+
 
 (*** Low-level term operations ***)
 
diff -r 5fe7731d0836 -r 06cb6743adf6 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Jun 05 21:54:20 2006 +0200
+++ b/src/Pure/pure_thy.ML	Mon Jun 05 21:54:21 2006 +0200
@@ -21,6 +21,7 @@
     sig
       val thy: theory
       val prop_def: thm
+      val term_def: thm
       val conjunction_def: thm
     end
 end;
@@ -585,6 +586,7 @@
     ("_DDDOT",   "logic",                 Delimfix "\\<dots>")]
   |> Theory.add_modesyntax ("", false)
    [("prop", "prop => prop", Mixfix ("_", [0], 0)),
+    ("ProtoPure.term", "'a => prop", Delimfix "TERM _"),
     ("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
   |> Theory.add_modesyntax ("HTML", false)
    [("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
@@ -605,12 +607,14 @@
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Sign.local_path
   |> Theory.add_consts
-   [("conjunction", "prop => prop => prop", NoSyn)]
+   [("term", "'a => prop", NoSyn),
+    ("conjunction", "prop => prop => prop", NoSyn)]
   |> (add_defs false o map Thm.no_attributes)
    [("prop_def", "prop(A) == A"),
+    ("term_def", "term(x) == (!!A. PROP A ==> PROP A)"),
     ("conjunction_def",
       "conjunction(A, B) == (!!C. (PROP A ==> PROP B ==> PROP C) ==> PROP C)")] |> snd
-  |> Sign.hide_consts false ["conjunction"]
+  |> Sign.hide_consts false ["conjunction", "term"]
   |> add_thmss [(("nothing", []), [])] |> snd
   |> Theory.add_axioms_i Proofterm.equality_axms
   |> Theory.end_theory;
@@ -619,6 +623,7 @@
 struct
   val thy = proto_pure;
   val prop_def = get_axiom thy "prop_def";
+  val term_def = get_axiom thy "term_def";
   val conjunction_def = get_axiom thy "conjunction_def";
 end;