Added equivariance lemmas for fresh_star.
--- a/src/HOL/Nominal/Nominal.thy Wed Feb 25 07:42:20 2009 +0100
+++ b/src/HOL/Nominal/Nominal.thy Wed Feb 25 11:02:25 2009 +0100
@@ -1645,6 +1645,31 @@
apply(rule at)
done
+lemma pt_fresh_star_eqvt:
+ fixes pi :: "'x prm"
+ and x :: "'a"
+ and a :: "'x set"
+ and b :: "'x list"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
+ and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
+ by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
+
+lemma pt_fresh_star_eqvt_ineq:
+ fixes pi::"'x prm"
+ and a::"'y set"
+ and b::"'y list"
+ 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>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
+ and "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
+ by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
+
lemma pt_fresh_bij1:
fixes pi :: "'x prm"
and x :: "'a"
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Feb 25 07:42:20 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Feb 25 11:02:25 2009 +0100
@@ -1,5 +1,4 @@
(* title: HOL/Nominal/nominal_atoms.ML
- ID: $Id$
Author: Christian Urban and Stefan Berghofer, TU Muenchen
Declaration of atom types to be used in nominal datatypes.
@@ -784,6 +783,8 @@
val fresh_star_bij = @{thms "Nominal.pt_fresh_star_bij"};
val fresh_eqvt = @{thm "Nominal.pt_fresh_eqvt"};
val fresh_eqvt_ineq = @{thm "Nominal.pt_fresh_eqvt_ineq"};
+ val fresh_star_eqvt = @{thms "Nominal.pt_fresh_star_eqvt"};
+ val fresh_star_eqvt_ineq= @{thms "Nominal.pt_fresh_star_eqvt_ineq"};
val set_diff_eqvt = @{thm "Nominal.pt_set_diff_eqvt"};
val in_eqvt = @{thm "Nominal.pt_in_eqvt"};
val eq_eqvt = @{thm "Nominal.pt_eq_eqvt"};
@@ -947,13 +948,17 @@
in [(("fresh_bij", thms1 @ thms2),[])] end
||>> add_thmss_string
let val thms1 = inst_pt_at fresh_star_bij
- and thms2 = flat (map (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq);
+ and thms2 = maps (fn ti => inst_pt_pt_at_cp [ti]) fresh_star_bij_ineq
in [(("fresh_star_bij", thms1 @ thms2),[])] end
||>> add_thmss_string
let val thms1 = inst_pt_at [fresh_eqvt]
and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
||>> add_thmss_string
+ let val thms1 = inst_pt_at fresh_star_eqvt
+ and thms2 = maps (fn ti => inst_pt_pt_at_cp_dj [ti]) fresh_star_eqvt_ineq
+ in [(("fresh_star_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
+ ||>> add_thmss_string
let val thms1 = inst_pt_at [in_eqvt]
in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
||>> add_thmss_string