src/HOL/Nominal/nominal_atoms.ML
changeset 21289 920b7b893d9c
parent 20377 3baf326b2b5f
child 21377 c29146dc14f1
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Nov 10 10:42:28 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Nov 10 19:04:18 2006 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4      (* produces a list consisting of pairs:         *)
     1.5      (*  fst component is the atom-kind name         *)
     1.6      (*  snd component is its type                   *)
     1.7 -    val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names;
     1.8 +    val full_ak_names = map (Sign.intern_type thy1) ak_names;
     1.9      val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names;
    1.10       
    1.11      (* adds for every atom-kind an axiom             *)
    1.12 @@ -76,7 +76,7 @@
    1.13      val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy =>
    1.14        let
    1.15          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    1.16 -        val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name);
    1.17 +        val swap_name = Sign.full_name thy ("swap_" ^ ak_name);
    1.18          val a = Free ("a", T);
    1.19          val b = Free ("b", T);
    1.20          val c = Free ("c", T);
    1.21 @@ -105,10 +105,10 @@
    1.22      val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy =>
    1.23        let
    1.24          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    1.25 -        val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name)
    1.26 +        val swap_name = Sign.full_name thy ("swap_" ^ ak_name)
    1.27          val prmT = mk_permT T --> T --> T;
    1.28          val prm_name = ak_name ^ "_prm_" ^ ak_name;
    1.29 -        val qu_prm_name = Sign.full_name (sign_of thy) prm_name;
    1.30 +        val qu_prm_name = Sign.full_name thy prm_name;
    1.31          val x  = Free ("x", HOLogic.mk_prodT (T, T));
    1.32          val xs = Free ("xs", mk_permT T);
    1.33          val a  = Free ("a", T) ;
    1.34 @@ -141,7 +141,7 @@
    1.35            val pi = Free ("pi", mk_permT T);
    1.36            val a  = Free ("a", T');
    1.37            val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
    1.38 -          val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
    1.39 +          val cperm_def = Const (Sign.full_name thy' perm_def_name, mk_permT T --> T' --> T');
    1.40  
    1.41            val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
    1.42            val def = Logic.mk_equals
    1.43 @@ -156,7 +156,7 @@
    1.44      val (prm_cons_thms,thy6) = 
    1.45        thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
    1.46        let
    1.47 -        val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
    1.48 +        val ak_name_qu = Sign.full_name thy5 (ak_name);
    1.49          val i_type = Type(ak_name_qu,[]);
    1.50  	val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
    1.51          val at_type = Logic.mk_type i_type;
    1.52 @@ -217,8 +217,8 @@
    1.53      val (prm_inst_thms,thy8) = 
    1.54        thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
    1.55        let
    1.56 -        val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name);
    1.57 -        val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
    1.58 +        val ak_name_qu = Sign.full_name thy7 ak_name;
    1.59 +        val pt_name_qu = Sign.full_name thy7 ("pt_"^ak_name);
    1.60          val i_type1 = TFree("'x",[pt_name_qu]);
    1.61          val i_type2 = Type(ak_name_qu,[]);
    1.62  	val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.63 @@ -244,7 +244,7 @@
    1.64       val (fs_ax_classes,thy11) =  fold_map (fn (ak_name, T) => fn thy =>
    1.65         let 
    1.66  	  val cl_name = "fs_"^ak_name;
    1.67 -	  val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
    1.68 +	  val pt_name = Sign.full_name thy ("pt_"^ak_name);
    1.69            val ty = TFree("'a",["HOL.type"]);
    1.70            val x   = Free ("x", ty);
    1.71            val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
    1.72 @@ -263,8 +263,8 @@
    1.73       val (fs_inst_thms,thy12) = 
    1.74         thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
    1.75         let
    1.76 -         val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name);
    1.77 -         val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
    1.78 +         val ak_name_qu = Sign.full_name thy11 ak_name;
    1.79 +         val fs_name_qu = Sign.full_name thy11 ("fs_"^ak_name);
    1.80           val i_type1 = TFree("'x",[fs_name_qu]);
    1.81           val i_type2 = Type(ak_name_qu,[]);
    1.82   	 val cfs = Const ("Nominal.fs", 
    1.83 @@ -311,9 +311,9 @@
    1.84          val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy =>
    1.85  	 fold_map (fn (ak_name', T') => fn thy' =>
    1.86             let
    1.87 -             val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
    1.88 -	     val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
    1.89 -             val cp_name_qu  = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
    1.90 +             val ak_name_qu  = Sign.full_name thy' (ak_name);
    1.91 +	     val ak_name_qu' = Sign.full_name thy' (ak_name');
    1.92 +             val cp_name_qu  = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
    1.93               val i_type0 = TFree("'a",[cp_name_qu]);
    1.94               val i_type1 = Type(ak_name_qu,[]);
    1.95               val i_type2 = Type(ak_name_qu',[]);
    1.96 @@ -344,8 +344,8 @@
    1.97            (if not (ak_name = ak_name') 
    1.98             then 
    1.99  	       let
   1.100 -		 val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
   1.101 -	         val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
   1.102 +		 val ak_name_qu  = Sign.full_name thy' ak_name;
   1.103 +	         val ak_name_qu' = Sign.full_name thy' ak_name';
   1.104                   val i_type1 = Type(ak_name_qu,[]);
   1.105                   val i_type2 = Type(ak_name_qu',[]);
   1.106  	         val cdj = Const ("Nominal.disjoint",
   1.107 @@ -390,8 +390,8 @@
   1.108       val thy13 = fold (fn ak_name => fn thy =>
   1.109  	fold (fn ak_name' => fn thy' =>
   1.110           let
   1.111 -           val qu_name =  Sign.full_name (sign_of thy') ak_name';
   1.112 -           val cls_name = Sign.full_name (sign_of thy') ("pt_"^ak_name);
   1.113 +           val qu_name =  Sign.full_name thy' ak_name';
   1.114 +           val cls_name = Sign.full_name thy' ("pt_"^ak_name);
   1.115             val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); 
   1.116  
   1.117             val proof1 = EVERY [ClassPackage.intro_classes_tac [],
   1.118 @@ -421,7 +421,7 @@
   1.119       (* are instances of pt_<ak>        *)
   1.120       val thy18 = fold (fn ak_name => fn thy =>
   1.121         let
   1.122 -          val cls_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   1.123 +          val cls_name = Sign.full_name thy ("pt_"^ak_name);
   1.124            val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
   1.125            val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   1.126  
   1.127 @@ -467,8 +467,8 @@
   1.128         val thy20 = fold (fn ak_name => fn thy =>
   1.129          fold (fn ak_name' => fn thy' =>
   1.130          let
   1.131 -           val qu_name =  Sign.full_name (sign_of thy') ak_name';
   1.132 -           val qu_class = Sign.full_name (sign_of thy') ("fs_"^ak_name);
   1.133 +           val qu_name =  Sign.full_name thy' ak_name';
   1.134 +           val qu_class = Sign.full_name thy' ("fs_"^ak_name);
   1.135             val proof =
   1.136                 (if ak_name = ak_name'
   1.137                  then
   1.138 @@ -493,7 +493,7 @@
   1.139  
   1.140         val thy24 = fold (fn ak_name => fn thy => 
   1.141          let
   1.142 -          val cls_name = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   1.143 +          val cls_name = Sign.full_name thy ("fs_"^ak_name);
   1.144            val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
   1.145            fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];
   1.146  
   1.147 @@ -533,8 +533,8 @@
   1.148           fold (fn ak_name' => fn thy' =>
   1.149            fold (fn ak_name'' => fn thy'' =>
   1.150              let
   1.151 -              val name =  Sign.full_name (sign_of thy'') ak_name;
   1.152 -              val cls_name = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');
   1.153 +              val name =  Sign.full_name thy'' ak_name;
   1.154 +              val cls_name = Sign.full_name thy'' ("cp_"^ak_name'^"_"^ak_name'');
   1.155                val proof =
   1.156                  (if (ak_name'=ak_name'') then 
   1.157                    (let
   1.158 @@ -570,7 +570,7 @@
   1.159         val thy26 = fold (fn ak_name => fn thy =>
   1.160  	fold (fn ak_name' => fn thy' =>
   1.161          let
   1.162 -            val cls_name = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   1.163 +            val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
   1.164              val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   1.165              val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
   1.166              val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
   1.167 @@ -602,7 +602,7 @@
   1.168  	  fun discrete_pt_inst discrete_ty defn =
   1.169  	     fold (fn ak_name => fn thy =>
   1.170  	     let
   1.171 -	       val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   1.172 +	       val qu_class = Sign.full_name thy ("pt_"^ak_name);
   1.173  	       val simp_s = HOL_basic_ss addsimps [defn];
   1.174                 val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
   1.175               in 
   1.176 @@ -612,7 +612,7 @@
   1.177            fun discrete_fs_inst discrete_ty defn = 
   1.178  	     fold (fn ak_name => fn thy =>
   1.179  	     let
   1.180 -	       val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   1.181 +	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
   1.182  	       val supp_def = thm "Nominal.supp_def";
   1.183                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
   1.184                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.185 @@ -623,7 +623,7 @@
   1.186            fun discrete_cp_inst discrete_ty defn = 
   1.187  	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
   1.188  	     let
   1.189 -	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
   1.190 +	       val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
   1.191  	       val supp_def = thm "Nominal.supp_def";
   1.192                 val simp_s = HOL_ss addsimps [defn];
   1.193                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];