--- a/Nominal/Perm.thy	Tue Apr 20 09:13:52 2010 +0200
+++ b/Nominal/Perm.thy	Tue Apr 20 11:29:00 2010 +0200
@@ -2,56 +2,11 @@
 imports "../Nominal-General/Nominal2_Atoms"
 begin
 
+(* definitions of the permute function for raw nominal datatypes *)
 
 
 ML {*
-fun prove_perm_zero 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);
-  fun glc ((perm, T), x) =
-    HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T))
-  val gl =
-    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
-  fun tac _ =
-    EVERY [
-      Datatype_Aux.indtac induct perm_indnames 1,
-      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
-    ];
-in
-  Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
-end;
-*}
-
-ML {*
-fun prove_perm_plus lthy induct perm_def perm_frees =
-let
-  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);
-  fun glc ((perm, T), x) =
-    HOLogic.mk_eq (
-      perm $ (mk_plus pi1 pi2) $ Free (x, T),
-      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
-  val goal =
-    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
-  fun tac _ =
-    EVERY [
-      Datatype_Aux.indtac induct perm_indnames 1,
-      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
-    ]
-in
-  Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac)
-end;
-*}
-
-
-(* definitions of the permute function for a raw nominal datatype *)
-
-ML {*
+(* returns the type of the nth datatype *)
 fun nth_dtyp dt_descr sorts i = 
   Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i);
 *}
@@ -93,8 +48,59 @@
 *}
 
 ML {*
+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 pi1 = Free ("p", @{typ perm})
+  val pi2 = 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, T), x) = HOLogic.mk_eq 
+      (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ 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
+
+   dt_nos refers to the number of "un-unfolded" datatypes
+   given by the user
 *)
 fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =
 let
@@ -117,12 +123,12 @@
   val lthy =
     Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
    
-  val ((perm_frees, perm_ldef), lthy') =
+  val ((perm_fns, perm_ldef), lthy') =
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  val perm_zero_thms = prove_perm_zero lthy' induct perm_ldef perm_frees
-  val perm_plus_thms = prove_perm_plus lthy' induct perm_ldef perm_frees
+  val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns
+  val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
   val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
   val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
   val perms_name = space_implode "_" perm_fn_names
@@ -130,42 +136,20 @@
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")
   
   fun tac _ (_, simps, _) =
-    (Class.intro_classes_tac []) THEN ALLGOALS (resolve_tac simps);
+    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
   
   fun morphism phi (dfs, simps, fvs) =
     (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
-  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_ldef, perm_zero_thms' @ perm_plus_thms', perm_frees)
-  end
-*}
-
-(* Test *)
-(*atom_decl name
-
-datatype trm =
-  Var "name"
-| App "trm" "trm list"
-| Lam "name" "trm"
-| Let "bp" "trm" "trm"
-and bp =
-  BUnit
-| BVar "name"
-| BPair "bp" "bp"
-
-setup {* fn thy =>
-let 
-  val info = Datatype.the_info thy "Perm.trm"
 in
-  define_raw_perms info 2 thy |> snd
+  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_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns)
 end
 *}
 
-print_theorems
-*)
+(* permutations for quotient types *)
 
 ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
@@ -228,11 +212,12 @@
 
 
 (* Test *)
-(*atom_decl name
+(*
+atom_decl name
 
 datatype trm =
   Var "name"
-| App "trm" "trm list"
+| App "trm" "(trm list) list"
 | Lam "name" "trm"
 | Let "bp" "trm" "trm"
 and bp =
@@ -242,9 +227,9 @@
 
 setup {* fn thy =>
 let 
-  val inf = Datatype.the_info thy "Perm.trm"
+  val info = Datatype.the_info thy "Perm.trm"
 in
-  define_raw_perms inf 2 thy |> snd
+  define_raw_perms info 2 thy |> snd
 end
 *}