support embedded terms;
authorwenzelm
Mon Jun 05 21:54:21 2006 +0200 (2006-06-05)
changeset 1977506cb6743adf6
parent 19774 5fe7731d0836
child 19776 a8c02d8b8b40
support embedded terms;
src/Pure/drule.ML
src/Pure/logic.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/drule.ML	Mon Jun 05 21:54:20 2006 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Jun 05 21:54:21 2006 +0200
     1.3 @@ -121,6 +121,9 @@
     1.4    val protectD: thm
     1.5    val protect_cong: thm
     1.6    val implies_intr_protected: cterm list -> thm -> thm
     1.7 +  val termI: thm
     1.8 +  val mk_term: cterm -> thm
     1.9 +  val dest_term: thm -> cterm
    1.10    val freeze_all: thm -> thm
    1.11    val tvars_of_terms: term list -> (indexname * sort) list
    1.12    val vars_of_terms: term list -> (indexname * typ) list
    1.13 @@ -939,11 +942,12 @@
    1.14  fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts);
    1.15  
    1.16  
    1.17 -(** protected propositions **)
    1.18 +(** protected propositions and embedded terms **)
    1.19  
    1.20  local
    1.21    val A = cert (Free ("A", propT));
    1.22    val prop_def = #1 (freeze_thaw ProtoPure.prop_def);
    1.23 +  val term_def = #1 (freeze_thaw ProtoPure.term_def);
    1.24  in
    1.25    val protect = Thm.capply (cert Logic.protectC);
    1.26    val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
    1.27 @@ -951,6 +955,9 @@
    1.28    val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard
    1.29        (Thm.equal_elim prop_def (Thm.assume (protect A)))));
    1.30    val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
    1.31 +
    1.32 +  val termI = store_thm "termI" (PureThy.kind_rule PureThy.internalK (standard
    1.33 +      (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
    1.34  end;
    1.35  
    1.36  fun implies_intr_protected asms th =
    1.37 @@ -961,6 +968,23 @@
    1.38      |> implies_intr_list asms'
    1.39    end;
    1.40  
    1.41 +fun mk_term ct =
    1.42 +  let
    1.43 +    val {thy, T, ...} = Thm.rep_cterm ct;
    1.44 +    val cert = Thm.cterm_of thy;
    1.45 +    val certT = Thm.ctyp_of thy;
    1.46 +    val a = certT (TVar (("'a", 0), []));
    1.47 +    val x = cert (Var (("x", 0), T));
    1.48 +  in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;
    1.49 +
    1.50 +fun dest_term th =
    1.51 +  let val cprop = Thm.cprop_of th in
    1.52 +    if can Logic.dest_term (Thm.term_of cprop) then
    1.53 +      #2 (Thm.dest_comb cprop)
    1.54 +    else raise THM ("dest_term", 0, [th])
    1.55 +  end;
    1.56 +
    1.57 +
    1.58  
    1.59  (** variations on instantiate **)
    1.60  
     2.1 --- a/src/Pure/logic.ML	Mon Jun 05 21:54:20 2006 +0200
     2.2 +++ b/src/Pure/logic.ML	Mon Jun 05 21:54:21 2006 +0200
     2.3 @@ -48,6 +48,8 @@
     2.4    val protectC: term
     2.5    val protect: term -> term
     2.6    val unprotect: term -> term
     2.7 +  val mk_term: term -> term
     2.8 +  val dest_term: term -> term
     2.9    val occs: term * term -> bool
    2.10    val close_form: term -> term
    2.11    val combound: term * int * int -> term
    2.12 @@ -316,7 +318,7 @@
    2.13  
    2.14  
    2.15  
    2.16 -(** protected propositions **)
    2.17 +(** protected propositions and embedded terms **)
    2.18  
    2.19  val protectC = Const ("prop", propT --> propT);
    2.20  fun protect t = protectC $ t;
    2.21 @@ -325,6 +327,12 @@
    2.22    | unprotect t = raise TERM ("unprotect", [t]);
    2.23  
    2.24  
    2.25 +fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
    2.26 +
    2.27 +fun dest_term (Const ("ProtoPure.term", _) $ t) = t
    2.28 +  | dest_term t = raise TERM ("dest_term", [t]);
    2.29 +
    2.30 +
    2.31  
    2.32  (*** Low-level term operations ***)
    2.33  
     3.1 --- a/src/Pure/pure_thy.ML	Mon Jun 05 21:54:20 2006 +0200
     3.2 +++ b/src/Pure/pure_thy.ML	Mon Jun 05 21:54:21 2006 +0200
     3.3 @@ -21,6 +21,7 @@
     3.4      sig
     3.5        val thy: theory
     3.6        val prop_def: thm
     3.7 +      val term_def: thm
     3.8        val conjunction_def: thm
     3.9      end
    3.10  end;
    3.11 @@ -585,6 +586,7 @@
    3.12      ("_DDDOT",   "logic",                 Delimfix "\\<dots>")]
    3.13    |> Theory.add_modesyntax ("", false)
    3.14     [("prop", "prop => prop", Mixfix ("_", [0], 0)),
    3.15 +    ("ProtoPure.term", "'a => prop", Delimfix "TERM _"),
    3.16      ("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
    3.17    |> Theory.add_modesyntax ("HTML", false)
    3.18     [("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
    3.19 @@ -605,12 +607,14 @@
    3.20    |> Theory.add_trfunsT Syntax.pure_trfunsT
    3.21    |> Sign.local_path
    3.22    |> Theory.add_consts
    3.23 -   [("conjunction", "prop => prop => prop", NoSyn)]
    3.24 +   [("term", "'a => prop", NoSyn),
    3.25 +    ("conjunction", "prop => prop => prop", NoSyn)]
    3.26    |> (add_defs false o map Thm.no_attributes)
    3.27     [("prop_def", "prop(A) == A"),
    3.28 +    ("term_def", "term(x) == (!!A. PROP A ==> PROP A)"),
    3.29      ("conjunction_def",
    3.30        "conjunction(A, B) == (!!C. (PROP A ==> PROP B ==> PROP C) ==> PROP C)")] |> snd
    3.31 -  |> Sign.hide_consts false ["conjunction"]
    3.32 +  |> Sign.hide_consts false ["conjunction", "term"]
    3.33    |> add_thmss [(("nothing", []), [])] |> snd
    3.34    |> Theory.add_axioms_i Proofterm.equality_axms
    3.35    |> Theory.end_theory;
    3.36 @@ -619,6 +623,7 @@
    3.37  struct
    3.38    val thy = proto_pure;
    3.39    val prop_def = get_axiom thy "prop_def";
    3.40 +  val term_def = get_axiom thy "term_def";
    3.41    val conjunction_def = get_axiom thy "conjunction_def";
    3.42  end;
    3.43