--- a/src/HOL/Nominal/Nominal.thy Mon Apr 23 16:38:40 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy Mon Apr 23 18:38:42 2007 +0200
@@ -78,6 +78,12 @@
shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
by (induct l) (simp_all add: append_eqvt)
+lemma set_eqvt:
+ fixes pi :: "'x prm"
+ and xs :: "'a list"
+ shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
+by (induct xs, auto simp add: empty_eqvt insert_eqvt)
+
(* permutation on functions *)
defs (unchecked overloaded)
perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
@@ -2279,13 +2285,6 @@
apply(simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
done
-lemma pt_set_eqvt:
- fixes pi :: "'x prm"
- and xs :: "'a list"
- assumes pt: "pt TYPE('a) TYPE('x)"
- shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs, auto simp add: perm_set_def pt1[OF pt])
-
lemma pt_list_set_supp:
fixes xs :: "'a list"
assumes pt: "pt TYPE('a) TYPE('x)"
@@ -3187,7 +3186,7 @@
plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
(* sets *)
- union_eqvt empty_eqvt insert_eqvt
+ union_eqvt empty_eqvt insert_eqvt set_eqvt
(* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
--- a/src/HOL/Nominal/nominal_atoms.ML Mon Apr 23 16:38:40 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Mon Apr 23 18:38:42 2007 +0200
@@ -707,7 +707,6 @@
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";
val eq_eqvt = thm "Nominal.pt_eq_eqvt";
@@ -854,9 +853,6 @@
let val thms1 = inst_pt_at [eq_eqvt]
in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
||>> PureThy.add_thmss
- let val thms1 = inst_pt [set_eqvt]
- in [(("set_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
- ||>> PureThy.add_thmss
let val thms1 = inst_pt_at [set_diff_eqvt]
in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
||>> PureThy.add_thmss