--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/Perm.thy	Tue Feb 16 14:57:22 2010 +0100
@@ -0,0 +1,134 @@
+theory Perm
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+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, ... *)
+*}
+
+instantiation rtrm1 and bp :: pt
+begin
+
+
+ML {*
+  val {descr, induct, ...} = Datatype.the_info @{theory} "Perm.rtrm1";
+  val new_type_names = ["rtrm1", "bp"];
+  (* 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 {*
+  val perm_eqs = maps (fn (i, (_, _, constrs)) =>
+    let val T = nth_dtyp i
+    in map (fn (cname, dts) =>
+      let
+        val Ts = map (typ_of_dtyp descr sorts) dts;
+        val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
+        val args = map Free (names ~~ Ts);
+        val c = Const (cname, Ts ---> T);
+        fun perm_arg (dt, x) =
+          let val T = type_of x
+          in
+            if is_rec_type dt then
+              let val (Us, _) = strip_type T
+              in list_abs (map (pair "x") Us,
+                Free (nth perm_names_types' (body_index dt)) $ pi $
+                  list_comb (x, map (fn (i, U) =>
+                    (permute U) $ (minus_perm $ pi) $ Bound i)
+                    ((length Us - 1 downto 0) ~~ Us)))
+              end
+            else (permute T) $ pi $ x
+          end;
+      in
+        (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
+          (Free (nth perm_names_types' i) $
+             Free ("pi", @{typ perm}) $ list_comb (c, args),
+           list_comb (c, map perm_arg (dts ~~ args)))))
+      end) constrs
+    end) descr;
+*}
+
+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_global @{theory} [] [] gl tac),
+       length new_type_names))
+     end
+*}
+
+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_global @{theory} [] []
+           (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)
+*}
+
+instance
+apply(tactic {*
+ (Class.intro_classes_tac []) THEN
+ (ALLGOALS (simp_tac (@{simpset} addsimps (perm_empty_thms @ perm_append_thms)))) *})
+done
+end