--- a/src/HOL/List.thy Thu Feb 28 16:54:52 2013 +0100
+++ b/src/HOL/List.thy Thu Feb 28 17:14:55 2013 +0100
@@ -514,24 +514,14 @@
Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
| _ => raise CTERM ("Collect_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
- | _ => raise CTERM ("eq_conv", [ct]))
-
-fun conj_conv cv1 cv2 ct =
- (case Thm.term_of ct of
- Const (@{const_name HOL.conj}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
- | _ => raise CTERM ("conj_conv", [ct]))
-
fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
fun conjunct_assoc_conv ct =
Conv.try_conv
- (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
+ (rewr_conv' @{thm conj_assoc} then_conv HOLogic.conj_conv Conv.all_conv conjunct_assoc_conv) ct
fun right_hand_set_comprehension_conv conv ctxt =
- HOLogic.Trueprop_conv (eq_conv Conv.all_conv
+ HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv
(Collect_conv (all_exists_conv conv o #2) ctxt))
@@ -593,14 +583,14 @@
THEN rtac @{thm impI} 1
THEN Subgoal.FOCUS (fn {prems, context, ...} =>
CONVERSION (right_hand_set_comprehension_conv (K
- (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
+ (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
then_conv
rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
THEN tac ctxt cont
THEN rtac @{thm impI} 1
THEN Subgoal.FOCUS (fn {prems, context, ...} =>
CONVERSION (right_hand_set_comprehension_conv (K
- (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
+ (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
THEN rtac set_Nil_I 1
| tac ctxt (Case (T, i) :: cont) =
@@ -617,13 +607,13 @@
(* continue recursively *)
Subgoal.FOCUS (fn {prems, context, ...} =>
CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K
- ((conj_conv
- (eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
+ ((HOLogic.conj_conv
+ (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv
(Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))
Conv.all_conv)
then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
then_conv conjunct_assoc_conv)) context
- then_conv (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
+ then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
Conv.repeat_conv
(all_but_last_exists_conv
(K (rewr_conv'
@@ -633,14 +623,14 @@
Subgoal.FOCUS (fn {prems, context, ...} =>
CONVERSION
(right_hand_set_comprehension_conv (K
- (conj_conv
- ((eq_conv Conv.all_conv
+ (HOLogic.conj_conv
+ ((HOLogic.eq_conv Conv.all_conv
(rewr_conv' (List.last prems))) then_conv
(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
HOLogic.Trueprop_conv
- (eq_conv Conv.all_conv
+ (HOLogic.eq_conv Conv.all_conv
(Collect_conv (fn (_, ctxt) =>
Conv.repeat_conv
(Conv.bottom_conv
--- a/src/HOL/Tools/hologic.ML Thu Feb 28 16:54:52 2013 +0100
+++ b/src/HOL/Tools/hologic.ML Thu Feb 28 17:14:55 2013 +0100
@@ -42,9 +42,11 @@
val disjuncts: term -> term list
val dest_imp: term -> term * term
val dest_not: term -> term
+ val conj_conv: conv -> conv -> conv
val eq_const: typ -> term
val mk_eq: term * term -> term
val dest_eq: term -> term * term
+ val eq_conv: conv -> conv -> conv
val all_const: typ -> term
val mk_all: string * typ * term -> term
val list_all: (string * typ) list * term -> term
@@ -257,12 +259,27 @@
fun dest_not (Const ("HOL.Not", _) $ t) = t
| dest_not t = raise TERM ("dest_not", [t]);
-fun eq_const T = Const ("HOL.eq", T --> T --> boolT);
+
+fun conj_conv cv1 cv2 ct =
+ (case Thm.term_of ct of
+ Const (@{const_name HOL.conj}, _) $ _ $ _ =>
+ Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
+ | _ => raise CTERM ("conj_conv", [ct]));
+
+
+fun eq_const T = Const (@{const_name HOL.eq}, T --> T --> boolT);
+
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const ("HOL.eq", _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
+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
+ | _ => raise CTERM ("eq_conv", [ct]));
+
+
fun all_const T = Const ("HOL.All", (T --> boolT) --> boolT);
fun mk_all (x, T, P) = all_const T $ absfree (x, T) P;
fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Thu Feb 28 16:54:52 2013 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Feb 28 17:14:55 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: another clone *)
-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
- | _ => raise CTERM ("eq_conv", [ct]))
-
val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
val vimageE' =
@{lemma "a \<notin> f -` B ==> (\<And> x. f a = x ==> x \<notin> B ==> P) ==> P" by simp}
@@ -331,7 +325,8 @@
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
- (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
+ (HOLogic.Trueprop_conv
+ (HOLogic.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
@@ -482,7 +477,9 @@
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 (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
+ val post =
+ Conv.fconv_rule
+ (HOLogic.Trueprop_conv (HOLogic.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'')