--- a/Nominal-General/Nominal2_Eqvt.thy	Mon Apr 12 17:44:26 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Tue Apr 13 00:47:57 2010 +0200
@@ -204,6 +204,9 @@
   shows "supp (set xs) = supp xs"
 *)
 
+lemma map_eqvt: 
+  shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+  by (induct xs) (simp_all, simp only: permute_fun_app_eq)
 
 section {* Product Operations *}
 
@@ -250,7 +253,7 @@
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
-  fst_eqvt snd_eqvt Pair_eqvt permute_list.simps
+  map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps
 
   (* sets *)
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
@@ -368,5 +371,144 @@
 (* 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

--- a/Nominal/Nominal2_FSet.thy	Mon Apr 12 17:44:26 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Tue Apr 13 00:47:57 2010 +0200
@@ -18,14 +18,13 @@
 instantiation FSet.fset :: (pt) pt
 begin
 
-term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
 quotient_definition
   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
-instance proof
+instance 
+proof
   fix x :: "'a fset" and p q :: "perm"
   show "0 \<bullet> x = x"
     by (lifting permute_zero [where 'a="'a list"])
@@ -36,17 +35,12 @@
 end
 
 lemma permute_fset[eqvt]:
-  "p \<bullet> ({||} :: 'a :: pt fset) = {||}"
+  "(p \<bullet> {||}) = ({||} :: 'a::pt fset)"
   "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
   by (lifting permute_list.simps)
 
-lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
-  apply (induct l)
-  apply (simp_all)
-  apply (simp only: eqvt_apply)
-  done
-
-lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
+lemma fmap_eqvt[eqvt]: 
+  shows "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
   by (lifting map_eqvt)
 
 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"