src/HOL/Nominal/nominal_atoms.ML
changeset 19139 af69e41eab5d
parent 19134 47d337aefc21
child 19165 7dc4fc25de8d
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Feb 25 15:19:47 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Feb 26 22:24:05 2006 +0100
     1.3 @@ -658,7 +658,8 @@
     1.4         val pt_fresh_fresh    = thm "nominal.pt_fresh_fresh";
     1.5         val pt_bij            = thm "nominal.pt_bij";
     1.6         val pt_perm_compose   = thm "nominal.pt_perm_compose";
     1.7 -       val perm_eq_app       = thm "nominal.perm_eq_app";
     1.8 +       val pt_perm_compose'  = thm "nominal.pt_perm_compose'";
     1.9 +       val perm_app          = thm "nominal.pt_fun_app_eq";
    1.10         val at_fresh          = thm "nominal.at_fresh";
    1.11         val at_calc           = thms "nominal.at_calc";
    1.12         val at_supp           = thm "nominal.at_supp";
    1.13 @@ -667,6 +668,8 @@
    1.14         val fresh_left        = thm "nominal.pt_fresh_left";
    1.15         val fresh_bij_ineq    = thm "nominal.pt_fresh_bij_ineq";
    1.16         val fresh_bij         = thm "nominal.pt_fresh_bij";
    1.17 +       val pt_pi_rev         = thm "nominal.pt_pi_rev";
    1.18 +       val pt_rev_pi         = thm "nominal.pt_rev_pi";
    1.19  
    1.20         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.21         (* types; this allows for example to use abs_perm (which is a      *)
    1.22 @@ -732,13 +735,18 @@
    1.23              thy32 
    1.24  	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.25              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
    1.26 +            ||>> PureThy.add_thmss 
    1.27 +	      let val thms1 = inst_pt_at [pt_pi_rev];
    1.28 +		  val thms2 = inst_pt_at [pt_rev_pi];
    1.29 +              in [(("perm_pi_simp",thms1 @ thms2),[])] end
    1.30              ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
    1.31              ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
    1.32              ||>> PureThy.add_thmss 
    1.33  	      let val thms1 = inst_pt_at [pt_perm_compose];
    1.34  		  val thms2 = instR cp1 (Library.flat cps');
    1.35                in [(("perm_compose",thms1 @ thms2),[])] end
    1.36 -            ||>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])]
    1.37 +            ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
    1.38 +            ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
    1.39              ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
    1.40              ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
    1.41              ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]