--- a/src/HOL/Nominal/Nominal.thy Tue Mar 27 19:13:28 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Tue Mar 27 19:39:40 2007 +0200
@@ -1590,6 +1590,18 @@
shows "c\<sharp>(pi\<bullet>x)"
using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj])
+lemma pt_fresh_eqvt_ineq:
+ fixes pi::"'x prm"
+ and c::"'y"
+ and x::"'a"
+ assumes pta: "pt TYPE('a) TYPE('x)"
+ and ptb: "pt TYPE('y) TYPE('x)"
+ and at: "at TYPE('x)"
+ and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
+ and dj: "disjoint TYPE('y) TYPE('x)"
+ shows "pi\<bullet>(c\<sharp>x) = (pi\<bullet>c)\<sharp>(pi\<bullet>x)"
+by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
+
-- "three helper lemmas for the perm_fresh_fresh-lemma"
lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
by (auto)
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Mar 27 19:13:28 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Mar 27 19:39:40 2007 +0200
@@ -700,6 +700,7 @@
val fresh_aux_ineq = thm "Nominal.pt_fresh_aux_ineq";
val fresh_aux = thm "Nominal.pt_fresh_aux";
val fresh_eqvt = thm "Nominal.pt_fresh_eqvt";
+ val fresh_eqvt_ineq = thm "Nominal.pt_fresh_eqvt_ineq";
val set_eqvt = thm "Nominal.pt_set_eqvt";
val set_diff_eqvt = thm "Nominal.pt_set_diff_eqvt";
val in_eqvt = thm "Nominal.pt_in_eqvt";
@@ -837,7 +838,8 @@
in [(("fresh_bij", thms1 @ thms2),[])] end
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [fresh_eqvt]
- in [(("fresh_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
+ and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
+ in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
||>> PureThy.add_thmss
let val thms1 = inst_pt_at [in_eqvt]
in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end