--- a/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 08:16:54 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 10:28:17 2010 +0200
@@ -371,144 +371,4 @@
 (* apply(perm_strict_simp) *)
 oops
 
-atom_decl var
-
-ML {*
-val inductive_atomize = @{thms induct_atomize};
-
-val atomize_conv =
-  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
-    (HOL_basic_ss addsimps inductive_atomize);
-val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
-fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
-  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
-
-fun map_term f t u = (case f t u of
-      NONE => map_term' f t u | x => x)
-and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of
-      (NONE, NONE) => NONE
-    | (SOME t'', NONE) => SOME (t'' $ u)
-    | (NONE, SOME u'') => SOME (t $ u'')
-    | (SOME t'', SOME u'') => SOME (t'' $ u''))
-  | map_term' f (Abs (s, T, t)) (Abs (s', T', t')) = (case map_term f t t' of
-      NONE => NONE
-    | SOME t'' => SOME (Abs (s, T, t'')))
-  | map_term' _ _ _ = NONE;
-
-
-fun map_thm ctxt f tac monos opt th =
-  let
-    val prop = prop_of th;
-    fun prove t =
-      Goal.prove ctxt [] [] t (fn _ =>
-        EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
-          REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
-          REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
-  in Option.map prove (map_term f prop (the_default prop opt)) end;
-
-fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
-      Const (name, _) =>
-        if name mem names then SOME (f p q) else NONE
-    | _ => NONE)
-  | split_conj _ _ _ _ = NONE;
-*}
-
-ML {*
-val perm_bool = @{thm "permute_bool_def"};
-val perm_boolI = @{thm "permute_boolI"};
-val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
-  (Drule.strip_imp_concl (cprop_of perm_boolI))));
-
-fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
-  [(perm_boolI_pi, pi)] perm_boolI;
-
-*}
-
-ML {*
-fun transp ([] :: _) = []
-  | transp xs = map hd xs :: transp (map tl xs);
-
-fun prove_eqvt s xatoms ctxt =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val ({names, ...}, {raw_induct, intrs, elims, ...}) =
-      Inductive.the_inductive ctxt (Sign.intern_const thy s);
-    val raw_induct = atomize_induct ctxt raw_induct;
-    val elims = map (atomize_induct ctxt) elims;
-    val intrs = map atomize_intr intrs;
-    val monos = Inductive.get_monos ctxt;
-    val intrs' = Inductive.unpartition_rules intrs
-      (map (fn (((s, ths), (_, k)), th) =>
-           (s, ths ~~ Inductive.infer_intro_vars th k ths))
-         (Inductive.partition_rules raw_induct intrs ~~
-          Inductive.arities_of raw_induct ~~ elims));
-    val k = length (Inductive.params_of raw_induct);
-    val atoms' = ["var"];
-    val atoms =
-      if null xatoms then atoms' else
-      let val atoms = map (Sign.intern_type thy) xatoms
-      in
-        (case duplicates op = atoms of
-             [] => ()
-           | xs => error ("Duplicate atoms: " ^ commas xs);
-         case subtract (op =) atoms' atoms of
-             [] => ()
-           | xs => error ("No such atoms: " ^ commas xs);
-         atoms)
-      end;
-    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
-    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
-      (Nominal_ThmDecls.get_eqvts_thms ctxt @ perm_pi_simp);
-    val (([t], [pi]), ctxt') = ctxt |>
-      Variable.import_terms false [concl_of raw_induct] ||>>
-      Variable.variant_fixes ["pi"];
-    val ps = map (fst o HOLogic.dest_imp)
-      (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
-    fun eqvt_tac ctxt'' pi (intr, vs) st =
-      let
-        fun eqvt_err s =
-          let val ([t], ctxt''') = Variable.import_terms true [prop_of intr] ctxt
-          in error ("Could not prove equivariance for introduction rule\n" ^
-            Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
-          end;
-        val res = SUBPROOF (fn {prems, params, ...} =>
-          let
-            val prems' = map (fn th => the_default th (map_thm ctxt'
-              (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
-            val prems'' = map (fn th => Simplifier.simplify eqvt_ss
-              (mk_perm_bool (cterm_of thy pi) th)) prems';
-            val intr' = intr 
-          in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
-          end) ctxt' 1 st
-      in
-        case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
-          NONE => eqvt_err ("Rule does not match goal\n" ^
-            Syntax.string_of_term ctxt'' (hd (prems_of st)))
-        | SOME (th, _) => Seq.single th
-      end;
-    val thss = map (fn atom =>
-      let val pi' = Free (pi, @{typ perm})
-      in map (fn th => zero_var_indexes (th RS mp))
-        (Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] []
-          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn p =>
-            let
-              val (h, ts) = strip_comb p;
-              val (ts1, ts2) = chop k ts
-            in
-              HOLogic.mk_imp (p, list_comb (h, ts1))
-            end) ps)))
-          (fn {context, ...} => EVERY (rtac raw_induct 1 :: map (fn intr_vs =>
-              full_simp_tac eqvt_ss 1 THEN
-              eqvt_tac context pi' intr_vs) intrs')) |>
-          singleton (ProofContext.export ctxt' ctxt)))
-      end) atoms
-  in
-    ctxt |>
-    Local_Theory.notes (map (fn (name, ths) =>
-        ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
-          [Attrib.internal (K Nominal_ThmDecls.eqvt_add)]), [(ths, [])]))
-      (names ~~ transp thss)) |> snd
-  end;
-*}
-
 end