--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Unused.thy	Thu Oct 15 11:42:14 2009 +0200
@@ -0,0 +1,74 @@
+
+ML {*
+  fun dest_cbinop t =
+    let
+      val (t2, rhs) = Thm.dest_comb t;
+      val (bop, lhs) = Thm.dest_comb t2;
+    in
+      (bop, (lhs, rhs))
+    end
+*}
+
+ML {*
+  fun dest_ceq t =
+    let
+      val (bop, pair) = dest_cbinop t;
+      val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
+    in
+      if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
+    end
+*}
+
+ML {*
+  fun split_binop_conv t =
+    let
+      val (lhs, rhs) = dest_ceq t;
+      val (bop, _) = dest_cbinop lhs;
+      val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+      val [cmT, crT] = Thm.dest_ctyp cr2;
+    in
+      Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
+    end
+*}
+
+
+ML {*
+  fun split_arg_conv t =
+    let
+      val (lhs, rhs) = dest_ceq t;
+      val (lop, larg) = Thm.dest_comb lhs;
+      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+    in
+      Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
+    end
+*}
+
+ML {*
+  fun split_binop_tac n thm =
+    let
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      val rewr = split_binop_conv cconcl;
+    in
+      rtac rewr n thm
+    end
+      handle CTERM _ => Seq.empty
+*}
+
+
+ML {*
+  fun split_arg_tac n thm =
+    let
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      val rewr = split_arg_conv cconcl;
+    in
+      rtac rewr n thm
+    end
+      handle CTERM _ => Seq.empty
+*}
+
+
+lemma trueprop_cong:
+  shows "(a ≡ b) ⟹ (Trueprop a ≡ Trueprop b)"
+  by auto