src/HOL/Nominal/nominal_atoms.ML
changeset 23894 1a4167d761ac
parent 23158 749b6870b1a1
child 24162 8dfd5dd65d82
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 21 17:40:40 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 21 23:25:00 2007 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4  structure NominalAtoms : NOMINAL_ATOMS =
     1.5  struct
     1.6  
     1.7 -val finite_emptyI = thm "finite.emptyI";
     1.8 -val Collect_const = thm "Collect_const";
     1.9 +val finite_emptyI = @{thm "finite.emptyI"};
    1.10 +val Collect_const = @{thm "Collect_const"};
    1.11  
    1.12  
    1.13  (* theory data *)
    1.14 @@ -60,6 +60,8 @@
    1.15  (* atom_decl <ak1> ... <akn>                           *)
    1.16  fun create_nom_typedecls ak_names thy =
    1.17    let
    1.18 +    val cla_s = claset_of thy;
    1.19 +
    1.20      (* declares a type-decl for every atom-kind: *) 
    1.21      (* that is typedecl <ak>                     *)
    1.22      val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
    1.23 @@ -184,7 +186,7 @@
    1.24  	val name = "at_"^ak_name^ "_inst";
    1.25          val statement = HOLogic.mk_Trueprop (cat $ at_type);
    1.26  
    1.27 -        val proof = fn _ => auto_tac (claset(),simp_s);
    1.28 +        val proof = fn _ => auto_tac (cla_s,simp_s);
    1.29  
    1.30        in 
    1.31          ((name, Goal.prove_global thy5 [] [] statement proof), []) 
    1.32 @@ -246,7 +248,7 @@
    1.33  	val name = "pt_"^ak_name^ "_inst";
    1.34          val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);
    1.35  
    1.36 -        val proof = fn _ => auto_tac (claset(),simp_s);
    1.37 +        val proof = fn _ => auto_tac (cla_s,simp_s);
    1.38        in 
    1.39          ((name, Goal.prove_global thy7 [] [] statement proof), []) 
    1.40        end) ak_names_types);
    1.41 @@ -291,7 +293,7 @@
    1.42  	 val name = "fs_"^ak_name^ "_inst";
    1.43           val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);
    1.44  
    1.45 -         val proof = fn _ => auto_tac (claset(),simp_s);
    1.46 +         val proof = fn _ => auto_tac (cla_s,simp_s);
    1.47         in 
    1.48           ((name, Goal.prove_global thy11 [] [] statement proof), []) 
    1.49         end) ak_names_types);
    1.50 @@ -342,7 +344,7 @@
    1.51  	     val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
    1.52               val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
    1.53  
    1.54 -             val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];
    1.55 +             val proof = fn _ => EVERY [auto_tac (cla_s,simp_s), rtac cp1 1];
    1.56  	   in
    1.57  	     PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    1.58  	   end) 
    1.59 @@ -373,7 +375,7 @@
    1.60  	         val name = "dj_"^ak_name^"_"^ak_name';
    1.61                   val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
    1.62  
    1.63 -                 val proof = fn _ => auto_tac (claset(),simp_s);
    1.64 +                 val proof = fn _ => auto_tac (cla_s,simp_s);
    1.65  	       in
    1.66  		PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    1.67  	       end
    1.68 @@ -384,18 +386,18 @@
    1.69       (********  pt_<ak> class instances  ********)
    1.70       (*=========================================*)
    1.71       (* some abbreviations for theorems *)
    1.72 -      val pt1           = thm "pt1";
    1.73 -      val pt2           = thm "pt2";
    1.74 -      val pt3           = thm "pt3";
    1.75 -      val at_pt_inst    = thm "at_pt_inst";
    1.76 -      val pt_set_inst   = thm "pt_set_inst"; 
    1.77 -      val pt_unit_inst  = thm "pt_unit_inst";
    1.78 -      val pt_prod_inst  = thm "pt_prod_inst"; 
    1.79 -      val pt_nprod_inst = thm "pt_nprod_inst"; 
    1.80 -      val pt_list_inst  = thm "pt_list_inst";   
    1.81 -      val pt_optn_inst  = thm "pt_option_inst";   
    1.82 -      val pt_noptn_inst = thm "pt_noption_inst";   
    1.83 -      val pt_fun_inst   = thm "pt_fun_inst";     
    1.84 +      val pt1           = @{thm "pt1"};
    1.85 +      val pt2           = @{thm "pt2"};
    1.86 +      val pt3           = @{thm "pt3"};
    1.87 +      val at_pt_inst    = @{thm "at_pt_inst"};
    1.88 +      val pt_set_inst   = @{thm "pt_set_inst"}; 
    1.89 +      val pt_unit_inst  = @{thm "pt_unit_inst"};
    1.90 +      val pt_prod_inst  = @{thm "pt_prod_inst"}; 
    1.91 +      val pt_nprod_inst = @{thm "pt_nprod_inst"}; 
    1.92 +      val pt_list_inst  = @{thm "pt_list_inst"};
    1.93 +      val pt_optn_inst  = @{thm "pt_option_inst"};
    1.94 +      val pt_noptn_inst = @{thm "pt_noption_inst"};
    1.95 +      val pt_fun_inst   = @{thm "pt_fun_inst"};
    1.96  
    1.97       (* for all atom-kind combinations <ak>/<ak'> show that        *)
    1.98       (* every <ak> is an instance of pt_<ak'>; the proof for       *)
    1.99 @@ -466,14 +468,14 @@
   1.100         (********  fs_<ak> class instances  ********)
   1.101         (*=========================================*)
   1.102         (* abbreviations for some lemmas *)
   1.103 -       val fs1            = thm "fs1";
   1.104 -       val fs_at_inst     = thm "fs_at_inst";
   1.105 -       val fs_unit_inst   = thm "fs_unit_inst";
   1.106 -       val fs_prod_inst   = thm "fs_prod_inst";
   1.107 -       val fs_nprod_inst  = thm "fs_nprod_inst";
   1.108 -       val fs_list_inst   = thm "fs_list_inst";
   1.109 -       val fs_option_inst = thm "fs_option_inst";
   1.110 -       val dj_supp        = thm "dj_supp"
   1.111 +       val fs1            = @{thm "fs1"};
   1.112 +       val fs_at_inst     = @{thm "fs_at_inst"};
   1.113 +       val fs_unit_inst   = @{thm "fs_unit_inst"};
   1.114 +       val fs_prod_inst   = @{thm "fs_prod_inst"};
   1.115 +       val fs_nprod_inst  = @{thm "fs_nprod_inst"};
   1.116 +       val fs_list_inst   = @{thm "fs_list_inst"};
   1.117 +       val fs_option_inst = @{thm "fs_option_inst"};
   1.118 +       val dj_supp        = @{thm "dj_supp"};
   1.119  
   1.120         (* shows that <ak> is an instance of fs_<ak>     *)
   1.121         (* uses the theorem at_<ak>_inst                 *)
   1.122 @@ -528,18 +530,18 @@
   1.123         (********  cp_<ak>_<ai> class instances  ********)
   1.124         (*==============================================*)
   1.125         (* abbreviations for some lemmas *)
   1.126 -       val cp1             = thm "cp1";
   1.127 -       val cp_unit_inst    = thm "cp_unit_inst";
   1.128 -       val cp_bool_inst    = thm "cp_bool_inst";
   1.129 -       val cp_prod_inst    = thm "cp_prod_inst";
   1.130 -       val cp_list_inst    = thm "cp_list_inst";
   1.131 -       val cp_fun_inst     = thm "cp_fun_inst";
   1.132 -       val cp_option_inst  = thm "cp_option_inst";
   1.133 -       val cp_noption_inst = thm "cp_noption_inst";
   1.134 -       val cp_set_inst     = thm "cp_set_inst";
   1.135 -       val pt_perm_compose = thm "pt_perm_compose";
   1.136 +       val cp1             = @{thm "cp1"};
   1.137 +       val cp_unit_inst    = @{thm "cp_unit_inst"};
   1.138 +       val cp_bool_inst    = @{thm "cp_bool_inst"};
   1.139 +       val cp_prod_inst    = @{thm "cp_prod_inst"};
   1.140 +       val cp_list_inst    = @{thm "cp_list_inst"};
   1.141 +       val cp_fun_inst     = @{thm "cp_fun_inst"};
   1.142 +       val cp_option_inst  = @{thm "cp_option_inst"};
   1.143 +       val cp_noption_inst = @{thm "cp_noption_inst"};
   1.144 +       val cp_set_inst     = @{thm "cp_set_inst"};
   1.145 +       val pt_perm_compose = @{thm "pt_perm_compose"};
   1.146  
   1.147 -       val dj_pp_forget    = thm "dj_perm_perm_forget";
   1.148 +       val dj_pp_forget    = @{thm "dj_perm_perm_forget"};
   1.149  
   1.150         (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
   1.151         (* for every  <ak>/<ai>-combination                *)
   1.152 @@ -630,7 +632,7 @@
   1.153  	     fold (fn ak_name => fn thy =>
   1.154  	     let
   1.155  	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
   1.156 -	       val supp_def = thm "Nominal.supp_def";
   1.157 +	       val supp_def = @{thm "Nominal.supp_def"};
   1.158                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
   1.159                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.160               in 
   1.161 @@ -641,7 +643,7 @@
   1.162  	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
   1.163  	     let
   1.164  	       val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
   1.165 -	       val supp_def = thm "Nominal.supp_def";
   1.166 +	       val supp_def = @{thm "Nominal.supp_def"};
   1.167                 val simp_s = HOL_ss addsimps [defn];
   1.168                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.169               in
   1.170 @@ -650,70 +652,70 @@
   1.171  
   1.172          in
   1.173           thy26
   1.174 -         |> discrete_pt_inst "nat"  (thm "perm_nat_def")
   1.175 -         |> discrete_fs_inst "nat"  (thm "perm_nat_def") 
   1.176 -         |> discrete_cp_inst "nat"  (thm "perm_nat_def") 
   1.177 -         |> discrete_pt_inst "bool" (thm "perm_bool")
   1.178 -         |> discrete_fs_inst "bool" (thm "perm_bool")
   1.179 -         |> discrete_cp_inst "bool" (thm "perm_bool")
   1.180 -         |> discrete_pt_inst "IntDef.int" (thm "perm_int_def")
   1.181 -         |> discrete_fs_inst "IntDef.int" (thm "perm_int_def") 
   1.182 -         |> discrete_cp_inst "IntDef.int" (thm "perm_int_def") 
   1.183 -         |> discrete_pt_inst "List.char" (thm "perm_char_def")
   1.184 -         |> discrete_fs_inst "List.char" (thm "perm_char_def")
   1.185 -         |> discrete_cp_inst "List.char" (thm "perm_char_def")
   1.186 +         |> discrete_pt_inst "nat"  @{thm "perm_nat_def"}
   1.187 +         |> discrete_fs_inst "nat"  @{thm "perm_nat_def"}
   1.188 +         |> discrete_cp_inst "nat"  @{thm "perm_nat_def"}
   1.189 +         |> discrete_pt_inst "bool" @{thm "perm_bool"}
   1.190 +         |> discrete_fs_inst "bool" @{thm "perm_bool"}
   1.191 +         |> discrete_cp_inst "bool" @{thm "perm_bool"}
   1.192 +         |> discrete_pt_inst "IntDef.int" @{thm "perm_int_def"}
   1.193 +         |> discrete_fs_inst "IntDef.int" @{thm "perm_int_def"}
   1.194 +         |> discrete_cp_inst "IntDef.int" @{thm "perm_int_def"}
   1.195 +         |> discrete_pt_inst "List.char" @{thm "perm_char_def"}
   1.196 +         |> discrete_fs_inst "List.char" @{thm "perm_char_def"}
   1.197 +         |> discrete_cp_inst "List.char" @{thm "perm_char_def"}
   1.198          end;
   1.199  
   1.200  
   1.201         (* abbreviations for some lemmas *)
   1.202         (*===============================*)
   1.203 -       val abs_fun_pi          = thm "Nominal.abs_fun_pi";
   1.204 -       val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
   1.205 -       val abs_fun_eq          = thm "Nominal.abs_fun_eq";
   1.206 -       val abs_fun_eq'         = thm "Nominal.abs_fun_eq'";
   1.207 -       val abs_fun_fresh       = thm "Nominal.abs_fun_fresh";
   1.208 -       val abs_fun_fresh'      = thm "Nominal.abs_fun_fresh'";
   1.209 -       val dj_perm_forget      = thm "Nominal.dj_perm_forget";
   1.210 -       val dj_pp_forget        = thm "Nominal.dj_perm_perm_forget";
   1.211 -       val fresh_iff           = thm "Nominal.fresh_abs_fun_iff";
   1.212 -       val fresh_iff_ineq      = thm "Nominal.fresh_abs_fun_iff_ineq";
   1.213 -       val abs_fun_supp        = thm "Nominal.abs_fun_supp";
   1.214 -       val abs_fun_supp_ineq   = thm "Nominal.abs_fun_supp_ineq";
   1.215 -       val pt_swap_bij         = thm "Nominal.pt_swap_bij";
   1.216 -       val pt_swap_bij'        = thm "Nominal.pt_swap_bij'";
   1.217 -       val pt_fresh_fresh      = thm "Nominal.pt_fresh_fresh";
   1.218 -       val pt_bij              = thm "Nominal.pt_bij";
   1.219 -       val pt_perm_compose     = thm "Nominal.pt_perm_compose";
   1.220 -       val pt_perm_compose'    = thm "Nominal.pt_perm_compose'";
   1.221 -       val perm_app            = thm "Nominal.pt_fun_app_eq";
   1.222 -       val at_fresh            = thm "Nominal.at_fresh";
   1.223 -       val at_fresh_ineq       = thm "Nominal.at_fresh_ineq";
   1.224 -       val at_calc             = thms "Nominal.at_calc";
   1.225 -       val at_swap_simps       = thms "Nominal.at_swap_simps";
   1.226 -       val at_supp             = thm "Nominal.at_supp";
   1.227 -       val dj_supp             = thm "Nominal.dj_supp";
   1.228 -       val fresh_left_ineq     = thm "Nominal.pt_fresh_left_ineq";
   1.229 -       val fresh_left          = thm "Nominal.pt_fresh_left";
   1.230 -       val fresh_right_ineq    = thm "Nominal.pt_fresh_right_ineq";
   1.231 -       val fresh_right         = thm "Nominal.pt_fresh_right";
   1.232 -       val fresh_bij_ineq      = thm "Nominal.pt_fresh_bij_ineq";
   1.233 -       val fresh_bij           = thm "Nominal.pt_fresh_bij";
   1.234 -       val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
   1.235 -       val fresh_eqvt_ineq     = thm "Nominal.pt_fresh_eqvt_ineq";
   1.236 -       val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
   1.237 -       val in_eqvt             = thm "Nominal.pt_in_eqvt";
   1.238 -       val eq_eqvt             = thm "Nominal.pt_eq_eqvt";
   1.239 -       val all_eqvt            = thm "Nominal.pt_all_eqvt";
   1.240 -       val ex_eqvt             = thm "Nominal.pt_ex_eqvt";
   1.241 -       val pt_pi_rev           = thm "Nominal.pt_pi_rev";
   1.242 -       val pt_rev_pi           = thm "Nominal.pt_rev_pi";
   1.243 -       val at_exists_fresh     = thm "Nominal.at_exists_fresh";
   1.244 -       val at_exists_fresh'    = thm "Nominal.at_exists_fresh'";
   1.245 -       val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
   1.246 -       val fresh_perm_app      = thm "Nominal.pt_fresh_perm_app";	
   1.247 -       val fresh_aux           = thm "Nominal.pt_fresh_aux";  
   1.248 -       val pt_perm_supp_ineq   = thm "Nominal.pt_perm_supp_ineq";
   1.249 -       val pt_perm_supp        = thm "Nominal.pt_perm_supp";
   1.250 +       val abs_fun_pi          = @{thm "Nominal.abs_fun_pi"};
   1.251 +       val abs_fun_pi_ineq     = @{thm "Nominal.abs_fun_pi_ineq"};
   1.252 +       val abs_fun_eq          = @{thm "Nominal.abs_fun_eq"};
   1.253 +       val abs_fun_eq'         = @{thm "Nominal.abs_fun_eq'"};
   1.254 +       val abs_fun_fresh       = @{thm "Nominal.abs_fun_fresh"};
   1.255 +       val abs_fun_fresh'      = @{thm "Nominal.abs_fun_fresh'"};
   1.256 +       val dj_perm_forget      = @{thm "Nominal.dj_perm_forget"};
   1.257 +       val dj_pp_forget        = @{thm "Nominal.dj_perm_perm_forget"};
   1.258 +       val fresh_iff           = @{thm "Nominal.fresh_abs_fun_iff"};
   1.259 +       val fresh_iff_ineq      = @{thm "Nominal.fresh_abs_fun_iff_ineq"};
   1.260 +       val abs_fun_supp        = @{thm "Nominal.abs_fun_supp"};
   1.261 +       val abs_fun_supp_ineq   = @{thm "Nominal.abs_fun_supp_ineq"};
   1.262 +       val pt_swap_bij         = @{thm "Nominal.pt_swap_bij"};
   1.263 +       val pt_swap_bij'        = @{thm "Nominal.pt_swap_bij'"};
   1.264 +       val pt_fresh_fresh      = @{thm "Nominal.pt_fresh_fresh"};
   1.265 +       val pt_bij              = @{thm "Nominal.pt_bij"};
   1.266 +       val pt_perm_compose     = @{thm "Nominal.pt_perm_compose"};
   1.267 +       val pt_perm_compose'    = @{thm "Nominal.pt_perm_compose'"};
   1.268 +       val perm_app            = @{thm "Nominal.pt_fun_app_eq"};
   1.269 +       val at_fresh            = @{thm "Nominal.at_fresh"};
   1.270 +       val at_fresh_ineq       = @{thm "Nominal.at_fresh_ineq"};
   1.271 +       val at_calc             = @{thms "Nominal.at_calc"};
   1.272 +       val at_swap_simps       = @{thms "Nominal.at_swap_simps"};
   1.273 +       val at_supp             = @{thm "Nominal.at_supp"};
   1.274 +       val dj_supp             = @{thm "Nominal.dj_supp"};
   1.275 +       val fresh_left_ineq     = @{thm "Nominal.pt_fresh_left_ineq"};
   1.276 +       val fresh_left          = @{thm "Nominal.pt_fresh_left"};
   1.277 +       val fresh_right_ineq    = @{thm "Nominal.pt_fresh_right_ineq"};
   1.278 +       val fresh_right         = @{thm "Nominal.pt_fresh_right"};
   1.279 +       val fresh_bij_ineq      = @{thm "Nominal.pt_fresh_bij_ineq"};
   1.280 +       val fresh_bij           = @{thm "Nominal.pt_fresh_bij"};
   1.281 +       val fresh_eqvt          = @{thm "Nominal.pt_fresh_eqvt"};
   1.282 +       val fresh_eqvt_ineq     = @{thm "Nominal.pt_fresh_eqvt_ineq"};
   1.283 +       val set_diff_eqvt       = @{thm "Nominal.pt_set_diff_eqvt"};
   1.284 +       val in_eqvt             = @{thm "Nominal.pt_in_eqvt"};
   1.285 +       val eq_eqvt             = @{thm "Nominal.pt_eq_eqvt"};
   1.286 +       val all_eqvt            = @{thm "Nominal.pt_all_eqvt"};
   1.287 +       val ex_eqvt             = @{thm "Nominal.pt_ex_eqvt"};
   1.288 +       val pt_pi_rev           = @{thm "Nominal.pt_pi_rev"};
   1.289 +       val pt_rev_pi           = @{thm "Nominal.pt_rev_pi"};
   1.290 +       val at_exists_fresh     = @{thm "Nominal.at_exists_fresh"};
   1.291 +       val at_exists_fresh'    = @{thm "Nominal.at_exists_fresh'"};
   1.292 +       val fresh_perm_app_ineq = @{thm "Nominal.pt_fresh_perm_app_ineq"};
   1.293 +       val fresh_perm_app      = @{thm "Nominal.pt_fresh_perm_app"};	
   1.294 +       val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
   1.295 +       val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
   1.296 +       val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
   1.297  
   1.298         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
   1.299         (* types; this allows for example to use abs_perm (which is a      *)