just one HOLogic.Trueprop_conv, with regular exception CTERM;
authorwenzelm
Thu Feb 28 16:54:52 2013 +0100 (2013-02-28)
changeset 51314eac4bb5adbf9
parent 51313 102a0a0718c5
child 51315 536a5603a138
just one HOLogic.Trueprop_conv, with regular exception CTERM;
tuned;
src/HOL/HOL.thy
src/HOL/List.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_util.ML
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/HOL/Tools/transfer.ML
     1.1 --- a/src/HOL/HOL.thy	Thu Feb 28 16:38:17 2013 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Feb 28 16:54:52 2013 +0100
     1.3 @@ -699,8 +699,6 @@
     1.4    and [sym] = sym not_sym
     1.5    and [Pure.elim?] = iffD1 iffD2 impE
     1.6  
     1.7 -ML_file "Tools/hologic.ML"
     1.8 -
     1.9  
    1.10  subsubsection {* Atomizing meta-level connectives *}
    1.11  
    1.12 @@ -782,6 +780,9 @@
    1.13  
    1.14  subsection {* Package setup *}
    1.15  
    1.16 +ML_file "Tools/hologic.ML"
    1.17 +
    1.18 +
    1.19  subsubsection {* Sledgehammer setup *}
    1.20  
    1.21  text {*
     2.1 --- a/src/HOL/List.thy	Thu Feb 28 16:38:17 2013 +0100
     2.2 +++ b/src/HOL/List.thy	Thu Feb 28 16:54:52 2013 +0100
     2.3 @@ -514,11 +514,6 @@
     2.4      Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
     2.5    | _ => raise CTERM ("Collect_conv", [ct]))
     2.6  
     2.7 -fun Trueprop_conv cv ct =
     2.8 -  (case Thm.term_of ct of
     2.9 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    2.10 -  | _ => raise CTERM ("Trueprop_conv", [ct]))
    2.11 -
    2.12  fun eq_conv cv1 cv2 ct =
    2.13    (case Thm.term_of ct of
    2.14      Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    2.15 @@ -536,7 +531,7 @@
    2.16      (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
    2.17  
    2.18  fun right_hand_set_comprehension_conv conv ctxt =
    2.19 -  Trueprop_conv (eq_conv Conv.all_conv
    2.20 +  HOLogic.Trueprop_conv (eq_conv Conv.all_conv
    2.21      (Collect_conv (all_exists_conv conv o #2) ctxt))
    2.22  
    2.23  
    2.24 @@ -628,7 +623,7 @@
    2.25                          Conv.all_conv)
    2.26                          then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
    2.27                          then_conv conjunct_assoc_conv)) context
    2.28 -                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
    2.29 +                    then_conv (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
    2.30                        Conv.repeat_conv
    2.31                          (all_but_last_exists_conv
    2.32                            (K (rewr_conv'
    2.33 @@ -644,7 +639,7 @@
    2.34                            (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
    2.35                          Conv.all_conv then_conv
    2.36                          (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
    2.37 -                      Trueprop_conv
    2.38 +                      HOLogic.Trueprop_conv
    2.39                          (eq_conv Conv.all_conv
    2.40                            (Collect_conv (fn (_, ctxt) =>
    2.41                              Conv.repeat_conv
     3.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 28 16:38:17 2013 +0100
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Feb 28 16:54:52 2013 +0100
     3.3 @@ -365,7 +365,7 @@
     3.4      
     3.5      val unfold_ret_val_invs = Conv.bottom_conv 
     3.6        (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
     3.7 -    val simp_conv = Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
     3.8 +    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
     3.9      val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
    3.10      val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
    3.11      val beta_conv = Thm.beta_conversion true
     4.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Thu Feb 28 16:38:17 2013 +0100
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Thu Feb 28 16:54:52 2013 +0100
     4.3 @@ -7,7 +7,6 @@
     4.4  signature LIFTING_UTIL =
     4.5  sig
     4.6    val MRSL: thm list * thm -> thm
     4.7 -  val Trueprop_conv: conv -> conv
     4.8    val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
     4.9    val dest_Quotient: term -> term * term * term * term
    4.10  
    4.11 @@ -26,11 +25,6 @@
    4.12  
    4.13  fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    4.14  
    4.15 -fun Trueprop_conv cv ct =
    4.16 -  (case Thm.term_of ct of
    4.17 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    4.18 -  | _ => raise CTERM ("Trueprop_conv", [ct]))
    4.19 -
    4.20  fun option_fold a _ NONE = a
    4.21    | option_fold _ f (SOME x) = f x
    4.22  
     5.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 28 16:38:17 2013 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Feb 28 16:54:52 2013 +0100
     5.3 @@ -303,15 +303,10 @@
     5.4      Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
     5.5    | _ => Conv.all_conv ct
     5.6  
     5.7 -fun Trueprop_conv cv ct =
     5.8 -  case Thm.term_of ct of
     5.9 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
    5.10 -  | _ => raise Fail "Trueprop_conv"
    5.11 -
    5.12  fun preprocess_intro thy rule =
    5.13    Conv.fconv_rule
    5.14      (imp_prems_conv
    5.15 -      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
    5.16 +      (HOLogic.Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq}))))
    5.17      (Thm.transfer thy rule)
    5.18  
    5.19  fun translate_intros ensure_groundness ctxt gr const constant_table =
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 28 16:38:17 2013 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 28 16:54:52 2013 +0100
     6.3 @@ -1158,15 +1158,11 @@
     6.4  
     6.5  (* preprocessing rules *)
     6.6  
     6.7 -fun Trueprop_conv cv ct =
     6.8 -  case Thm.term_of ct of
     6.9 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
    6.10 -  | _ => raise Fail "Trueprop_conv"
    6.11 -
    6.12  fun preprocess_equality thy rule =
    6.13    Conv.fconv_rule
    6.14      (imp_prems_conv
    6.15 -      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
    6.16 +      (HOLogic.Trueprop_conv
    6.17 +        (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
    6.18      (Thm.transfer thy rule)
    6.19  
    6.20  fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
     7.1 --- a/src/HOL/Tools/hologic.ML	Thu Feb 28 16:38:17 2013 +0100
     7.2 +++ b/src/HOL/Tools/hologic.ML	Thu Feb 28 16:54:52 2013 +0100
     7.3 @@ -15,6 +15,7 @@
     7.4    val Trueprop: term
     7.5    val mk_Trueprop: term -> term
     7.6    val dest_Trueprop: term -> term
     7.7 +  val Trueprop_conv: conv -> conv
     7.8    val mk_induct_forall: typ -> term
     7.9    val mk_setT: typ -> typ
    7.10    val dest_setT: typ -> typ
    7.11 @@ -195,13 +196,19 @@
    7.12  
    7.13  (* logic *)
    7.14  
    7.15 -val Trueprop = Const ("HOL.Trueprop", boolT --> propT);
    7.16 +val Trueprop = Const (@{const_name Trueprop}, boolT --> propT);
    7.17  
    7.18  fun mk_Trueprop P = Trueprop $ P;
    7.19  
    7.20 -fun dest_Trueprop (Const ("HOL.Trueprop", _) $ P) = P
    7.21 +fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
    7.22    | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    7.23  
    7.24 +fun Trueprop_conv cv ct =
    7.25 +  (case Thm.term_of ct of
    7.26 +    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    7.27 +  | _ => raise CTERM ("Trueprop_conv", [ct]))
    7.28 +
    7.29 +
    7.30  fun conj_intr thP thQ =
    7.31    let
    7.32      val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
     8.1 --- a/src/HOL/Tools/numeral.ML	Thu Feb 28 16:38:17 2013 +0100
     8.2 +++ b/src/HOL/Tools/numeral.ML	Thu Feb 28 16:54:52 2013 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  (*  Title:      HOL/Tools/numeral.ML
     8.5      Author:     Makarius
     8.6  
     8.7 -Logical operations on numerals (see also HOL/hologic.ML).
     8.8 +Logical operations on numerals (see also HOL/Tools/hologic.ML).
     8.9  *)
    8.10  
    8.11  signature NUMERAL =
     9.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Feb 28 16:38:17 2013 +0100
     9.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Feb 28 16:54:52 2013 +0100
     9.3 @@ -307,12 +307,6 @@
     9.4  
     9.5  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)}
     9.6  
     9.7 -(* FIXME: one of many clones *)
     9.8 -fun Trueprop_conv cv ct =
     9.9 -  (case Thm.term_of ct of
    9.10 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    9.11 -  | _ => raise CTERM ("Trueprop_conv", [ct]))
    9.12 -
    9.13  (* FIXME: another clone *)
    9.14  fun eq_conv cv1 cv2 ct =
    9.15    (case Thm.term_of ct of
    9.16 @@ -337,7 +331,7 @@
    9.17        ORELSE' rtac
    9.18          @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}
    9.19        ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
    9.20 -        (Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
    9.21 +        (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
    9.22  
    9.23  fun elim_image_tac ss = etac @{thm imageE}
    9.24    THEN' REPEAT_DETERM o CHANGED o
    9.25 @@ -488,7 +482,7 @@
    9.26      fun mk_thm (fm, t''') = Goal.prove ctxt' [] []
    9.27        (HOLogic.mk_Trueprop (HOLogic.mk_eq (t'', t'''))) (fn {context, ...} => tac ss' context fm 1)
    9.28      fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
    9.29 -    val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
    9.30 +    val post = Conv.fconv_rule (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
    9.31      val export = singleton (Variable.export ctxt' ctxt)
    9.32    in
    9.33      Option.map (export o post o unfold o mk_thm) (rewrite_term t'')
    10.1 --- a/src/HOL/Tools/transfer.ML	Thu Feb 28 16:38:17 2013 +0100
    10.2 +++ b/src/HOL/Tools/transfer.ML	Thu Feb 28 16:54:52 2013 +0100
    10.3 @@ -98,16 +98,11 @@
    10.4        val (cU, _) = dest_funcT cT'
    10.5    in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
    10.6  
    10.7 -fun Trueprop_conv cv ct =
    10.8 -  (case Thm.term_of ct of
    10.9 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
   10.10 -  | _ => raise CTERM ("Trueprop_conv", [ct]))
   10.11 -
   10.12  (* Conversion to preprocess a transfer rule *)
   10.13  fun prep_conv ct = (
   10.14        Conv.implies_conv Conv.all_conv prep_conv
   10.15        else_conv
   10.16 -      Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
   10.17 +      HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
   10.18        else_conv
   10.19        Conv.all_conv) ct
   10.20