# HG changeset patch
# User urbanc
# Date 1133803189 -3600
# Node ID e53a5075953eb7f694bd671b0450822f87ab128d
# Parent  715d6df89fccd414c12dc79c1397d88d6b0adb26
added code to say that discrete types (nat, bool, char)
are instances of cp_*_*.

diff -r 715d6df89fcc -r e53a5075953e src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Dec 05 17:02:20 2005 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Dec 05 18:19:49 2005 +0100
@@ -556,17 +556,32 @@
              in  
 	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
              end) ak_names;  
+
+          fun discrete_cp_inst discrete_ty defn = 
+	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
+	     let
+	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
+	       val supp_def = thm "nominal.supp_def";
+               val simp_s = HOL_ss addsimps [defn];
+               val proof = EVERY [AxClass.intro_classes_tac [], asm_simp_tac simp_s 1];      
+             in  
+	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
+             end) ak_names)) ak_names;  
           
         in
          thy19a
          |> discrete_pt_inst "nat"  (thm "perm_nat_def")
-         |> discrete_fs_inst "nat"  (thm "perm_nat_def")
+         |> discrete_fs_inst "nat"  (thm "perm_nat_def") 
+         |> discrete_cp_inst "nat"  (thm "perm_nat_def") 
          |> discrete_pt_inst "bool" (thm "perm_bool")
          |> discrete_fs_inst "bool" (thm "perm_bool")
+         |> discrete_cp_inst "bool" (thm "perm_bool")
          |> discrete_pt_inst "IntDef.int" (thm "perm_int_def")
-         |> discrete_fs_inst "IntDef.int" (thm "perm_int_def")
+         |> discrete_fs_inst "IntDef.int" (thm "perm_int_def") 
+         |> discrete_cp_inst "IntDef.int" (thm "perm_int_def") 
          |> discrete_pt_inst "List.char" (thm "perm_char_def")
          |> discrete_fs_inst "List.char" (thm "perm_char_def")
+         |> discrete_cp_inst "List.char" (thm "perm_char_def")
         end;