diff -r 486d4647bb37 -r 8f8652a8107f Nominal/nominal_dt_rawperm.ML
--- a/Nominal/nominal_dt_rawperm.ML	Fri Sep 10 09:17:40 2010 +0800
+++ b/Nominal/nominal_dt_rawperm.ML	Sat Sep 11 05:56:49 2010 +0800
@@ -21,109 +21,109 @@
 (** proves the two pt-type class properties **)
 
 fun prove_permute_zero induct perm_defs perm_fns lthy =
-let
-  val perm_types = map (body_type o fastype_of) perm_fns
-  val perm_indnames = Datatype_Prop.make_tnames perm_types
+  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))
+    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 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 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
+    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
 
 
 fun prove_permute_plus induct perm_defs perm_fns lthy =
-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
+  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 
+    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 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 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
+    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
 
 
 fun mk_perm_eq ty_perm_assoc cnstr = 
-let
-  fun lookup_perm p (ty, arg) = 
-    case (AList.lookup (op=) ty_perm_assoc ty) of
-      SOME perm => perm $ p $ arg
-    | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
+  let
+    fun lookup_perm p (ty, arg) = 
+      case (AList.lookup (op=) ty_perm_assoc ty) of
+        SOME perm => perm $ p $ arg
+      | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg
 
-  val p = Free ("p", @{typ perm})
-  val (arg_tys, ty) =
-    fastype_of cnstr
-    |> strip_type
+    val p = Free ("p", @{typ perm})
+    val (arg_tys, ty) =
+      fastype_of cnstr
+      |> strip_type
 
-  val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
-  val args = map Free (arg_names ~~ arg_tys)
+    val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
+    val args = map Free (arg_names ~~ arg_tys)
 
-  val lhs = lookup_perm p (ty, list_comb (cnstr, args))
-  val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
+    val lhs = lookup_perm p (ty, list_comb (cnstr, args))
+    val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args))
   
-  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))  
-in
-  (Attrib.empty_binding, eq)
-end
+    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))  
+  in
+    (Attrib.empty_binding, eq)
+  end
 
 
 fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy =
-let
-  val perm_fn_names = full_ty_names
-    |> map Long_Name.base_name
-    |> map (prefix "permute_")
+  let
+    val perm_fn_names = full_ty_names
+      |> map Long_Name.base_name
+      |> map (prefix "permute_")
 
-  val perm_fn_types = map perm_ty tys
-  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
-  val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
+    val perm_fn_types = map perm_ty tys
+    val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
+    val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names
 
-  val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
+    val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs
 
-  fun tac _ (_, _, simps) =
-    Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
+    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);
+    fun morphism phi (fvs, dfs, simps) =
+      (map (Morphism.term phi) fvs, 
+       map (Morphism.thm phi) dfs, 
+       map (Morphism.thm phi) simps);
 
-  val ((perm_funs, perm_eq_thms), lthy') =
-    lthy
-    |> Local_Theory.exit_global
-    |> Class.instantiation (full_ty_names, tvs, @{sort pt}) 
-    |> Primrec.add_primrec perm_fn_binds perm_eqs
+    val ((perm_funs, perm_eq_thms), lthy') =
+      lthy
+      |> Local_Theory.exit_global
+      |> Class.instantiation (full_ty_names, tvs, @{sort pt}) 
+      |> Primrec.add_primrec perm_fn_binds perm_eqs
     
-  val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
-  val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' 
-in
-  lthy'
-  |> Class.prove_instantiation_exit_result morphism tac 
-       (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
-  ||> Named_Target.theory_init
-end
+    val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy'
+    val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy'  
+  in
+    lthy'
+    |> Class.prove_instantiation_exit_result morphism tac 
+         (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms)
+    ||> Named_Target.theory_init
+  end
 
 
 end (* structure *)