--- a/CookBook/comp_simproc.ML	Thu Jan 08 22:46:06 2009 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-
-fun dest_relcomp (t as (Const (@{const_name "Collect"}, _) $ Abs (_, pT, ex_exp))) =
-    let
-      val (T1, T2) = HOLogic.dest_prodT pT
-      val qs  = Term.strip_qnt_vars "Ex" ex_exp
-      val bod = Term.strip_qnt_body "Ex" ex_exp
-
-      val (l, r, cond) = case bod of
-        Const ("op &", _) 
-         $ (Const ("op =", _) $ Bound idx
-              $ (Const ("Pair", _) $ l $ r)) 
-         $ cond
-          => if idx = length qs then (l, r, cond)
-            else raise TERM ("dest_relcomp", [t])
-      | _ => raise TERM ("dest_relcomp", [t])
-    in
-      (T1, T2, qs, l, r, cond)
-    end
-  | dest_relcomp t = raise TERM ("dest_relcomp", [t])
-
-fun mk_pair_compr (T1, T2, qs, l, r, cond) =
-    let
-      val pT = HOLogic.mk_prodT (T1, T2)
-      val peq = HOLogic.eq_const pT $ Bound (length qs) $ (HOLogic.pair_const T1 T2 $ l $ r)
-      val bod = HOLogic.mk_conj (peq, cond)
-    in
-      HOLogic.Collect_const pT $
-      Abs ("uu_", pT, fold_rev (fn (a,T) => fn b => HOLogic.exists_const T $ Abs(a, T, b)) qs bod)
-    end
-
-fun join_compr c1 c2 : term = 
-    let
-      val (T1, T2, qs1, l1, r1, cond1) = dest_relcomp c1
-      val (T2, T3, qs2, l2, r2, cond2) = dest_relcomp c2
-
-      val lift = incr_boundvars (length qs2)
-      val cond = HOLogic.mk_conj (HOLogic.eq_const T2 $ lift r1 $ l2,
-                   HOLogic.mk_conj (lift cond1, cond2))
-    in
-      mk_pair_compr
-        (T1, T3, qs1 @ qs2, lift l1, r2, cond)
-    end
-
-val compr_compose_tac'=
-    EVERY1 (map (curry op o DETERM)
-  [rtac @{thm set_ext},
-   rtac @{thm iffI},
-   etac @{thm rel_compE},
-   etac @{thm CollectE},
-   etac @{thm CollectE},
-   single_hyp_subst_tac 0,
-   (fn i => REPEAT_DETERM (etac @{thm exE} i)),
-   K (print_tac "A"),
-   etac @{thm conjE},
-   K (print_tac "B"),
-   etac @{thm conjE},
-   K (print_tac "B'"),
-   etac @{thm Pair_inject},
-   K (print_tac "C"),
-   rotate_tac 1,
-   K (print_tac "D"),
-   etac @{thm Pair_inject},
-   K (print_tac "E"),
-   single_hyp_subst_tac 2,
-   single_hyp_subst_tac 3,
-   single_hyp_subst_tac 3,
-   rtac @{thm CollectI},
-   (fn i => REPEAT_DETERM (rtac @{thm exI} i)),
-   rtac @{thm conjI},
-   rtac @{thm refl},
-   rtac @{thm conjI},
-   assume_tac,
-   rtac @{thm conjI},
-   assume_tac,
-   assume_tac,
-   etac @{thm CollectE},
-   (fn i => REPEAT (etac @{thm exE} i)),
-   etac @{thm conjE},
-   single_hyp_subst_tac 0,
-   etac @{thm conjE},
-   etac @{thm conjE},
-   rtac @{thm rel_compI},
-   rtac @{thm CollectI},
-   (fn i => REPEAT (rtac @{thm exI} i)),
-   rtac @{thm conjI},
-   rtac @{thm refl},
-   assume_tac,
-   rtac @{thm CollectI},
-   (fn i => REPEAT (rtac @{thm exI} i)),
-   rtac @{thm conjI},
-   stac @{thm Pair_eq},
-   rtac @{thm conjI},
-   assume_tac,
-   rtac @{thm refl},
-   assume_tac])
-
-
-fun compose_simproc _ ss ct : thm option =
-    let
-      val thy = theory_of_cterm ct
-      val sCt as (_ $ s $ t) = term_of ct
-      val T = fastype_of sCt
-      val g : term = Logic.mk_equals (sCt, join_compr t s)
-(*      val _ = Output.tracing (Syntax.string_of_term (Simplifier.the_context ss) g)*)
-    in
-      SOME (Goal.prove_internal [] (cterm_of thy g)
-             (K (rtac @{thm eq_reflection} 1
-                 THEN compr_compose_tac')))
-    end
-    handle TERM _ => NONE
-