added the collection of lemmas "supp_at"
authorurbanc
Wed Nov 02 11:02:29 2005 +0100 (2005-11-02)
changeset 180542493cb9f5ede
parent 18053 2719a6b7d95e
child 18055 a93881a4422d
added the collection of lemmas "supp_at"
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Nov 01 23:55:53 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 11:02:29 2005 +0100
     1.3 @@ -770,6 +770,10 @@
     1.4         val pt_bij            = PureThy.get_thm thy32 (Name ("nominal.pt_bij"));
     1.5         val pt_perm_compose   = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose"));
     1.6         val perm_eq_app       = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app"));
     1.7 +       val at_fresh          = PureThy.get_thm thy32 (Name ("nominal.at_fresh"));
     1.8 +       (*val at_calc           = PureThy.get_thms thy32 (Name ("nominal.at_calc"));*)
     1.9 +       val at_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
    1.10 +       val dj_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
    1.11  
    1.12         (* abs_perm collects all lemmas for simplifying a permutation *)
    1.13         (* in front of an abs_fun                                     *)
    1.14 @@ -792,31 +796,21 @@
    1.15               (PureThy.add_thmss [((name, thm_list),[])] thy32)
    1.16             end;
    1.17  
    1.18 -        (* alpha collects all lemmas analysing an equation *)
    1.19 -        (* between abs_funs                                *)
    1.20 -        (*val (thy34,_) = 
    1.21 +       val (thy34,_) = 
    1.22  	   let 
    1.23 -	     val name = "alpha"
    1.24 -             val thm_list = map (fn (ak_name, T) =>
    1.25 -	        let	
    1.26 -		  val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
    1.27 -		  val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
    1.28 -	        in
    1.29 -                  [pt_inst, at_inst] MRS abs_fun_eq
    1.30 -	        end) ak_names_types
    1.31 -           in
    1.32 -             (PureThy.add_thmss [((name, thm_list),[])] thy33)
    1.33 -           end;*)
    1.34 - 
    1.35 -          val (thy34,_) = 
    1.36 -	   let 
    1.37 -	     fun inst_pt_at thm ak_name =
    1.38 +	       fun inst_pt_at thm ak_name =
    1.39  		 let	
    1.40  		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
    1.41  		   val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
    1.42  	         in
    1.43                       [pt_inst, at_inst] MRS thm
    1.44 -	         end	 
    1.45 +	         end	
    1.46 +               fun inst_at thm ak_name =
    1.47 +		 let	
    1.48 +		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
    1.49 +                 in
    1.50 +                     at_inst RS thm
    1.51 +	         end
    1.52  
    1.53             in
    1.54              thy33 
    1.55 @@ -826,6 +820,11 @@
    1.56              |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]
    1.57              |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]
    1.58              |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]
    1.59 +            |>>> PureThy.add_thmss [(("supp_at", map (inst_at at_supp) ak_names),[])]
    1.60 +            (*|>>> PureThy.add_thmss [(("fresh_at", map (inst_at at_fresh) ak_names),
    1.61 +                                    [Simplifier.simp_add_global])]*)
    1.62 +            (*|>>> PureThy.add_thmss [(("calc_at", map (inst_at at_calc) ak_names),
    1.63 +                                    [Simplifier.simp_add_global])]*)
    1.64  	   end;
    1.65  
    1.66           (* perm_dj collects all lemmas that forget an permutation *)