src/HOL/Nominal/nominal_atoms.ML
changeset 19494 2e909d5309f4
parent 19488 8bd2c840458e
child 19509 351e1b1ea251
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 28 15:53:47 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 28 15:54:34 2006 +0200
     1.3 @@ -1,4 +1,9 @@
     1.4 -(* $Id$ *)
     1.5 +(*  Title:      HOL/Nominal/nominal_atoms.ML
     1.6 +    ID:         $Id$
     1.7 +    Author:     Christian Urban and Stefan Berghofer, TU Muenchen
     1.8 +
     1.9 +Declaration of atom types to be used in nominal datatypes.
    1.10 +*)
    1.11  
    1.12  signature NOMINAL_ATOMS =
    1.13  sig
    1.14 @@ -80,7 +85,7 @@
    1.15          val ab = Free ("ab", HOLogic.mk_prodT (T, T))
    1.16          val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
    1.17          val cswap_akname = Const (swap_name, swapT);
    1.18 -        val cswap = Const ("nominal.swap", swapT)
    1.19 +        val cswap = Const ("Nominal.swap", swapT)
    1.20  
    1.21          val name = "swap_"^ak_name^"_def";
    1.22          val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.23 @@ -136,7 +141,7 @@
    1.24            val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
    1.25            val pi = Free ("pi", mk_permT T);
    1.26            val a  = Free ("a", T');
    1.27 -          val cperm = Const ("nominal.perm", mk_permT T --> T' --> T');
    1.28 +          val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
    1.29            val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
    1.30  
    1.31            val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
    1.32 @@ -154,7 +159,7 @@
    1.33        let
    1.34          val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
    1.35          val i_type = Type(ak_name_qu,[]);
    1.36 -	val cat = Const ("nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
    1.37 +	val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
    1.38          val at_type = Logic.mk_type i_type;
    1.39          val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5
    1.40                                    [Name "at_def",
    1.41 @@ -185,10 +190,10 @@
    1.42            val x   = Free ("x", ty);
    1.43            val pi1 = Free ("pi1", mk_permT T);
    1.44            val pi2 = Free ("pi2", mk_permT T);
    1.45 -          val cperm = Const ("nominal.perm", mk_permT T --> ty --> ty);
    1.46 +          val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
    1.47            val cnil  = Const ("List.list.Nil", mk_permT T);
    1.48            val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
    1.49 -          val cprm_eq = Const ("nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
    1.50 +          val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
    1.51            (* nil axiom *)
    1.52            val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
    1.53                         (cperm $ cnil $ x, x));
    1.54 @@ -217,7 +222,7 @@
    1.55          val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
    1.56          val i_type1 = TFree("'x",[pt_name_qu]);
    1.57          val i_type2 = Type(ak_name_qu,[]);
    1.58 -	val cpt = Const ("nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.59 +	val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.60          val pt_type = Logic.mk_type i_type1;
    1.61          val at_type = Logic.mk_type i_type2;
    1.62          val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy7
    1.63 @@ -243,7 +248,7 @@
    1.64  	  val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
    1.65            val ty = TFree("'a",["HOL.type"]);
    1.66            val x   = Free ("x", ty);
    1.67 -          val csupp    = Const ("nominal.supp", ty --> HOLogic.mk_setT T);
    1.68 +          val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
    1.69            val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
    1.70            
    1.71            val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
    1.72 @@ -263,7 +268,7 @@
    1.73           val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
    1.74           val i_type1 = TFree("'x",[fs_name_qu]);
    1.75           val i_type2 = Type(ak_name_qu,[]);
    1.76 - 	 val cfs = Const ("nominal.fs", 
    1.77 + 	 val cfs = Const ("Nominal.fs", 
    1.78                                   (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.79           val fs_type = Logic.mk_type i_type1;
    1.80           val at_type = Logic.mk_type i_type2;
    1.81 @@ -290,9 +295,9 @@
    1.82                 val x   = Free ("x", ty);
    1.83                 val pi1 = Free ("pi1", mk_permT T);
    1.84  	       val pi2 = Free ("pi2", mk_permT T');                  
    1.85 -	       val cperm1 = Const ("nominal.perm", mk_permT T  --> ty --> ty);
    1.86 -               val cperm2 = Const ("nominal.perm", mk_permT T' --> ty --> ty);
    1.87 -               val cperm3 = Const ("nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
    1.88 +	       val cperm1 = Const ("Nominal.perm", mk_permT T  --> ty --> ty);
    1.89 +               val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty);
    1.90 +               val cperm3 = Const ("Nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
    1.91  
    1.92                 val ax1   = HOLogic.mk_Trueprop 
    1.93  			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    1.94 @@ -313,7 +318,7 @@
    1.95               val i_type0 = TFree("'a",[cp_name_qu]);
    1.96               val i_type1 = Type(ak_name_qu,[]);
    1.97               val i_type2 = Type(ak_name_qu',[]);
    1.98 -	     val ccp = Const ("nominal.cp",
    1.99 +	     val ccp = Const ("Nominal.cp",
   1.100                               (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
   1.101                                                        (Term.itselfT i_type2)-->HOLogic.boolT);
   1.102               val at_type  = Logic.mk_type i_type1;
   1.103 @@ -344,7 +349,7 @@
   1.104  	         val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
   1.105                   val i_type1 = Type(ak_name_qu,[]);
   1.106                   val i_type2 = Type(ak_name_qu',[]);
   1.107 -	         val cdj = Const ("nominal.disjoint",
   1.108 +	         val cdj = Const ("Nominal.disjoint",
   1.109                             (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   1.110                   val at_type  = Logic.mk_type i_type1;
   1.111                   val at_type' = Logic.mk_type i_type2;
   1.112 @@ -436,11 +441,11 @@
   1.113         in 
   1.114  	thy
   1.115  	|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
   1.116 -        |> AxClass.prove_arity ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   1.117 +        |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   1.118          |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
   1.119          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   1.120          |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   1.121 -        |> AxClass.prove_arity ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   1.122 +        |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   1.123                                      (pt_proof pt_thm_nprod)
   1.124          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
   1.125          |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
   1.126 @@ -502,7 +507,7 @@
   1.127           thy 
   1.128           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
   1.129           |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   1.130 -         |> AxClass.prove_arity ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   1.131 +         |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   1.132                                       (fs_proof fs_thm_nprod) 
   1.133           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   1.134           |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   1.135 @@ -586,7 +591,7 @@
   1.136           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   1.137           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   1.138           |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   1.139 -         |> AxClass.prove_arity ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   1.140 +         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   1.141          end) ak_names thy) ak_names thy25;
   1.142         
   1.143       (* show that discrete nominal types are permutation types, finitely     *) 
   1.144 @@ -609,7 +614,7 @@
   1.145  	     fold (fn ak_name => fn thy =>
   1.146  	     let
   1.147  	       val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   1.148 -	       val supp_def = thm "nominal.supp_def";
   1.149 +	       val supp_def = thm "Nominal.supp_def";
   1.150                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
   1.151                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.152               in  
   1.153 @@ -620,7 +625,7 @@
   1.154  	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
   1.155  	     let
   1.156  	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
   1.157 -	       val supp_def = thm "nominal.supp_def";
   1.158 +	       val supp_def = thm "Nominal.supp_def";
   1.159                 val simp_s = HOL_ss addsimps [defn];
   1.160                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.161               in  
   1.162 @@ -646,32 +651,32 @@
   1.163  
   1.164         (* abbreviations for some lemmas *)
   1.165         (*===============================*)
   1.166 -       val abs_fun_pi          = thm "nominal.abs_fun_pi";
   1.167 -       val abs_fun_pi_ineq     = thm "nominal.abs_fun_pi_ineq";
   1.168 -       val abs_fun_eq          = thm "nominal.abs_fun_eq";
   1.169 -       val dj_perm_forget      = thm "nominal.dj_perm_forget";
   1.170 -       val dj_pp_forget        = thm "nominal.dj_perm_perm_forget";
   1.171 -       val fresh_iff           = thm "nominal.fresh_abs_fun_iff";
   1.172 -       val fresh_iff_ineq      = thm "nominal.fresh_abs_fun_iff_ineq";
   1.173 -       val abs_fun_supp        = thm "nominal.abs_fun_supp";
   1.174 -       val abs_fun_supp_ineq   = thm "nominal.abs_fun_supp_ineq";
   1.175 -       val pt_swap_bij         = thm "nominal.pt_swap_bij";
   1.176 -       val pt_fresh_fresh      = thm "nominal.pt_fresh_fresh";
   1.177 -       val pt_bij              = thm "nominal.pt_bij";
   1.178 -       val pt_perm_compose     = thm "nominal.pt_perm_compose";
   1.179 -       val pt_perm_compose'    = thm "nominal.pt_perm_compose'";
   1.180 -       val perm_app            = thm "nominal.pt_fun_app_eq";
   1.181 -       val at_fresh            = thm "nominal.at_fresh";
   1.182 -       val at_calc             = thms "nominal.at_calc";
   1.183 -       val at_supp             = thm "nominal.at_supp";
   1.184 -       val dj_supp             = thm "nominal.dj_supp";
   1.185 -       val fresh_left_ineq     = thm "nominal.pt_fresh_left_ineq";
   1.186 -       val fresh_left          = thm "nominal.pt_fresh_left";
   1.187 -       val fresh_bij_ineq      = thm "nominal.pt_fresh_bij_ineq";
   1.188 -       val fresh_bij           = thm "nominal.pt_fresh_bij";
   1.189 -       val pt_pi_rev           = thm "nominal.pt_pi_rev";
   1.190 -       val pt_rev_pi           = thm "nominal.pt_rev_pi";
   1.191 -       val fresh_fun_eqvt      = thm "nominal.fresh_fun_equiv";
   1.192 +       val abs_fun_pi          = thm "Nominal.abs_fun_pi";
   1.193 +       val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
   1.194 +       val abs_fun_eq          = thm "Nominal.abs_fun_eq";
   1.195 +       val dj_perm_forget      = thm "Nominal.dj_perm_forget";
   1.196 +       val dj_pp_forget        = thm "Nominal.dj_perm_perm_forget";
   1.197 +       val fresh_iff           = thm "Nominal.fresh_abs_fun_iff";
   1.198 +       val fresh_iff_ineq      = thm "Nominal.fresh_abs_fun_iff_ineq";
   1.199 +       val abs_fun_supp        = thm "Nominal.abs_fun_supp";
   1.200 +       val abs_fun_supp_ineq   = thm "Nominal.abs_fun_supp_ineq";
   1.201 +       val pt_swap_bij         = thm "Nominal.pt_swap_bij";
   1.202 +       val pt_fresh_fresh      = thm "Nominal.pt_fresh_fresh";
   1.203 +       val pt_bij              = thm "Nominal.pt_bij";
   1.204 +       val pt_perm_compose     = thm "Nominal.pt_perm_compose";
   1.205 +       val pt_perm_compose'    = thm "Nominal.pt_perm_compose'";
   1.206 +       val perm_app            = thm "Nominal.pt_fun_app_eq";
   1.207 +       val at_fresh            = thm "Nominal.at_fresh";
   1.208 +       val at_calc             = thms "Nominal.at_calc";
   1.209 +       val at_supp             = thm "Nominal.at_supp";
   1.210 +       val dj_supp             = thm "Nominal.dj_supp";
   1.211 +       val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
   1.212 +       val fresh_left          = thm "Nominal.pt_fresh_left";
   1.213 +       val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
   1.214 +       val fresh_bij           = thm "Nominal.pt_fresh_bij";
   1.215 +       val pt_pi_rev           = thm "Nominal.pt_pi_rev";
   1.216 +       val pt_rev_pi           = thm "Nominal.pt_rev_pi";
   1.217 +       val fresh_fun_eqvt      = thm "Nominal.fresh_fun_equiv";
   1.218  
   1.219         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
   1.220         (* types; this allows for example to use abs_perm (which is a      *)