--- a/src/HOL/HOL.thy Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/HOL.thy Thu Feb 28 16:54:52 2013 +0100
@@ -699,8 +699,6 @@
and [sym] = sym not_sym
and [Pure.elim?] = iffD1 iffD2 impE
-ML_file "Tools/hologic.ML"
-
subsubsection {* Atomizing meta-level connectives *}
@@ -782,6 +780,9 @@
subsection {* Package setup *}
+ML_file "Tools/hologic.ML"
+
+
subsubsection {* Sledgehammer setup *}
text {*
--- a/src/HOL/List.thy Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/List.thy Thu Feb 28 16:54:52 2013 +0100
@@ -514,11 +514,6 @@
Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
| _ => raise CTERM ("Collect_conv", [ct]))
-fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
-
fun eq_conv cv1 cv2 ct =
(case Thm.term_of ct of
Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
@@ -536,7 +531,7 @@
(rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
fun right_hand_set_comprehension_conv conv ctxt =
- Trueprop_conv (eq_conv Conv.all_conv
+ HOLogic.Trueprop_conv (eq_conv Conv.all_conv
(Collect_conv (all_exists_conv conv o #2) ctxt))
@@ -628,7 +623,7 @@
Conv.all_conv)
then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
then_conv conjunct_assoc_conv)) context
- then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
+ then_conv (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
Conv.repeat_conv
(all_but_last_exists_conv
(K (rewr_conv'
@@ -644,7 +639,7 @@
(Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
Conv.all_conv then_conv
(rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
- Trueprop_conv
+ HOLogic.Trueprop_conv
(eq_conv Conv.all_conv
(Collect_conv (fn (_, ctxt) =>
Conv.repeat_conv
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Feb 28 16:54:52 2013 +0100
@@ -365,7 +365,7 @@
val unfold_ret_val_invs = Conv.bottom_conv
(K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
- val simp_conv = Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
+ val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
val beta_conv = Thm.beta_conversion true
--- a/src/HOL/Tools/Lifting/lifting_util.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Thu Feb 28 16:54:52 2013 +0100
@@ -7,7 +7,6 @@
signature LIFTING_UTIL =
sig
val MRSL: thm list * thm -> thm
- val Trueprop_conv: conv -> conv
val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
val dest_Quotient: term -> term * term * term * term
@@ -26,11 +25,6 @@
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
-fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
-
fun option_fold a _ NONE = a
| option_fold _ f (SOME x) = f x
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Feb 28 16:54:52 2013 +0100
@@ -303,15 +303,10 @@
Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
| _ => Conv.all_conv ct
-fun Trueprop_conv cv ct =
- case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise Fail "Trueprop_conv"
-
fun preprocess_intro thy rule =
Conv.fconv_rule
(imp_prems_conv
- (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
+ (HOLogic.Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
(Thm.transfer thy rule)
fun translate_intros ensure_groundness ctxt gr const constant_table =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Feb 28 16:54:52 2013 +0100
@@ -1158,15 +1158,11 @@
(* preprocessing rules *)
-fun Trueprop_conv cv ct =
- case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise Fail "Trueprop_conv"
-
fun preprocess_equality thy rule =
Conv.fconv_rule
(imp_prems_conv
- (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
+ (HOLogic.Trueprop_conv
+ (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
(Thm.transfer thy rule)
fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
--- a/src/HOL/Tools/hologic.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/hologic.ML Thu Feb 28 16:54:52 2013 +0100
@@ -15,6 +15,7 @@
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
+ val Trueprop_conv: conv -> conv
val mk_induct_forall: typ -> term
val mk_setT: typ -> typ
val dest_setT: typ -> typ
@@ -195,13 +196,19 @@
(* logic *)
-val Trueprop = Const ("HOL.Trueprop", boolT --> propT);
+val Trueprop = Const (@{const_name Trueprop}, boolT --> propT);
fun mk_Trueprop P = Trueprop $ P;
-fun dest_Trueprop (Const ("HOL.Trueprop", _) $ P) = P
+fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
+fun Trueprop_conv cv ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+ | _ => raise CTERM ("Trueprop_conv", [ct]))
+
+
fun conj_intr thP thQ =
let
val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
--- a/src/HOL/Tools/numeral.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/numeral.ML Thu Feb 28 16:54:52 2013 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/numeral.ML
Author: Makarius
-Logical operations on numerals (see also HOL/hologic.ML).
+Logical operations on numerals (see also HOL/Tools/hologic.ML).
*)
signature NUMERAL =
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Feb 28 16:54:52 2013 +0100
@@ -307,12 +307,6 @@
val prod_case_distrib = @{lemma "(prod_case g x) z = prod_case (% x y. (g x y) z) x" by (simp add: prod_case_beta)}
-(* FIXME: one of many clones *)
-fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
-
(* FIXME: another clone *)
fun eq_conv cv1 cv2 ct =
(case Thm.term_of ct of
@@ -337,7 +331,7 @@
ORELSE' rtac
@{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
- (Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
+ (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
fun elim_image_tac ss = etac @{thm imageE}
THEN' REPEAT_DETERM o CHANGED o
@@ -488,7 +482,7 @@
fun mk_thm (fm, t''') = Goal.prove ctxt' [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t'', t'''))) (fn {context, ...} => tac ss' context fm 1)
fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
- val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
+ val post = Conv.fconv_rule (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
val export = singleton (Variable.export ctxt' ctxt)
in
Option.map (export o post o unfold o mk_thm) (rewrite_term t'')
--- a/src/HOL/Tools/transfer.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/transfer.ML Thu Feb 28 16:54:52 2013 +0100
@@ -98,16 +98,11 @@
val (cU, _) = dest_funcT cT'
in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
-fun Trueprop_conv cv ct =
- (case Thm.term_of ct of
- Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
- | _ => raise CTERM ("Trueprop_conv", [ct]))
-
(* Conversion to preprocess a transfer rule *)
fun prep_conv ct = (
Conv.implies_conv Conv.all_conv prep_conv
else_conv
- Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
+ HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
else_conv
Conv.all_conv) ct