--- a/Nominal/Nominal2_Abs.thy Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy Thu Jul 12 10:11:32 2012 +0100
@@ -792,103 +792,175 @@
section {* Abstractions of single atoms *}
lemma Abs1_eq:
- fixes x::"'a::fs"
- shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"
- and "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y"
- and "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y"
+ fixes x y::"'a::fs"
+ shows "[{atom a}]set. x = [{atom a}]set. y \<longleftrightarrow> x = y"
+ and "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y"
+ and "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y"
unfolding Abs_eq_iff2 alphas
apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)
apply(blast)+
done
+lemma Abs1_eq_fresh:
+ fixes x y::"'a::fs"
+ and a b c::"'b::at"
+ assumes "atom c \<sharp> (a, b, x, y)"
+ shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+ and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+ and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+proof -
+ have "[{atom a}]set. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]set. x)"
+ by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+ then have "[{atom a}]set. x = [{atom c}]set. ((a \<leftrightarrow> c) \<bullet> x)" by simp
+ moreover
+ have "[{atom b}]set. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]set. y)"
+ by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+ then have "[{atom b}]set. y = [{atom c}]set. ((b \<leftrightarrow> c) \<bullet> y)" by simp
+ ultimately
+ show "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+ by (simp add: Abs1_eq)
+next
+ have "[{atom a}]res. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]res. x)"
+ by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+ then have "[{atom a}]res. x = [{atom c}]res. ((a \<leftrightarrow> c) \<bullet> x)" by simp
+ moreover
+ have "[{atom b}]res. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]res. y)"
+ by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+ then have "[{atom b}]res. y = [{atom c}]res. ((b \<leftrightarrow> c) \<bullet> y)" by simp
+ ultimately
+ show "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+ by (simp add: Abs1_eq)
+next
+ have "[[atom a]]lst. x = (a \<leftrightarrow> c) \<bullet> ([[atom a]]lst. x)"
+ by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+ then have "[[atom a]]lst. x = [[atom c]]lst. ((a \<leftrightarrow> c) \<bullet> x)" by simp
+ moreover
+ have "[[atom b]]lst. y = (b \<leftrightarrow> c) \<bullet> ([[atom b]]lst. y)"
+ by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms)
+ then have "[[atom b]]lst. y = [[atom c]]lst. ((b \<leftrightarrow> c) \<bullet> y)" by simp
+ ultimately
+ show "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y"
+ by (simp add: Abs1_eq)
+qed
+
+lemma Abs1_eq_all:
+ fixes x y::"'a::fs"
+ and z::"'c::fs"
+ and a b::"'b::at"
+ shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+ and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+ and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+apply -
+apply(auto)
+apply(simp add: Abs1_eq_fresh(1)[symmetric])
+apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
+apply(drule_tac x="aa" in spec)
+apply(simp)
+apply(subst Abs1_eq_fresh(1))
+apply(auto simp add: fresh_Pair)[1]
+apply(assumption)
+apply(simp add: Abs1_eq_fresh(2)[symmetric])
+apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
+apply(drule_tac x="aa" in spec)
+apply(simp)
+apply(subst Abs1_eq_fresh(2))
+apply(auto simp add: fresh_Pair)[1]
+apply(assumption)
+apply(simp add: Abs1_eq_fresh(3)[symmetric])
+apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
+apply(drule_tac x="aa" in spec)
+apply(simp)
+apply(subst Abs1_eq_fresh(3))
+apply(auto simp add: fresh_Pair)[1]
+apply(assumption)
+done
+
lemma Abs1_eq_iff:
- fixes x::"'a::fs"
- assumes "sort_of a = sort_of b"
- and "sort_of c = sort_of d"
- shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
- and "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
- and "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+ fixes x y::"'a::fs"
+ and a b::"'b::at"
+ shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
+ and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
+ and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
proof -
{ assume "a = b"
- then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
+ then have "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
}
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_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
- finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+ { assume *: "a \<noteq> b" and **: "Abs_set {atom a} x = Abs_set {atom b} y"
+ have #: "atom a \<sharp> Abs_set {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+ have "Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_set {atom b} y)" by (simp)
+ also have "\<dots> = Abs_set {atom b} y"
+ by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+ also have "\<dots> = Abs_set {atom a} x" using ** by simp
+ finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
}
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_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" .
+ { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
+ have "Abs_set {atom a} x = Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+ also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_set {atom b} y" by (simp add: permute_set_def assms)
+ also have "\<dots> = Abs_set {atom b} y"
+ by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+ finally have "Abs_set {atom a} x = Abs_set {atom b} y" .
}
ultimately
- show "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+ show "Abs_set {atom a} x = Abs_set {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
by blast
next
{ assume "a = b"
- then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
+ then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
}
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_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
- finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+ { assume *: "a \<noteq> b" and **: "Abs_res {atom a} x = Abs_res {atom b} y"
+ have #: "atom a \<sharp> Abs_res {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+ have "Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_res {atom b} y)" by (simp add: assms)
+ also have "\<dots> = Abs_res {atom b} y"
+ by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+ also have "\<dots> = Abs_res {atom a} x" using ** by simp
+ finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
}
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_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" .
+ { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
+ have "Abs_res {atom a} x = Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+ also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_res {atom b} y" by (simp add: permute_set_def assms)
+ also have "\<dots> = Abs_res {atom b} y"
+ by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+ finally have "Abs_res {atom a} x = Abs_res {atom b} y" .
}
ultimately
- show "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+ show "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
by blast
next
- { assume "c = d"
- then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" by (simp add: Abs1_eq)
+ { assume "a = b"
+ then have "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
}
moreover
- { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y"
- have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff)
- have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms)
- also have "\<dots> = Abs_lst [d] y"
- by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
- also have "\<dots> = Abs_lst [c] x" using ** by simp
- finally have "c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+ { assume *: "a \<noteq> b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y"
+ have #: "atom a \<sharp> Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff)
+ have "Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_lst [atom b] y)" by (simp add: assms)
+ also have "\<dots> = Abs_lst [atom b] y"
+ by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+ also have "\<dots> = Abs_lst [atom a] x" using ** by simp
+ finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
}
moreover
- { assume *: "c \<noteq> d" and **: "x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y"
- have "Abs_lst [c] x = Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y)" using ** by simp
- also have "\<dots> = (c \<rightleftharpoons> d) \<bullet> Abs_lst [d] y" by (simp add: assms)
- also have "\<dots> = Abs_lst [d] y"
- by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
- finally have "Abs_lst [c] x = Abs_lst [d] y" .
+ { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y"
+ have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+ also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_lst [atom b] y" by (simp add: assms)
+ also have "\<dots> = Abs_lst [atom b] y"
+ by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+ finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" .
}
ultimately
- show "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+ show "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)"
by blast
qed
lemma Abs1_eq_iff':
fixes x::"'a::fs"
- assumes "sort_of a = sort_of b"
- and "sort_of c = sort_of d"
- shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
- and "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
- and "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> (d \<rightleftharpoons> c) \<bullet> x = y \<and> d \<sharp> x)"
+ and a b::"'b::at"
+ shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
+ and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
+ and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)