--- a/LMCS-Review Tue Jan 03 01:42:10 2012 +0000
+++ b/LMCS-Review Tue Jan 03 11:43:27 2012 +0000
@@ -203,6 +203,18 @@
> of pairs. I think that the system should at the very least allow encoding
> this example, otherwise set-abstractions will not be very useful in
> practice.
+
+>> datatype trm =
+>> Var string
+>> | App trm trm
+>> | Lam string trm
+>> | Let "(string * trm) fset" trm
+>> Not a problem. Both finite sets and bags should be possible as
+>> constructors within the new package.
+>> Best regards and a happy new year!
+>> Andrei Popescu
+
+
>
> Detailed comments
>
--- a/Nominal/Ex/LamTest.thy Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/LamTest.thy Tue Jan 03 11:43:27 2012 +0000
@@ -1658,7 +1658,7 @@
and S::"'a::at set"
assumes a: "a \<notin> S" "b \<notin> S"
shows "(a \<leftrightarrow> b) \<bullet> S = S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: permute_flip_at)
lemma removeAll_eqvt[eqvt]:
--- a/Nominal/Ex/TypeSchemes1.thy Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy Tue Jan 03 11:43:27 2012 +0000
@@ -2,7 +2,7 @@
imports "../Nominal2"
begin
-section {*** Type Schemes defined as two separate nominal datatypes ***}
+section {* Type Schemes defined as two separate nominal datatypes *}
atom_decl name
@@ -26,6 +26,40 @@
thm tys.supp
thm tys.fresh
+subsection {* Some Tests about Alpha-Equality *}
+
+lemma
+ shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
+ apply(simp add: Abs_eq_iff)
+ apply(rule_tac x="0::perm" in exI)
+ apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+ done
+
+lemma
+ shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
+ apply(simp add: Abs_eq_iff)
+ apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+ apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
+ done
+
+lemma
+ shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
+ apply(simp add: Abs_eq_iff)
+ apply(rule_tac x="0::perm" in exI)
+ apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+done
+
+lemma
+ assumes a: "a \<noteq> b"
+ shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
+ using a
+ apply(simp add: Abs_eq_iff)
+ apply(clarify)
+ apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+ apply auto
+ done
+
+
subsection {* Substitution function for types and type schemes *}
type_synonym
@@ -39,10 +73,7 @@
lemma lookup_eqvt[eqvt]:
shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
-apply(simp_all)
-done
-
+ by (induct Ts T rule: lookup.induct) (simp_all)
nominal_primrec
subst :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
@@ -124,69 +155,14 @@
termination (eqvt)
by (lexicographic_order)
-text {* Some Tests about Alpha-Equality *}
-lemma
- shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
- apply(simp add: Abs_eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
- done
-
-lemma
- shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
- apply(simp add: Abs_eq_iff)
- apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
- apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
- done
-
-lemma
- shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
- apply(simp add: Abs_eq_iff)
- apply(rule_tac x="0::perm" in exI)
- apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
-done
+subsection {* Generalisation of types and type-schemes*}
-lemma
- assumes a: "a \<noteq> b"
- shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
- using a
- apply(simp add: Abs_eq_iff)
- apply(clarify)
- apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
- apply auto
- done
-
-
-text {* HERE *}
-
-fun
- compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
+fun
+ subst_dom_pi :: "Subst \<Rightarrow> perm \<Rightarrow> Subst" ("_|_")
where
- "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"
-| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"
-
-lemma compose_eqvt:
- fixes \<theta>1 \<theta>2::"Subst"
- shows "(p \<bullet> (\<theta>1 \<circ> \<theta>2)) = ((p \<bullet> \<theta>1) \<circ> (p \<bullet> \<theta>2))"
-apply(induct \<theta>2)
-apply(auto simp add: subst.eqvt)
-done
-
-lemma compose_ty:
- fixes \<theta>1 :: "Subst"
- and \<theta>2 :: "Subst"
- and T :: "ty"
- shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"
-proof (induct T rule: ty.induct)
- case (Var X)
- have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X"
- by (induct \<theta>2) (auto)
- then show ?case by simp
-next
- case (Fun T1 T2)
- then show ?case by simp
-qed
+ "[]|p = []"
+| "((X,T)#\<theta>)|p = (p \<bullet> X, T)#(\<theta>|p)"
fun
subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>" [100,60] 120)
@@ -194,12 +170,6 @@
"\<theta><[]> = []"
| "\<theta> <((X,T)#\<theta>')> = (X,\<theta><T>)#(\<theta><\<theta>'>)"
-lemma redundant1:
- fixes \<theta>1::"Subst"
- and \<theta>2::"Subst"
- shows "\<theta>1 \<circ> \<theta>2 = (\<theta>1<\<theta>2>)@\<theta>1"
-by (induct \<theta>2) (auto)
-
fun
dom :: "Subst \<Rightarrow> name fset"
where
@@ -207,38 +177,24 @@
| "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>"
lemma dom_eqvt[eqvt]:
- shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)"
-apply(induct \<theta> rule: dom.induct)
-apply(simp_all)
-done
+ shows "p \<bullet> (dom \<theta>) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
-lemma dom_compose:
- shows "dom (\<theta>1 \<circ> \<theta>2) = dom \<theta>1 |\<union>| dom \<theta>2"
-apply(induct rule: dom.induct)
-apply(simp)
-apply(simp)
-by (metis sup_commute union_insert_fset)
-
-lemma redundant3:
- fixes \<theta>1::"Subst"
- and \<theta>2::"Subst"
+lemma dom_subst:
+ fixes \<theta>1 \<theta>2::"Subst"
shows "dom (\<theta>2<\<theta>1>) = (dom \<theta>1)"
by (induct \<theta>1) (auto)
lemma dom_pi:
- shows "(p \<bullet> (dom \<theta>)) = dom (map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>)"
-apply(induct \<theta>)
-apply(auto)
-done
+ shows "dom (\<theta>|p) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
lemma dom_fresh_lookup:
fixes \<theta>::"Subst"
- assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> name"
- shows "lookup \<theta> name = Var name"
+ assumes "\<forall>Y \<in> fset (dom \<theta>). atom Y \<sharp> X"
+ shows "lookup \<theta> X = Var X"
using assms
-apply(induct \<theta>)
-apply(auto simp add: fresh_at_base)
-done
+by (induct \<theta>) (auto simp add: fresh_at_base)
lemma dom_fresh_ty:
fixes \<theta>::"Subst"
@@ -246,30 +202,20 @@
assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> T"
shows "\<theta><T> = T"
using assms
-apply(induct T rule: ty.induct)
-apply(auto simp add: ty.fresh dom_fresh_lookup)
-done
+by (induct T rule: ty.induct) (auto simp add: ty.fresh dom_fresh_lookup)
lemma dom_fresh_subst:
fixes \<theta> \<theta>'::"Subst"
assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> \<theta>'"
shows "\<theta><\<theta>'> = \<theta>'"
using assms
-apply(induct \<theta>')
-apply(auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
-done
-
-
-abbreviation
- "sub_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60)
-where
- "xs\<^isub>1 \<subseteq> xs\<^isub>2 \<equiv> \<forall>x. x \<in> set xs\<^isub>1 \<longrightarrow> x \<in> set xs\<^isub>2"
+by (induct \<theta>') (auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
definition
- generalises3 :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec>\<prec>\<prec> _")
+ generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
where
- " T \<prec>\<prec>\<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
+ "T \<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
lemma lookup_fresh:
@@ -277,40 +223,34 @@
assumes a: "atom X \<sharp> \<theta>"
shows "lookup \<theta> X = Var X"
using a
- apply (induct \<theta>)
- apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
- done
+ by (induct \<theta>) (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
lemma lookup_dom:
fixes X::"name"
- assumes a: "X |\<notin>| dom \<theta>"
+ assumes "X |\<notin>| dom \<theta>"
shows "lookup \<theta> X = Var X"
- using a
- apply (induct \<theta>)
- apply(auto)
- done
+ using assms
+ by (induct \<theta>) (auto)
lemma w1:
- "\<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'> = map (\<lambda>(X, y). (p \<bullet> X, y)) (\<theta><\<theta>'>)"
-apply(induct \<theta>')
-apply(auto)
-done
+ shows "\<theta><\<theta>'|p> = (\<theta><\<theta>'>)|p"
+ by (induct \<theta>')(auto)
lemma w2:
assumes "name |\<in>| dom \<theta>'"
shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"
using assms
apply(induct \<theta>')
-apply(auto)
-by (metis notin_empty_fset)
+apply(auto simp add: notin_empty_fset)
+done
lemma w3:
assumes "name |\<in>| dom \<theta>"
- shows "lookup \<theta> name = lookup (map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>) (p \<bullet> name)"
+ shows "lookup \<theta> name = lookup (\<theta>|p) (p \<bullet> name)"
using assms
apply(induct \<theta>)
-apply(auto)
-by (metis notin_empty_fset)
+apply(auto simp add: notin_empty_fset)
+done
lemma fresh_lookup:
fixes X Y::"name"
@@ -320,13 +260,13 @@
using assms
apply (induct \<theta>)
apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
-done
+ done
lemma test:
fixes \<theta> \<theta>'::"Subst"
and T::"ty"
assumes "(p \<bullet> atom ` fset (dom \<theta>')) \<sharp>* \<theta>" "supp All [dom \<theta>'].T \<sharp>* p"
- shows "\<theta><\<theta>'<T>> = \<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'><\<theta><p \<bullet> T>>"
+ shows "\<theta><\<theta>'<T>> = \<theta><\<theta>'|p><\<theta><p \<bullet> T>>"
using assms
apply(induct T rule: ty.induct)
defer
@@ -341,7 +281,7 @@
apply(simp add: w1)
apply(simp add: w2)
apply(subst w3[symmetric])
-apply(simp add:redundant3)
+apply(simp add: dom_subst)
apply(simp)
apply(perm_simp)
apply(rotate_tac 2)
@@ -354,18 +294,17 @@
apply(subst dom_fresh_ty)
apply(auto)[1]
apply(rule fresh_lookup)
-apply(simp add: redundant3)
-apply(simp add: dom_pi[symmetric])
+apply(simp add: dom_subst)
+apply(simp add: dom_pi)
apply(perm_simp)
apply(rotate_tac 2)
apply(drule_tac p="p" in permute_boolI)
apply(perm_simp)
apply(simp add: fresh_at_base)
apply (metis in_fset)
-apply(simp add: redundant3)
+apply(simp add: dom_subst)
apply(simp add: dom_pi[symmetric])
apply(perm_simp)
-apply metis
apply(subst supp_perm_eq)
apply(simp add: supp_at_base fresh_star_def)
apply (smt Diff_iff atom_eq_iff image_iff insertI1 notin_fset)
@@ -373,8 +312,8 @@
done
lemma
- shows "T \<prec>\<prec>\<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec>\<prec>\<prec> \<theta><S>"
-unfolding generalises3_def
+ shows "T \<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><S>"
+unfolding generalises_def
apply(erule exE)+
apply(erule conjE)+
apply(rule_tac t="S" and s="All [Xs].T'" in subst)
@@ -401,17 +340,18 @@
apply(subst substs.simps)
apply(perm_simp)
apply(simp)
-apply(rule_tac x="\<theta><map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>'>" in exI)
+apply(rule_tac x="\<theta><\<theta>'|p>" in exI)
apply(rule_tac x="p \<bullet> Xs" in exI)
apply(rule_tac x="\<theta><p \<bullet> T'>" in exI)
apply(rule conjI)
apply(simp)
apply(rule conjI)
defer
-apply(simp add: redundant3)
-apply(simp add: dom_pi[symmetric])
+apply(simp add: dom_subst)
+apply(simp add: dom_pi dom_eqvt[symmetric])
apply(rule_tac t="T" and s="\<theta>'<T'>" in subst)
apply(simp)
+apply(simp)
apply(rule test)
apply(perm_simp)
apply(rotate_tac 2)
@@ -420,5 +360,19 @@
apply(auto simp add: fresh_star_def)
done
+lemma
+ "T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> dom \<theta> = Xs)"
+apply(auto)
+defer
+unfolding generalises_def
+apply(auto)[1]
+apply(auto)[1]
+apply(drule sym)
+apply(simp add: Abs_eq_iff2)
+apply(simp add: alphas)
+apply(auto)
+apply(rule_tac x="map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>" in exI)
+apply(auto)
+oops
end
--- a/Nominal/Ex/TypeSchemes2.thy Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy Tue Jan 03 11:43:27 2012 +0000
@@ -265,7 +265,7 @@
apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
apply (erule subsetD)
apply (simp add: supp_eqvt)
- apply (metis le_eqvt permute_boolI)
+ apply (metis permute_pure subset_eqvt)
apply (rule perm_supp_eq)
apply (simp add: fresh_def fresh_star_def)
apply blast
@@ -307,7 +307,4 @@
apply auto
done
-
-
-
end
--- a/Nominal/Nominal2_Abs.thy Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Nominal2_Abs.thy Tue Jan 03 11:43:27 2012 +0000
@@ -365,7 +365,7 @@
then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
then have zb: "p \<bullet> as = p' \<bullet> as"
- apply(auto simp add: permute_set_eq)
+ apply(auto simp add: permute_set_def)
apply(rule_tac x="xa" in exI)
apply(simp)
done
@@ -800,7 +800,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
- have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms)
+ have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_set {b} y"
by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
also have "\<dots> = Abs_set {a} x" using ** by simp
@@ -809,7 +809,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
- also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_eq assms)
+ also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_set {b} y"
by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
finally have "Abs_set {a} x = Abs_set {b} y" .
@@ -824,7 +824,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
- have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms)
+ have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_res {b} y"
by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
also have "\<dots> = Abs_res {a} x" using ** by simp
@@ -833,7 +833,7 @@
moreover
{ assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
- also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_eq assms)
+ also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_def assms)
also have "\<dots> = Abs_res {b} y"
by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
finally have "Abs_res {a} x = Abs_res {b} y" .
--- a/Nominal/Nominal2_Base.thy Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Nominal2_Base.thy Tue Jan 03 11:43:27 2012 +0000
@@ -430,25 +430,33 @@
subsection {* Permutations for sets *}
+instantiation "set" :: (pt) pt
+begin
+
+definition
+ "p \<bullet> X = {p \<bullet> x | x. x \<in> X}"
+
+instance
+apply default
+apply (auto simp add: permute_set_def)
+done
+
+end
+
lemma permute_set_eq:
- fixes x::"'a::pt"
- shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
- unfolding permute_fun_def
- unfolding permute_bool_def
- apply(auto simp add: mem_def)
- apply(rule_tac x="- p \<bullet> x" in exI)
- apply(simp)
- done
+ shows "p \<bullet> X = {x. - p \<bullet> x \<in> X}"
+unfolding permute_set_def
+by (auto) (metis permute_minus_cancel(1))
lemma permute_set_eq_image:
shows "p \<bullet> X = permute p ` X"
- unfolding permute_set_eq by auto
+ unfolding permute_set_def by auto
lemma permute_set_eq_vimage:
shows "p \<bullet> X = permute (- p) -` X"
- unfolding permute_fun_def permute_bool_def
- unfolding vimage_def Collect_def mem_def ..
-
+ unfolding permute_set_eq vimage_def
+ by simp
+
lemma permute_finite [simp]:
shows "finite (p \<bullet> X) = finite X"
unfolding permute_set_eq_vimage
@@ -457,36 +465,36 @@
lemma swap_set_not_in:
assumes a: "a \<notin> S" "b \<notin> S"
shows "(a \<rightleftharpoons> b) \<bullet> S = S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma swap_set_in:
assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma swap_set_in_eq:
assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma swap_set_both_in:
assumes a: "a \<in> S" "b \<in> S"
shows "(a \<rightleftharpoons> b) \<bullet> S = S"
- unfolding permute_set_eq
+ unfolding permute_set_def
using a by (auto simp add: swap_atom)
lemma mem_permute_iff:
shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
- unfolding mem_def permute_fun_def permute_bool_def
- by simp
+ unfolding permute_set_def
+ by auto
lemma empty_eqvt:
shows "p \<bullet> {} = {}"
- unfolding empty_def Collect_def
- by (simp add: permute_fun_def permute_bool_def)
+ unfolding permute_set_def
+ by (simp)
lemma insert_eqvt:
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
@@ -665,6 +673,9 @@
instance "fun" :: (pure, pure) pure
by default (simp add: permute_fun_def permute_pure)
+instance set :: (pure) pure
+by default (simp add: permute_set_def permute_pure)
+
instance prod :: (pure, pure) pure
by default (induct_tac x, simp add: permute_pure)
@@ -879,12 +890,13 @@
lemma mem_eqvt [eqvt]:
shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
- unfolding mem_def
- by (rule permute_fun_app_eq)
+ unfolding permute_bool_def permute_set_def
+ by (auto)
lemma Collect_eqvt [eqvt]:
shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
- unfolding Collect_def permute_fun_def ..
+ unfolding permute_set_eq permute_fun_def
+ by (auto simp add: permute_bool_def)
lemma inter_eqvt [eqvt]:
shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
@@ -1871,7 +1883,7 @@
proof -
{ fix a b
have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
- unfolding permute_set_eq by force
+ unfolding permute_set_def by force
}
then show "(\<Union>x \<in> S. supp x) supports S"
unfolding supports_def
@@ -2491,7 +2503,7 @@
using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
have c: "(p \<bullet> a) \<sharp> c" using p1
unfolding fresh_star_def Ball_def
- by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
+ by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_def)
hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
qed
@@ -2506,7 +2518,7 @@
proof (induct)
case empty
have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
- by (simp add: permute_set_eq supp_perm)
+ by (simp add: permute_set_def supp_perm)
then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
next
case (insert a bs)