--- a/Quot/Nominal/Perm.thy	Wed Feb 24 17:32:22 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 24 17:32:43 2010 +0100
@@ -9,7 +9,55 @@
 *}
 
 ML {*
+fun prove_perm_empty lthy induct perm_def perm_frees =
+let
+  val perm_types = map fastype_of perm_frees;
+  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  val gl =
+    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map (fn ((perm, T), x) => HOLogic.mk_eq
+          (perm $ @{term "0 :: perm"} $ Free (x, T),
+           Free (x, T)))
+       (perm_frees ~~
+        map body_type perm_types ~~ perm_indnames)));
+  fun tac _ =
+    EVERY [
+      indtac induct perm_indnames 1,
+      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
+    ];
+in
+  split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
+end;
+*}
 
+ML {*
+fun prove_perm_append lthy induct perm_def perm_frees =
+let
+  val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
+  val pi1 = Free ("pi1", @{typ perm});
+  val pi2 = Free ("pi2", @{typ perm});
+  val perm_types = map fastype_of perm_frees
+  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
+  val gl =
+    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
+      (map (fn ((perm, T), x) =>
+          let
+            val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
+            val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
+          in HOLogic.mk_eq (lhs, rhs)
+          end)
+        (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
+  fun tac _ =
+    EVERY [
+      indtac induct perm_indnames 1,
+      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
+    ]
+in
+  split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac)
+end;
+*}
+
+ML {*
 (* TODO: full_name can be obtained from new_type_names with Datatype *)
 fun define_raw_perms new_type_names full_tnames thy =
 let
@@ -22,7 +70,6 @@
   val perm_types = map (fn (i, _) =>
     let val T = nth_dtyp i
     in @{typ perm} --> T --> T end) descr;
-  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
   val perm_names_types' = perm_names' ~~ perm_types;
   val pi = Free ("pi", @{typ perm});
   fun perm_eq_constr i (cname, dts) =
@@ -60,48 +107,21 @@
         (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
     val perm_frees =
       (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);
-    val perm_empty_thms =
-      let
-        val gl =
-          HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-            (map (fn ((perm, T), x) => HOLogic.mk_eq
-                (perm $ @{term "0 :: perm"} $ Free (x, T),
-                 Free (x, T)))
-             (perm_frees ~~
-              map body_type perm_types ~~ perm_indnames)));
-        fun tac {context = ctxt, ...} =
-          EVERY [
-            indtac induct perm_indnames 1,
-            ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))
-          ];
-      in
-        (List.take (split_conj_thm (Goal.prove lthy' perm_indnames [] gl tac), length new_type_names))
-      end;
-    val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
-    val pi1 = Free ("pi1", @{typ perm});
-    val pi2 = Free ("pi2", @{typ perm});
-    val perm_append_thms =
-       List.take ((split_conj_thm
-         (Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) []
-            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-               (map (fn ((perm, T), x) =>
-                   let
-                     val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
-                     val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
-                   in HOLogic.mk_eq (lhs, rhs)
-                   end)
-                 (perm_frees ~~
-                  map body_type perm_types ~~ perm_indnames))))
-            (fn _ => EVERY [indtac induct perm_indnames 1,
-               ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))),
-          length new_type_names);
-    fun tac ctxt perm_thms =
+    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
+    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
+    val perms_name = space_implode "_" perm_names'
+    val perms_zero_bind = Binding.name (perms_name ^ "_zero")
+    val perms_append_bind = Binding.name (perms_name ^ "_append")
+    fun tac _ perm_thms =
       (Class.intro_classes_tac []) THEN (ALLGOALS (
-        simp_tac (@{simpset} addsimps perm_thms
+        simp_tac (HOL_ss addsimps perm_thms
       )));
     fun morphism phi = map (Morphism.thm phi);
   in
-    Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy'
+  lthy'
+  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
+  |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
+  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms)
   end
 
 *}