--- a/Nominal/Tacs.thy	Wed Aug 25 22:55:42 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-theory Tacs
-imports Main
-begin
-
-(* General not-nominal/quotient functionality useful for proving *)
-
-(* A version of case_rule_tac that takes more exhaust rules *)
-ML {*
-fun case_rules_tac ctxt0 s rules i st =
-let
-  val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
-  val ty = fastype_of (ProofContext.read_term_schematic ctxt s)
-  fun exhaust_ty thm = fastype_of (hd (Induct.vars_of (Thm.term_of (Thm.cprem_of thm 1))));
-  val ty_rules = filter (fn x => exhaust_ty x = ty) rules;
-in
-  InductTacs.case_rule_tac ctxt0 s (hd ty_rules) i st
-end
-*}
-
-ML {*
-fun mk_conjl props =
-  fold (fn a => fn b =>
-    if a = @{term True} then b else
-    if b = @{term True} then a else
-    HOLogic.mk_conj (a, b)) (rev props) @{term True};
-*}
-
-ML {*
-val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
-
-
-ML {*
-fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =
-let
-  val tys = map (domain_type o fastype_of) alphas;
-  val names = Datatype_Prop.make_tnames tys;
-  val (namesl, ctxt') = Variable.variant_fixes names ctxt;
-  val (namesr, ctxt'') = Variable.variant_fixes names ctxt';
-  val freesl = map Free (namesl ~~ tys);
-  val freesr = map Free (namesr ~~ tys);
-  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ (freesl ~~ freesr))) inputs ctxt'';
-  val gls = flat gls_lists;
-  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
-  val trm_gl_lists = map trm_gls_map freesl;
-  val trm_gls = map mk_conjl trm_gl_lists;
-  val pgls = map
-    (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 
-    ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
-  fun tac {context,...} = (rtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
-    TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1
-  val th_loc = Goal.prove ctxt'' [] [] gl tac
-  val ths_loc = HOLogic.conj_elims th_loc
-  val ths = Variable.export ctxt'' ctxt ths_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
-
-ML {*
-fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
-*}
-
-(* Introduces an implication and immediately eliminates it by cases *)
-ML {*
-fun imp_elim_tac case_rules =
-  Subgoal.FOCUS (fn {concl, context, ...} =>
-    case term_of concl of
-      _ $ (_ $ asm $ _) =>
-        let
-          fun filter_fn case_rule = (
-            case Logic.strip_assums_hyp (prop_of case_rule) of
-              ((_ $ asmc) :: _) =>
-                let
-                  val thy = ProofContext.theory_of context
-                in
-                  Pattern.matches thy (asmc, asm)
-                end
-            | _ => false)
-          val matching_rules = filter filter_fn case_rules
-        in
-         (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
-        end
-    | _ => no_tac)
-*}
-
-ML {*
-fun is_ex (Const ("Ex", _) $ Abs _) = true
-  | is_ex _ = false;
-*}
-
-ML {*
-fun dtyp_no_of_typ _ (TFree (_, _)) = error "dtyp_no_of_typ: Illegal free"
-  | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
-  | dtyp_no_of_typ dts (Type (tname, _)) =
-      case try (find_index (curry op = tname o fst)) dts of
-        NONE => error "dtyp_no_of_typ: Illegal recursion"
-      | SOME i => i
-*}
-
-end
-