# HG changeset patch
# User wenzelm
# Date 1362066892 -3600
# Node ID eac4bb5adbf9fcdcdd065cd9ecef8502f8da4f7b
# Parent  102a0a0718c59c5c126b4aadff3957dad89312ac
just one HOLogic.Trueprop_conv, with regular exception CTERM;
tuned;

diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/HOL.thy
--- 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 {*
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/List.thy
--- 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
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/Lifting/lifting_def.ML
--- 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
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/Lifting/lifting_util.ML
--- 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
 
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- 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 =
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- 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
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/hologic.ML
--- 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)
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/numeral.ML
--- 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 =
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/set_comprehension_pointfree.ML
--- 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'')
diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/transfer.ML
--- 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