--- a/src/Pure/drule.ML Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/drule.ML Fri Oct 24 17:13:21 1997 +0200
@@ -68,10 +68,10 @@
val zero_var_indexes : thm -> thm
end;
-
structure Drule : DRULE =
struct
+
(** some cterm->cterm operations: much faster than calling cterm_of! **)
(** SAME NAMES as in structure Logic: use compound identifiers! **)
@@ -389,22 +389,22 @@
(*** Meta-Rewriting Rules ***)
val reflexive_thm =
- let val cx = cterm_of Sign.proto_pure (Var(("x",0),TVar(("'a",0),logicS)))
+ let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
in Thm.reflexive cx end;
val symmetric_thm =
- let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
+ let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
val transitive_thm =
- let val xy = read_cterm Sign.proto_pure ("x::'a::logic == y",propT)
- val yz = read_cterm Sign.proto_pure ("y::'a::logic == z",propT)
+ let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
+ val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
val xythm = Thm.assume xy and yzthm = Thm.assume yz
in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
(** Below, a "conversion" has type cterm -> thm **)
-val refl_implies = reflexive (cterm_of Sign.proto_pure implies);
+val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
(*Do not rewrite flex-flex pairs*)
@@ -474,8 +474,8 @@
end
handle THM _ => err th | bind => err th
in
-val flexpair_intr = flexpair_inst (symmetric flexpair_def)
-and flexpair_elim = flexpair_inst flexpair_def
+val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def)
+and flexpair_elim = flexpair_inst ProtoPure.flexpair_def
end;
(*Version for flexflex pairs -- this supports lifting.*)
@@ -486,17 +486,17 @@
(*** Some useful meta-theorems ***)
(*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = trivial(read_cterm Sign.proto_pure ("PROP ?psi",propT));
+val asm_rl = trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT));
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
-val cut_rl = trivial(read_cterm Sign.proto_pure
+val cut_rl = trivial(read_cterm (sign_of ProtoPure.thy)
("PROP ?psi ==> PROP ?theta", propT));
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
[| PROP V; PROP V ==> PROP W |] ==> PROP W *)
val revcut_rl =
- let val V = read_cterm Sign.proto_pure ("PROP V", propT)
- and VW = read_cterm Sign.proto_pure ("PROP V ==> PROP W", propT);
+ let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
+ and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
in standard (implies_intr V
(implies_intr VW
(implies_elim (assume VW) (assume V))))
@@ -504,16 +504,16 @@
(*for deleting an unwanted assumption*)
val thin_rl =
- let val V = read_cterm Sign.proto_pure ("PROP V", propT)
- and W = read_cterm Sign.proto_pure ("PROP W", propT);
+ let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
+ and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
in standard (implies_intr V (implies_intr W (assume W)))
end;
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
val triv_forall_equality =
- let val V = read_cterm Sign.proto_pure ("PROP V", propT)
- and QV = read_cterm Sign.proto_pure ("!!x::'a. PROP V", propT)
- and x = read_cterm Sign.proto_pure ("x", TFree("'a",logicS));
+ let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
+ and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
+ and x = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
in standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
(implies_intr V (forall_intr x (assume V))))
end;
@@ -523,12 +523,12 @@
`thm COMP swap_prems_rl' swaps the first two premises of `thm'
*)
val swap_prems_rl =
- let val cmajor = read_cterm Sign.proto_pure
+ let val cmajor = read_cterm (sign_of ProtoPure.thy)
("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
val major = assume cmajor;
- val cminor1 = read_cterm Sign.proto_pure ("PROP PhiA", propT);
+ val cminor1 = read_cterm (sign_of ProtoPure.thy) ("PROP PhiA", propT);
val minor1 = assume cminor1;
- val cminor2 = read_cterm Sign.proto_pure ("PROP PhiB", propT);
+ val cminor2 = read_cterm (sign_of ProtoPure.thy) ("PROP PhiB", propT);
val minor2 = assume cminor2;
in standard
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
@@ -540,8 +540,8 @@
Introduction rule for == using ==> not meta-hyps.
*)
val equal_intr_rule =
- let val PQ = read_cterm Sign.proto_pure ("PROP phi ==> PROP psi", propT)
- and QP = read_cterm Sign.proto_pure ("PROP psi ==> PROP phi", propT)
+ let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
+ and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
in equal_intr (assume PQ) (assume QP)
|> implies_intr QP
|> implies_intr PQ
--- a/src/Pure/tactic.ML Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/tactic.ML Fri Oct 24 17:13:21 1997 +0200
@@ -310,7 +310,7 @@
increment revcut_rl instead.*)
fun make_elim_preserve rl =
let val {maxidx,...} = rep_thm rl
- fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
+ fun cvar ixn = cterm_of (sign_of ProtoPure.thy) (Var(ixn,propT));
val revcut_rl' =
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)),
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
--- a/src/Pure/tctical.ML Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/tctical.ML Fri Oct 24 17:13:21 1997 +0200
@@ -334,7 +334,7 @@
(*SELECT_GOAL optimization: replace the conclusion by a variable X,
to avoid copying. Proof states have X==concl as an assuption.*)
-val prop_equals = cterm_of Sign.proto_pure
+val prop_equals = cterm_of (sign_of ProtoPure.thy)
(Const("==", propT-->propT-->propT));
fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
@@ -343,7 +343,7 @@
It is paired with a function to undo the transformation. If ct contains
Vars then it returns ct==>ct.*)
fun eq_trivial ct =
- let val xfree = cterm_of Sign.proto_pure (Free (gensym"EQ_TRIVIAL_", propT))
+ let val xfree = cterm_of (sign_of ProtoPure.thy) (Free (gensym"EQ_TRIVIAL_", propT))
val ct_eq_x = mk_prop_equals (ct, xfree)
and refl_ct = reflexive ct
fun restore th =
@@ -367,7 +367,7 @@
(* (!!selct. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*)
val dummy_quant_rl =
- read_cterm Sign.proto_pure ("!!selct::prop. PROP V",propT) |>
+ read_cterm (sign_of ProtoPure.thy) ("!!selct::prop. PROP V",propT) |>
assume |> forall_elim_var 0 |> standard;
(* Prevent the subgoal's assumptions from becoming additional subgoals in the
--- a/src/Pure/unify.ML Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/unify.ML Fri Oct 24 17:13:21 1997 +0200
@@ -41,7 +41,7 @@
and trace_types = ref false (*announce potential incompleteness
of type unification*)
-val sgr = ref(Sign.proto_pure);
+val sgr = ref(Sign.pre_pure);
type binderlist = (string*typ) list;