--- a/src/HOL/Nominal/Examples/Class2.thy Tue Jan 10 23:26:27 2012 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Wed Jan 11 00:05:31 2012 +0100
@@ -2123,7 +2123,7 @@
lemma NOTRIGHT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2149,7 +2149,7 @@
lemma NOTRIGHT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2182,7 +2182,7 @@
lemma NOTLEFT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2208,7 +2208,7 @@
lemma NOTLEFT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2242,7 +2242,7 @@
lemma ANDRIGHT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>c" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -2277,7 +2277,7 @@
lemma ANDRIGHT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>c" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -2319,7 +2319,7 @@
lemma ANDLEFT1_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2345,7 +2345,7 @@
lemma ANDLEFT1_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2378,7 +2378,7 @@
lemma ANDLEFT2_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2404,7 +2404,7 @@
lemma ANDLEFT2_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2438,7 +2438,7 @@
lemma ORLEFT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>z" in exI)
@@ -2473,7 +2473,7 @@
lemma ORLEFT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>z" in exI)
@@ -2515,7 +2515,7 @@
lemma ORRIGHT1_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2541,7 +2541,7 @@
lemma ORRIGHT1_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2574,7 +2574,7 @@
lemma ORRIGHT2_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2600,7 +2600,7 @@
lemma ORRIGHT2_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -2636,7 +2636,7 @@
lemma IMPRIGHT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -2696,7 +2696,7 @@
lemma IMPRIGHT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -2763,7 +2763,7 @@
lemma IMPLEFT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
@@ -2798,7 +2798,7 @@
lemma IMPLEFT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
@@ -2902,7 +2902,7 @@
and Y::"('b::pt_coname) set set"
shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
and "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
-apply(auto simp add: perm_set_eq)
+apply(auto simp add: perm_set_def)
apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
apply(perm_simp)
apply(rule ballI)
@@ -3130,7 +3130,7 @@
fixes pi::"name prm"
shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)"
and "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)"
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
apply(simp)
@@ -3185,7 +3185,7 @@
fixes pi::"coname prm"
shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)"
and "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)"
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
apply(simp)
--- a/src/HOL/Nominal/Examples/Fsub.thy Tue Jan 10 23:26:27 2012 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy Wed Jan 11 00:05:31 2012 +0100
@@ -270,7 +270,7 @@
fixes x::"vrs"
shows "x\<sharp>vrs_of b = x\<sharp>b"
by (nominal_induct b rule: binding.strong_induct)
- (simp_all add: fresh_singleton [OF pt_vrs_inst at_vrs_inst] fresh_set_empty ty_vrs_fresh fresh_atm)
+ (simp_all add: fresh_singleton fresh_set_empty ty_vrs_fresh fresh_atm)
lemma fresh_trm_dom:
fixes x::"vrs"
@@ -292,27 +292,7 @@
| valid_consT[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(ty_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (TVarB X T#\<Gamma>) ok"
| valid_cons [simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; x\<sharp>(trm_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<turnstile> (VarB x T#\<Gamma>) ok"
-(* FIXME The two following theorems should be subsumed by:
equivariance valid_rel
-*)
-
-lemma valid_eqvt[eqvt]:
- fixes pi::"tyvrs prm"
- assumes a: "\<turnstile> \<Gamma> ok" shows "\<turnstile> (pi\<bullet>\<Gamma>) ok"
- using a
-apply(induct \<Gamma>)
-apply auto
-apply (metis closed_in_eqvt doms_eqvt(1) fresh_bij(1) valid_consT)
-by (metis closed_in_eqvt fresh_aux(3) fresh_trm_dom perm_dj(1) valid_cons)
-
-lemma valid_eqvt'[eqvt]:
- fixes pi::"vrs prm"
- assumes a: "\<turnstile> \<Gamma> ok" shows "\<turnstile> (pi\<bullet>\<Gamma>) ok"
- using a
-apply(induct \<Gamma>)
-apply auto
-apply (metis closed_in_eqvt' perm_dj(2) ty_dom_vrs_prm_simp valid_consT)
-by (metis closed_in_eqvt' fresh_bij(2) fresh_trm_dom valid_cons)
declare binding.inject [simp add]
declare trm.inject [simp add]
@@ -372,7 +352,7 @@
by (simp add: fresh_ty_dom_cons
fresh_fin_union[OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst]
finite_vrs finite_doms,
- auto simp add: fresh_atm fresh_singleton [OF pt_tyvrs_inst at_tyvrs_inst])
+ auto simp add: fresh_atm fresh_singleton)
qed (simp)
}
ultimately show "T=S" by (auto simp add: binding.inject)
@@ -396,7 +376,7 @@
thus "\<not> (\<exists>T.(VarB x' T)\<in>set(y#\<Gamma>'))"
by (simp add: fresh_fin_union[OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
finite_vrs finite_doms,
- auto simp add: fresh_atm fresh_singleton [OF pt_vrs_inst at_vrs_inst])
+ auto simp add: fresh_atm fresh_singleton)
qed (simp)
}
ultimately show "T=S" by (auto simp add: binding.inject)
--- a/src/HOL/Nominal/Examples/Support.thy Tue Jan 10 23:26:27 2012 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Wed Jan 11 00:05:31 2012 +0100
@@ -98,14 +98,14 @@
proof (cases "x\<in>S")
case True
have "x\<in>S" by fact
- hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
+ hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
then show "x\<in>(supp S)" by (simp add: supp_def)
next
case False
have "x\<notin>S" by fact
- hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
+ hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
then show "x\<in>(supp S)" by (simp add: supp_def)
@@ -129,7 +129,7 @@
shows "supp (UNIV::atom set) = ({}::atom set)"
proof -
have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
- by (auto simp add: perm_set_eq calc_atm)
+ by (auto simp add: perm_set_def calc_atm)
then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
qed
--- a/src/HOL/Nominal/Nominal.thy Tue Jan 10 23:26:27 2012 +0100
+++ b/src/HOL/Nominal/Nominal.thy Wed Jan 11 00:05:31 2012 +0100
@@ -58,7 +58,7 @@
"perm_bool pi b = b"
definition perm_set :: "'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "perm_set pi A = {x. rev pi \<bullet> x \<in> A}"
+ "perm_set pi X = {pi \<bullet> x | x. x \<in> X}"
primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" where
"perm_unit pi () = ()"
@@ -137,11 +137,15 @@
(* permutation on sets *)
lemma empty_eqvt:
shows "pi\<bullet>{} = {}"
- by (simp add: perm_set_def fun_eq_iff)
+ by (simp add: perm_set_def)
lemma union_eqvt:
shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
- by (simp add: perm_set_def fun_eq_iff Un_def)
+ by (auto simp add: perm_set_def)
+
+lemma insert_eqvt:
+ shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+ by (auto simp add: perm_set_def)
(* permutations on products *)
lemma fst_eqvt:
@@ -166,6 +170,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 characters and strings *)
lemma perm_string:
fixes s::"string"
@@ -1018,16 +1028,13 @@
by (simp add: pt_def perm_bool_def)
lemma pt_set_inst:
- assumes pta: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "pt TYPE('a set) TYPE('x)"
-proof -
- have *: "\<And>pi A. pi \<bullet> A = {x. (pi \<bullet> (\<lambda>x. x \<in> A)) x}"
- by (simp add: perm_fun_def perm_bool_def perm_set_def)
- from pta pt_bool_inst at
- have "pt TYPE('a \<Rightarrow> bool) TYPE('x)" by (rule pt_fun_inst)
- then show ?thesis by (simp add: pt_def *)
-qed
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ shows "pt TYPE('a set) TYPE('x)"
+apply(simp add: pt_def)
+apply(simp_all add: perm_set_def)
+apply(simp add: pt1[OF pt])
+apply(force simp add: pt2[OF pt] pt3[OF pt])
+done
lemma pt_unit_inst:
shows "pt TYPE(unit) TYPE('x)"
@@ -1245,43 +1252,13 @@
apply(rule pt1[OF pt])
done
-lemma perm_set_eq:
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "(pi::'x prm)\<bullet>(X::'a set) = {pi\<bullet>x | x. x\<in>X}"
- apply (auto simp add: perm_fun_def perm_bool perm_set_def)
- apply (rule_tac x="rev pi \<bullet> x" in exI)
- apply (simp add: pt_pi_rev [OF pt at])
- apply (simp add: pt_rev_pi [OF pt at])
- done
-
-lemma pt_insert_eqvt:
- fixes pi::"'x prm"
- and x::"'a"
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "(pi\<bullet>(insert x X)) = insert (pi\<bullet>x) (pi\<bullet>X)"
- by (auto simp add: perm_set_eq [OF pt at])
-
-lemma pt_set_eqvt:
- fixes pi :: "'x prm"
- and xs :: "'a list"
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs) (auto simp add: empty_eqvt pt_insert_eqvt [OF pt at])
-
lemma supp_singleton:
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "(supp {x::'a} :: 'x set) = supp x"
- by (force simp add: supp_def perm_set_eq [OF pt at])
+ shows "supp {x} = supp x"
+ by (force simp add: supp_def perm_set_def)
lemma fresh_singleton:
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "(a::'x)\<sharp>{x::'a} = a\<sharp>x"
- by (simp add: fresh_def supp_singleton [OF pt at])
+ shows "a\<sharp>{x} = a\<sharp>x"
+ by (simp add: fresh_def supp_singleton)
lemma pt_set_bij1:
fixes pi :: "'x prm"
@@ -1290,7 +1267,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
- by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+ by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
lemma pt_set_bij1a:
fixes pi :: "'x prm"
@@ -1299,7 +1276,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
- by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+ by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
lemma pt_set_bij:
fixes pi :: "'x prm"
@@ -1308,7 +1285,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
- by (simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
+ by (simp add: perm_set_def pt_bij[OF pt, OF at])
lemma pt_in_eqvt:
fixes pi :: "'x prm"
@@ -1355,7 +1332,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
-by (auto simp add: perm_set_eq [OF pt at] perm_bool pt_bij[OF pt, OF at])
+by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
lemma pt_set_diff_eqvt:
fixes X::"'a set"
@@ -1364,14 +1341,14 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
- by (auto simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
+ by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
lemma pt_Collect_eqvt:
fixes pi::"'x prm"
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
-apply(auto simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at])
+apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
apply(rule_tac x="(rev pi)\<bullet>x" in exI)
apply(simp add: pt_pi_rev[OF pt, OF at])
done
@@ -1415,7 +1392,7 @@
and at: "at TYPE('y)"
shows "finite (pi\<bullet>X) = finite X"
proof -
- have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_eq [OF pt at])
+ have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
show ?thesis
proof (rule iffI)
assume "finite (pi\<bullet>X)"
@@ -1445,17 +1422,17 @@
and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
proof -
- have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_eq [OF ptb at])
+ have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}"
proof (rule Collect_permI, rule allI, rule iffI)
fix a
assume "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}"
hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
- thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: perm_set_eq [OF ptb at])
+ thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: perm_set_def)
next
fix a
assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
- hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_eq [OF ptb at])
+ hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
thus "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}"
by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
qed
@@ -1981,7 +1958,7 @@
shows "X supports X"
proof -
have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X"
- by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
+ by (auto simp add: perm_set_def at_calc[OF at])
then show ?thesis by (simp add: supports_def)
qed
@@ -2008,7 +1985,7 @@
{ fix a::"'x"
assume asm: "a\<in>X"
hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X"
- by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
+ by (auto simp add: perm_set_def at_calc[OF at])
with inf have "infinite {b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X}" by (rule infinite_Collection)
hence "infinite {b. [(a,b)]\<bullet>X\<noteq>X}" by (rule_tac infinite_super, auto)
hence "a\<in>(supp X)" by (simp add: supp_def)
@@ -2229,7 +2206,7 @@
proof (rule equalityI)
case goal1
show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
- apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
+ apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule conjI)
apply(rule_tac x="xb" in exI)
@@ -2245,7 +2222,7 @@
next
case goal2
show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
- apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
+ apply(auto simp add: perm_set_def)
apply(rule_tac x="(rev pi)\<bullet>x" in exI)
apply(rule conjI)
apply(simp add: pt_pi_rev[OF pt_x, OF at])
@@ -2278,7 +2255,7 @@
apply(rule allI)+
apply(rule impI)
apply(erule conjE)
- apply(simp add: perm_set_eq [OF pt at])
+ apply(simp add: perm_set_def)
apply(auto)
apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
apply(simp)
@@ -2362,7 +2339,7 @@
also have "\<dots> = (supp {x})\<union>(supp X)"
by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)"
- by (simp add: supp_singleton [OF pt at])
+ by (simp add: supp_singleton)
qed
lemma fresh_fin_union:
@@ -2513,10 +2490,10 @@
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
apply(drule_tac x="pi\<bullet>xa" in bspec)
apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
+apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt)
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
done
@@ -2638,10 +2615,7 @@
have "({}::'a set) \<inter> As = {}" by simp
moreover
have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp
- moreover
- have "([]::'a prm)\<bullet>{} = ({}::'a set)"
- by (rule pt1 [OF pt_set_inst, OF at_pt_inst [OF at] at])
- ultimately show ?case by simp
+ ultimately show ?case by (simp add: empty_eqvt)
next
case (insert x Xs)
then have ih: "\<exists>pi. (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by simp
@@ -2655,7 +2629,7 @@
obtain y::"'a" where fr: "y\<sharp>(c,pi\<bullet>Xs,As)"
apply(rule_tac at_exists_fresh[OF at, where x="(c,pi\<bullet>Xs,As)"])
apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at]
- pt_supp_finite_pi[OF pt_set_inst[OF at_pt_inst[OF at] at] at])
+ pt_supp_finite_pi[OF pt_set_inst[OF at_pt_inst[OF at]] at])
done
have "({y}\<union>(pi\<bullet>Xs))\<sharp>*c" using a1 fr by (simp add: fresh_star_def)
moreover
@@ -2671,20 +2645,18 @@
have eq: "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)"
proof -
have "(pi\<bullet>x)\<sharp>(pi\<bullet>Xs)" using b d2
- by (simp add: pt_fresh_bij [OF pt_set_inst, OF at_pt_inst [OF at],
- OF at, OF at]
+ by (simp add: pt_fresh_bij [OF pt_set_inst [OF at_pt_inst [OF at]], OF at]
at_fin_set_fresh [OF at])
moreover
have "y\<sharp>(pi\<bullet>Xs)" using fr by simp
ultimately show "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)"
- by (simp add: pt_fresh_fresh[OF pt_set_inst,
- OF at_pt_inst[OF at], OF at, OF at])
+ by (simp add: pt_fresh_fresh[OF pt_set_inst
+ [OF at_pt_inst[OF at]], OF at])
qed
have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
- by (simp add: pt2[symmetric, OF pt_set_inst, OF at_pt_inst[OF at],
- OF at])
+ by (simp add: pt2[symmetric, OF pt_set_inst [OF at_pt_inst[OF at]]])
also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))"
- by (simp only: union_eqvt perm_set_eq[OF at_pt_inst[OF at], OF at] at_calc[OF at])(auto)
+ by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto)
finally show "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)" using eq by simp
qed
ultimately
@@ -2714,6 +2686,17 @@
apply(auto)
done
+lemma cp_set_inst:
+ assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
+ shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
+using c1
+apply(simp add: cp_def)
+apply(auto)
+apply(auto simp add: perm_set_def)
+apply(rule_tac x="pi2\<bullet>xc" in exI)
+apply(auto)
+done
+
lemma cp_option_inst:
assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
@@ -3596,7 +3579,7 @@
plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
(* sets *)
- union_eqvt empty_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 Tue Jan 10 23:26:27 2012 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Jan 11 00:05:31 2012 +0100
@@ -542,7 +542,7 @@
rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
- val pt_thm_set = at_thm RS (pt_inst RS pt_set_inst);
+ val pt_thm_set = pt_inst RS pt_set_inst;
val pt_thm_noptn = pt_inst RS pt_noptn_inst;
val pt_thm_optn = pt_inst RS pt_optn_inst;
val pt_thm_list = pt_inst RS pt_list_inst;
@@ -635,6 +635,7 @@
val cp_fun_inst = @{thm "cp_fun_inst"};
val cp_option_inst = @{thm "cp_option_inst"};
val cp_noption_inst = @{thm "cp_noption_inst"};
+ val cp_set_inst = @{thm "cp_set_inst"};
val pt_perm_compose = @{thm "pt_perm_compose"};
val dj_pp_forget = @{thm "dj_perm_perm_forget"};
@@ -696,6 +697,7 @@
val cp_thm_fun = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)));
val cp_thm_optn = cp_inst RS cp_option_inst;
val cp_thm_noptn = cp_inst RS cp_noption_inst;
+ val cp_thm_set = cp_inst RS cp_set_inst;
in
thy'
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
@@ -704,6 +706,7 @@
|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
|> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
|> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+ |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
end) ak_names thy) ak_names thy25;
(* show that discrete nominal types are permutation types, finitely *)
@@ -817,9 +820,6 @@
val pt_perm_supp_ineq = @{thm "Nominal.pt_perm_supp_ineq"};
val pt_perm_supp = @{thm "Nominal.pt_perm_supp"};
val subseteq_eqvt = @{thm "Nominal.pt_subseteq_eqvt"};
- val insert_eqvt = @{thm "Nominal.pt_insert_eqvt"};
- val set_eqvt = @{thm "Nominal.pt_set_eqvt"};
- val perm_set_eq = @{thm "Nominal.perm_set_eq"};
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
(* types; this allows for example to use abs_perm (which is a *)
@@ -985,9 +985,6 @@
||>> add_thmss_string
let val thms1 = inst_pt_at [subseteq_eqvt]
in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
- ||>> add_thmss_string [(("insert_eqvt", inst_pt_at [insert_eqvt]), [NominalThmDecls.eqvt_add])]
- ||>> add_thmss_string [(("set_eqvt", inst_pt_at [set_eqvt]), [NominalThmDecls.eqvt_add])]
- ||>> add_thmss_string [(("perm_set_eq", inst_pt_at [perm_set_eq]), [])]
||>> add_thmss_string
let val thms1 = inst_pt_at [fresh_aux]
and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq]