--- 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 **)
--- 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 ***)
--- 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;