diff -r b9d02e0800e9 -r a7b4160ef463 Quot/Nominal/Perm.thy
--- a/Quot/Nominal/Perm.thy	Wed Feb 17 10:20:26 2010 +0100
+++ b/Quot/Nominal/Perm.thy	Wed Feb 17 13:54:35 2010 +0100
@@ -1,51 +1,30 @@
 theory Perm
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+imports "Nominal2_Atoms"
 begin
 
-atom_decl name
-
-datatype rtrm1 =
-  rVr1 "name"
-| rAp1 "rtrm1" "rtrm1 list"
-| rLm1 "name" "rtrm1"
-| rLt1 "bp" "rtrm1" "rtrm1"
-and bp =
-  BUnit
-| BVr "name"
-| BPr "bp" "bp"
+ML {*
+  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
+  fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
+  val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
+*}
 
 ML {*
-  open Datatype_Aux (* typ_of_dtyp, DtRec, ... *)
-*}
 
-instantiation rtrm1 and bp :: pt
-begin
-
-
-ML {*
-  val {descr, induct, ...} = Datatype.the_info @{theory} "Perm.rtrm1";
-  val new_type_names = ["rtrm1", "bp"];
+(* TODO: full_name can be obtained from new_type_names with Datatype *)
+fun define_raw_perms new_type_names full_tnames thy =
+let
+  val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames);
   (* TODO: [] should be the sorts that we'll take from the specification *)
   val sorts = [];
-
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "permute_" ^ name_of_typ (nth_dtyp i)) descr);
-  val perm_names = replicate (length new_type_names) @{const_name permute} @
-    map (Sign.full_bname @{theory}) (List.drop (perm_names', length new_type_names));
   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);
-  (* TODO: Next line only needed after instantiation *)
-  val perm_names_types = perm_names ~~ perm_types;
   val perm_names_types' = perm_names' ~~ perm_types;
-
   val pi = Free ("pi", @{typ perm});
-  fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
-  val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
-*}
-ML {*
   fun perm_eq_constr i (cname, dts) =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -71,63 +50,78 @@
            Free ("pi", @{typ perm}) $ list_comb (c, args),
          list_comb (c, map perm_arg (dts ~~ args)))))
     end;
-  fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
-  val perm_eqs = maps perm_eq descr;
-*}
+    fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
+    val perm_eqs = maps perm_eq descr;
+    val lthy =
+      Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+    (* TODO: Use the version of prmrec that gives the names explicitely. *)
+    val (perm_ldef, lthy') =
+      Primrec.add_primrec
+        (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 =
+      (Class.intro_classes_tac []) THEN (ALLGOALS (
+        simp_tac (@{simpset} 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'
+  end
 
-local_setup {*
-snd o (Primrec.add_primrec
-  (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs)
 *}
 
-print_theorems
-
-ML {*
-   val perm_empty_thms =
-     let
-       val gl =
-         HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-           (map (fn ((s, T), x) => HOLogic.mk_eq
-               (Const (s, @{typ perm} --> T --> T) $
-                  @{term "0 :: perm"} $ Free (x, T),
-                Free (x, T)))
-            (perm_names ~~
-             map body_type perm_types ~~ perm_indnames)));
-       fun tac _ =
-         EVERY [indtac induct perm_indnames 1,
-           ALLGOALS (asm_full_simp_tac @{simpset})];
-     in
-       map Drule.export_without_context (List.take (split_conj_thm
-         (Goal.prove @{context} [] [] gl tac),
-       length new_type_names))
-     end
-*}
+(* Test
+atom_decl name
 
-ML {*
-   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 (map Drule.export_without_context (split_conj_thm
-        (Goal.prove @{context} [] []
-           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-              (map (fn ((s, T), x) =>
-                  let
-                    val perm = Const (s, @{typ perm} --> T --> T);
-                    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_names ~~
-                 map body_type perm_types ~~ perm_indnames))))
-           (fn _ => EVERY [indtac induct perm_indnames 1,
-              ALLGOALS (asm_full_simp_tac @{simpset})]))),
-         length new_type_names)
-*}
+datatype rtrm1 =
+  rVr1 "name"
+| rAp1 "rtrm1" "rtrm1 list"
+| rLm1 "name" "rtrm1"
+| rLt1 "bp" "rtrm1" "rtrm1"
+and bp =
+  BUnit
+| BVr "name"
+| BPr "bp" "bp"
 
-instance
-apply(tactic {*
- (Class.intro_classes_tac []) THEN
- (ALLGOALS (simp_tac (@{simpset} addsimps (perm_empty_thms @ perm_append_thms)))) *})
-done
+
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *}
+print_theorems
+*)
+
 end