--- a/Nominal/Perm.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/Perm.thy	Thu May 20 21:23:53 2010 +0100
@@ -1,180 +1,9 @@
 theory Perm
-imports "../Nominal-General/Nominal2_Atoms"
+imports 
+  "../Nominal-General/Nominal2_Base"
+  "../Nominal-General/Nominal2_Atoms"
 begin
 
-(* definitions of the permute function for raw nominal datatypes *)
-
-
-ML {*
-(* returns the type of the nth datatype *)
-fun nth_dtyp descr sorts n = 
-  Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n);
-
-(* returns the constructors of the nth datatype *)
-fun nth_dtyp_constrs descr n = 
-let
-  val (_, (_, _, constrs)) = nth descr n
-in
-  constrs
-end
-
-(* returns the types of the constructors of the nth datatype *)
-fun nth_dtyp_constr_typs descr sorts n = 
-  map (map (Datatype_Aux.typ_of_dtyp descr sorts) o snd) (nth_dtyp_constrs descr n)
-*}
-
-ML {*
-(* generates for every datatype a name str ^ dt_name 
-   plus and index for multiple occurences of a string *)
-fun prefix_dt_names descr sorts str = 
-let
-  fun get_nth_name (i, _) = 
-    Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) 
-in
-  Datatype_Prop.indexify_names 
-    (map (prefix str o get_nth_name) descr)
-end
-*}
-
-
-ML {*
-(* permutation function for one argument 
-   
-    - in case the argument is recursive it returns 
-
-         permute_fn p arg
-
-    - in case the argument is non-recursive it will return
-
-         p o arg
-
-*)
-fun perm_arg permute_fn_frees p (arg_dty, arg) =
-  if Datatype_Aux.is_rec_type arg_dty 
-  then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg
-  else mk_perm p arg
-*}
-
-ML {*
-(* generates the equation for the permutation function for one constructor;
-   i is the index of the corresponding datatype *)
-fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) =
-let
-  val p = Free ("p", @{typ perm})
-  val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
-  val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
-  val args = map Free (arg_names ~~ arg_tys)
-  val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
-  val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args)
-  val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args))
-  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-in
-  (Attrib.empty_binding, eq)
-end
-*}
-
-ML {*
-(* proves the two pt-type class properties *)
-fun prove_permute_zero lthy induct perm_defs perm_fns =
-let
-  val perm_types = map (body_type o fastype_of) perm_fns
-  val perm_indnames = Datatype_Prop.make_tnames perm_types
-  
-  fun single_goal ((perm_fn, T), x) =
-    HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
-
-  val goals =
-    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-  val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
-
-  val tac = (Datatype_Aux.indtac induct perm_indnames 
-             THEN_ALL_NEW asm_simp_tac simps) 1
-in
-  Goal.prove lthy perm_indnames [] goals (K tac)
-  |> Datatype_Aux.split_conj_thm
-end
-*}
-
-ML {*
-fun prove_permute_plus lthy induct perm_defs perm_fns =
-let
-  val p = Free ("p", @{typ perm})
-  val q = Free ("q", @{typ perm})
-  val perm_types = map (body_type o fastype_of) perm_fns
-  val perm_indnames = Datatype_Prop.make_tnames perm_types
-  
-  fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 
-      (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
-
-  val goals =
-    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
-
-  val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
-
-  val tac = (Datatype_Aux.indtac induct perm_indnames
-             THEN_ALL_NEW asm_simp_tac simps) 1
-in
-  Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
-  |> Datatype_Aux.split_conj_thm 
-end
-*}
-
-ML {*
-(* defines the permutation functions for raw datatypes and
-   proves that they are instances of pt
-
-   user_dt_nos refers to the number of "un-unfolded" datatypes
-   given by the user
-*)
-fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
-let
-  val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
-  val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
-
-  val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
-  val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
-  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
-
-  fun perm_eq (i, (_, _, constrs)) = 
-    map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;
-
-  val perm_eqs = maps perm_eq dt_descr;
-
-  val lthy =
-    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
-   
-  val ((perm_funs, perm_eq_thms), lthy') =
-    Primrec.add_primrec
-      (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
-    
-  val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
-  val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
-  val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
-  val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
-  val perms_name = space_implode "_" perm_fn_names
-  val perms_zero_bind = Binding.name (perms_name ^ "_zero")
-  val perms_plus_bind = Binding.name (perms_name ^ "_plus")
-  
-  fun tac _ (_, _, simps) =
-    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
-  
-  fun morphism phi (fvs, dfs, simps) =
-    (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);
-in
-  lthy'
-  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
-  |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
-  |> Class_Target.prove_instantiation_exit_result morphism tac 
-       (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')
-end
-*}
-
-
-
-
 
 (* permutations for quotient types *)