--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/comp_simproc.ML	Wed Sep 03 18:12:36 2008 +0200
@@ -0,0 +1,111 @@
+
+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
+