src/HOL/Nominal/nominal_package.ML
changeset 18067 8b9848d150ba
parent 18066 d1e47ee13070
child 18068 e8c3d371594e
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 15:05:22 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Nov 02 15:31:12 2005 +0100
     1.3 @@ -49,6 +49,9 @@
     1.4    let val T = fastype_of x
     1.5    in Const ("List.list.Cons", T --> mk_listT T --> mk_listT T) $ x $ xs end;
     1.6  
     1.7 +(* FIXME: should be a library function *)
     1.8 +fun cprod ([], ys) = []
     1.9 +  | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
    1.10  
    1.11  (* this function sets up all matters related to atom-  *)
    1.12  (* kinds; the user specifies a list of atom-kind names *)
    1.13 @@ -771,9 +774,9 @@
    1.14         val pt_perm_compose   = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose"));
    1.15         val perm_eq_app       = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app"));
    1.16         val at_fresh          = PureThy.get_thm thy32 (Name ("nominal.at_fresh"));
    1.17 -       (*val at_calc           = PureThy.get_thms thy32 (Name ("nominal.at_calc"));*)
    1.18 +       val at_calc           = PureThy.get_thms thy32 (Name ("nominal.at_calc"));
    1.19         val at_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
    1.20 -       val dj_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
    1.21 +       val dj_supp           = PureThy.get_thm thy32 (Name ("nominal.dj_supp"));
    1.22  
    1.23         (* abs_perm collects all lemmas for simplifying a permutation *)
    1.24         (* in front of an abs_fun                                     *)
    1.25 @@ -797,34 +800,51 @@
    1.26             end;
    1.27  
    1.28         val (thy34,_) = 
    1.29 -	   let 
    1.30 -	       fun inst_pt_at thm ak_name =
    1.31 -		 let	
    1.32 -		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
    1.33 -		   val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
    1.34 -	         in
    1.35 -                     [pt_inst, at_inst] MRS thm
    1.36 -	         end	
    1.37 -               fun inst_at thm ak_name =
    1.38 -		 let	
    1.39 -		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
    1.40 -                 in
    1.41 -                     at_inst RS thm
    1.42 -	         end
    1.43 +	 let 
    1.44 +             (* takes a theorem and a list of theorems        *)
    1.45 +             (* produces a list of theorems of the form       *)
    1.46 +             (* [t1 RS thm,..,tn RS thm] where t1..tn in thms *) 
    1.47 +             fun instantiate thm thms = map (fn ti => ti RS thm) thms;
    1.48 +               
    1.49 +             (* takes two theorem lists (hopefully of the same length)           *)
    1.50 +             (* produces a list of theorems of the form                          *)
    1.51 +             (* [t1 RS m1,..,tn RS mn] where t1..tn in thms1 and m1..mn in thms2 *) 
    1.52 +             fun instantiate_zip thms1 thms2 = 
    1.53 +		 map (fn (t1,t2) => t1 RS t2) (thms1 ~~ thms2);
    1.54 +
    1.55 +             (* list of all at_inst-theorems *)
    1.56 +             val ats = map (fn ak => PureThy.get_thm thy33 (Name ("at_"^ak^"_inst"))) ak_names
    1.57 +             (* list of all pt_inst-theorems *)
    1.58 +             val pts = map (fn ak => PureThy.get_thm thy33 (Name ("pt_"^ak^"_inst"))) ak_names
    1.59 +             (* list of all cp_inst-theorems *)
    1.60 +             val cps = 
    1.61 +	       let fun cps_fun (ak1,ak2) = PureThy.get_thm thy33 (Name ("cp_"^ak1^"_"^ak2^"_inst"))
    1.62 +	       in map cps_fun (cprod (ak_names,ak_names)) end;	
    1.63 +             (* list of all dj_inst-theorems *)
    1.64 +             val djs = 
    1.65 +	       let fun djs_fun (ak1,ak2) = 
    1.66 +		    if ak1=ak2 
    1.67 +		    then NONE
    1.68 +		    else SOME(PureThy.get_thm thy33 (Name ("dj_"^ak1^"_"^ak2)))
    1.69 +	       in List.mapPartial I (map djs_fun (cprod (ak_names,ak_names))) end;	
    1.70 +
    1.71 +             fun inst_pt thms = Library.flat (map (fn ti => instantiate ti pts) thms); 
    1.72 +             fun inst_at thms = Library.flat (map (fn ti => instantiate ti ats) thms);               
    1.73 +	     fun inst_pt_at thms = instantiate_zip ats (inst_pt thms);			
    1.74 +             fun inst_dj thms = Library.flat (map (fn ti => instantiate ti djs) thms);  
    1.75  
    1.76             in
    1.77              thy33 
    1.78 -	    |> PureThy.add_thmss   [(("alpha", map (inst_pt_at abs_fun_eq) ak_names),[])]
    1.79 -            |>>> PureThy.add_thmss [(("perm_swap", map (inst_pt_at pt_swap_bij) ak_names),[])]
    1.80 -            |>>> PureThy.add_thmss [(("perm_fresh_fresh", map (inst_pt_at pt_fresh_fresh) ak_names),[])]
    1.81 -            |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]
    1.82 -            |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]
    1.83 -            |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]
    1.84 -            |>>> PureThy.add_thmss [(("supp_at", map (inst_at at_supp) ak_names),[])]
    1.85 -            (*|>>> PureThy.add_thmss [(("fresh_at", map (inst_at at_fresh) ak_names),
    1.86 -                                    [Simplifier.simp_add_global])]*)
    1.87 -            (*|>>> PureThy.add_thmss [(("calc_at", map (inst_at at_calc) ak_names),
    1.88 -                                    [Simplifier.simp_add_global])]*)
    1.89 +	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.90 +            |>>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
    1.91 +            |>>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
    1.92 +            |>>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
    1.93 +            |>>> PureThy.add_thmss [(("perm_compose", inst_pt_at [pt_perm_compose]),[])]
    1.94 +            |>>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])]
    1.95 +            |>>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    1.96 +            |>>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
    1.97 +            |>>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
    1.98 +            
    1.99  	   end;
   1.100  
   1.101           (* perm_dj collects all lemmas that forget an permutation *)
   1.102 @@ -1900,7 +1920,7 @@
   1.103      val indnames = DatatypeProp.make_tnames recTs;
   1.104  
   1.105      val abs_supp = PureThy.get_thms thy8 (Name "abs_supp");
   1.106 -    val supp_at = PureThy.get_thms thy8 (Name "supp_at");
   1.107 +    val supp_atm = PureThy.get_thms thy8 (Name "supp_atm");
   1.108  
   1.109      val finite_supp_thms = map (fn atom =>
   1.110        let val atomT = Type (atom, [])
   1.111 @@ -1912,7 +1932,7 @@
   1.112                 (indnames ~~ recTs))))
   1.113             (fn _ => indtac dt_induct indnames 1 THEN
   1.114              ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
   1.115 -              (abs_supp @ supp_at @
   1.116 +              (abs_supp @ supp_atm @
   1.117                 PureThy.get_thms thy8 (Name ("fs_" ^ Sign.base_name atom ^ "1")) @
   1.118                 List.concat supp_thms))))),
   1.119           length new_type_names))