--- a/src/HOL/Import/proof_kernel.ML Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Mon May 03 16:26:47 2010 +0200
@@ -2065,7 +2065,7 @@
let
val (HOLThm args) = norm_hthm (theory_of_thm th) hth
in
- apsnd strip_shyps args
+ apsnd Thm.strip_shyps args
end
fun to_isa_term tm = tm
--- a/src/HOL/Import/shuffler.ML Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Import/shuffler.ML Mon May 03 16:26:47 2010 +0200
@@ -502,7 +502,7 @@
t |> disamb_bound thy
|> chain (Simplifier.full_rewrite ss)
|> chain eta_conversion
- |> strip_shyps
+ |> Thm.strip_shyps
val _ = message ("norm_term: " ^ (string_of_thm th))
in
th
--- a/src/HOL/Matrix/cplex/matrixlp.ML Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Matrix/cplex/matrixlp.ML Mon May 03 16:26:47 2010 +0200
@@ -81,7 +81,7 @@
fun matrix_simplify th =
let
val simp_th = matrix_compute (cprop_of th)
- val th = strip_shyps (equal_elim simp_th th)
+ val th = Thm.strip_shyps (equal_elim simp_th th)
fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th (* FIXME avoid handle _ *)
in
removeTrue th
--- a/src/HOL/Tools/cnf_funcs.ML Mon May 03 15:34:55 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Mon May 03 16:26:47 2010 +0200
@@ -436,8 +436,8 @@
val var = new_free ()
val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
@@ -447,8 +447,8 @@
val var = new_free ()
val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
in
iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *)
end
@@ -467,8 +467,8 @@
val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *)
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *)
- val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
- val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
in
iff_trans OF [thm1, thm5]
end
--- a/src/Pure/thm.ML Mon May 03 15:34:55 2010 +0200
+++ b/src/Pure/thm.ML Mon May 03 16:26:47 2010 +0200
@@ -69,7 +69,6 @@
val weaken: cterm -> thm -> thm
val weaken_sorts: sort list -> cterm -> cterm
val extra_shyps: thm -> sort list
- val strip_shyps: thm -> thm
(*meta rules*)
val assume: cterm -> thm
@@ -138,6 +137,7 @@
val varifyT_global: thm -> thm
val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
val of_class: ctyp * class -> thm
+ val strip_shyps: thm -> thm
val unconstrainT: ctyp -> thm -> thm
val unconstrain_allTs: thm -> thm
val freezeT: thm -> thm
@@ -476,26 +476,6 @@
val sorts' = Sorts.union sorts more_sorts;
in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
-
-
-(** sort contexts of theorems **)
-
-(*remove extra sorts that are witnessed by type signature information*)
-fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
- | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
- let
- val thy = Theory.deref thy_ref;
- val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
- val extra = fold (Sorts.remove_sort o #2) present shyps;
- val witnessed = Sign.witness_sorts thy present extra;
- val extra' = fold (Sorts.remove_sort o #2) witnessed extra
- |> Sorts.minimal_sorts (Sign.classes_of thy);
- val shyps' = fold (Sorts.insert_sort o #2) present extra';
- in
- Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
- shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
- end;
-
(*dangling sort constraints of a thm*)
fun extra_shyps (th as Thm (_, {shyps, ...})) =
Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
@@ -1219,6 +1199,22 @@
else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
end;
+(*Remove extra sorts that are witnessed by type signature information*)
+fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
+ | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
+ let
+ val thy = Theory.deref thy_ref;
+ val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
+ val extra = fold (Sorts.remove_sort o #2) present shyps;
+ val witnessed = Sign.witness_sorts thy present extra;
+ val extra' = fold (Sorts.remove_sort o #2) witnessed extra
+ |> Sorts.minimal_sorts (Sign.classes_of thy);
+ val shyps' = fold (Sorts.insert_sort o #2) present extra';
+ in
+ Thm (der, {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
+ shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
+ end;
+
(*Internalize sort constraints of type variable*)
fun unconstrainT
(Ctyp {thy_ref = thy_ref1, T, ...})