added extended the lemma for equivariance of freshness
authorurbanc
Tue Mar 27 19:39:40 2007 +0200 (2007-03-27)
changeset 22535cbee450f88a6
parent 22534 bd4b954e85ee
child 22536 35debf264656
added extended the lemma for equivariance of freshness
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Tue Mar 27 19:13:28 2007 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Tue Mar 27 19:39:40 2007 +0200
     1.3 @@ -1590,6 +1590,18 @@
     1.4    shows "c\<sharp>(pi\<bullet>x)"
     1.5  using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj])
     1.6  
     1.7 +lemma pt_fresh_eqvt_ineq:
     1.8 +  fixes pi::"'x prm"
     1.9 +  and   c::"'y"
    1.10 +  and   x::"'a"
    1.11 +  assumes pta: "pt TYPE('a) TYPE('x)"
    1.12 +  and     ptb: "pt TYPE('y) TYPE('x)"
    1.13 +  and     at:  "at TYPE('x)"
    1.14 +  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
    1.15 +  and     dj:  "disjoint TYPE('y) TYPE('x)"
    1.16 +  shows "pi\<bullet>(c\<sharp>x) = (pi\<bullet>c)\<sharp>(pi\<bullet>x)"
    1.17 +by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
    1.18 +
    1.19  -- "three helper lemmas for the perm_fresh_fresh-lemma"
    1.20  lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
    1.21    by (auto)
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 27 19:13:28 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 27 19:39:40 2007 +0200
     2.3 @@ -700,6 +700,7 @@
     2.4         val fresh_aux_ineq      = thm "Nominal.pt_fresh_aux_ineq";
     2.5         val fresh_aux           = thm "Nominal.pt_fresh_aux";
     2.6         val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
     2.7 +       val fresh_eqvt_ineq     = thm "Nominal.pt_fresh_eqvt_ineq";
     2.8         val set_eqvt            = thm "Nominal.pt_set_eqvt";
     2.9         val set_diff_eqvt       = thm "Nominal.pt_set_diff_eqvt";
    2.10         val in_eqvt             = thm "Nominal.pt_in_eqvt";
    2.11 @@ -837,7 +838,8 @@
    2.12  	      in [(("fresh_bij", thms1 @ thms2),[])] end
    2.13              ||>> PureThy.add_thmss
    2.14  	      let val thms1 = inst_pt_at [fresh_eqvt]
    2.15 -	      in [(("fresh_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    2.16 +                  and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
    2.17 +	      in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
    2.18              ||>> PureThy.add_thmss
    2.19  	      let val thms1 = inst_pt_at [in_eqvt]
    2.20  	      in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end