--- a/Nominal/Nominal2_Abs.thy Tue Aug 28 16:47:26 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy Tue Aug 28 16:48:07 2012 +0100
@@ -12,30 +12,30 @@
alpha_set
where
alpha_set[simp del]:
- "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ "alpha_set (bs, x) R f p (cs, y) \<longleftrightarrow>
f x - bs = f y - cs \<and>
- (f x - bs) \<sharp>* pi \<and>
- R (pi \<bullet> x) y \<and>
- pi \<bullet> bs = cs"
+ (f x - bs) \<sharp>* p \<and>
+ R (p \<bullet> x) y \<and>
+ p \<bullet> bs = cs"
fun
alpha_res
where
alpha_res[simp del]:
- "alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ "alpha_res (bs, x) R f p (cs, y) \<longleftrightarrow>
f x - bs = f y - cs \<and>
- (f x - bs) \<sharp>* pi \<and>
- R (pi \<bullet> x) y"
+ (f x - bs) \<sharp>* p \<and>
+ R (p \<bullet> x) y"
fun
alpha_lst
where
alpha_lst[simp del]:
- "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
+ "alpha_lst (bs, x) R f p (cs, y) \<longleftrightarrow>
f x - set bs = f y - set cs \<and>
- (f x - set bs) \<sharp>* pi \<and>
- R (pi \<bullet> x) y \<and>
- pi \<bullet> bs = cs"
+ (f x - set bs) \<sharp>* p \<and>
+ R (p \<bullet> x) y \<and>
+ p \<bullet> bs = cs"
lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
@@ -66,8 +66,7 @@
unfolding Diff_eqvt[symmetric]
unfolding eq_eqvt[symmetric]
unfolding fresh_star_eqvt[symmetric]
- by (auto simp add: permute_bool_def)
-
+ by (auto simp only: permute_bool_def)
section {* Equivalence *}
@@ -88,7 +87,7 @@
and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
unfolding alphas fresh_star_def
using a
- by (auto simp add: fresh_minus_perm)
+ by (auto simp add: fresh_minus_perm)
lemma alpha_trans:
assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
@@ -108,12 +107,7 @@
apply(auto intro!: alpha_sym)
apply(drule_tac [!] a)
apply(rule_tac [!] p="p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel b)
-apply(assumption)
-apply(perm_simp add: permute_minus_cancel b)
-apply(assumption)
-apply(perm_simp add: permute_minus_cancel b)
-apply(assumption)
+apply(simp_all add: b permute_self)
done
lemma alpha_set_trans_eqvt:
@@ -122,18 +116,13 @@
and d: "q \<bullet> R = R"
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
-apply(rule alpha_trans)
-defer
-apply(rule a)
-apply(rule b)
+apply(rule alpha_trans(1)[OF _ a b])
apply(drule c)
apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel d)
-apply(assumption)
+apply(simp add: d permute_self)
apply(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
-apply(perm_simp add: permute_minus_cancel d)
-apply(simp add: permute_eqvt[symmetric])
+apply(simp add: d permute_self permute_eqvt[symmetric])
done
lemma alpha_res_trans_eqvt:
@@ -142,18 +131,13 @@
and d: "q \<bullet> R = R"
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
-apply(rule alpha_trans)
-defer
-apply(rule a)
-apply(rule b)
+apply(rule alpha_trans(2)[OF _ a b])
apply(drule c)
apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel d)
-apply(assumption)
+apply(simp add: d permute_self)
apply(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
-apply(perm_simp add: permute_minus_cancel d)
-apply(simp add: permute_eqvt[symmetric])
+apply(simp add: d permute_self permute_eqvt[symmetric])
done
lemma alpha_lst_trans_eqvt:
@@ -162,18 +146,13 @@
and d: "q \<bullet> R = R"
and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
-apply(rule alpha_trans)
-defer
-apply(rule a)
-apply(rule b)
+apply(rule alpha_trans(3)[OF _ a b])
apply(drule c)
apply(rule_tac p="q" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel d)
-apply(assumption)
+apply(simp add: d permute_self)
apply(rotate_tac -1)
apply(drule_tac p="q" in permute_boolI)
-apply(perm_simp add: permute_minus_cancel d)
-apply(simp add: permute_eqvt[symmetric])
+apply(simp add: d permute_self permute_eqvt[symmetric])
done
lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
@@ -457,17 +436,15 @@
section {* Quotient types *}
-(* FIXME: The three could be defined together, but due to bugs
- introduced by the lifting package it doesn't work anymore *)
quotient_type
'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
- apply(rule_tac [!] equivpI)
+ apply(rule equivpI)
unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
quotient_type
'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
- apply(rule_tac [!] equivpI)
+ apply(rule equivpI)
unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
@@ -537,7 +514,7 @@
apply (simp add: fresh_star_zero)
using asm by blast
-lemma Abs_exhausts:
+lemma Abs_exhausts[cases type]:
shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1"
and "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2"
and "(\<And>bs (x::'a::pt). y3 = [bs]lst. x \<Longrightarrow> P3) \<Longrightarrow> P3"
@@ -545,7 +522,6 @@
prod.exhaust[where 'a="atom set" and 'b="'a"]
prod.exhaust[where 'a="atom list" and 'b="'a"])
-
instantiation abs_set :: (pt) pt
begin
@@ -562,7 +538,7 @@
instance
apply(default)
- apply(case_tac [!] x rule: Abs_exhausts(1))
+ apply(case_tac [!] x)
apply(simp_all)
done
@@ -584,7 +560,7 @@
instance
apply(default)
- apply(case_tac [!] x rule: Abs_exhausts(2))
+ apply(case_tac [!] x)
apply(simp_all)
done
@@ -606,7 +582,7 @@
instance
apply(default)
- apply(case_tac [!] x rule: Abs_exhausts(3))
+ apply(case_tac [!] x)
apply(simp_all)
done
@@ -651,51 +627,37 @@
by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
function
- supp_set :: "('a::pt) abs_set \<Rightarrow> atom set"
+ supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" and
+ supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" and
+ supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
where
"supp_set ([as]set. x) = supp x - as"
-apply(case_tac x rule: Abs_exhausts(1))
+| "supp_res ([as]res. x) = supp x - as"
+| "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
+apply(simp_all add: Abs_eq_iff alphas_abs alphas)
+apply(case_tac x)
+apply(case_tac a)
apply(simp)
-apply(simp add: Abs_eq_iff alphas_abs alphas)
+apply(case_tac b)
+apply(case_tac a)
+apply(simp)
+apply(case_tac ba)
+apply(simp)
done
-termination supp_set
- by lexicographic_order
-
-function
- supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
-where
- "supp_res ([as]res. x) = supp x - as"
-apply(case_tac x rule: Abs_exhausts(2))
-apply(simp)
-apply(simp add: Abs_eq_iff alphas_abs alphas)
-done
-
-termination supp_res
- by lexicographic_order
-
-function
- supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
-where
- "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
-apply(case_tac x rule: Abs_exhausts(3))
-apply(simp)
-apply(simp add: Abs_eq_iff alphas_abs alphas)
-done
-
-termination supp_lst
+termination
by lexicographic_order
lemma supp_funs_eqvt[eqvt]:
shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
- apply(case_tac x rule: Abs_exhausts(1))
- apply(simp add: supp_eqvt Diff_eqvt)
- apply(case_tac y rule: Abs_exhausts(2))
- apply(simp add: supp_eqvt Diff_eqvt)
- apply(case_tac z rule: Abs_exhausts(3))
- apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
+ apply(case_tac x)
+ apply(simp)
+ apply(case_tac y)
+ apply(simp)
+ apply(case_tac z)
+ apply(simp)
done
lemma Abs_fresh_aux:
@@ -739,19 +701,19 @@
instance abs_set :: (fs) fs
apply(default)
- apply(case_tac x rule: Abs_exhausts(1))
+ apply(case_tac x)
apply(simp add: supp_Abs finite_supp)
done
instance abs_res :: (fs) fs
apply(default)
- apply(case_tac x rule: Abs_exhausts(2))
+ apply(case_tac x)
apply(simp add: supp_Abs finite_supp)
done
instance abs_lst :: (fs) fs
apply(default)
- apply(case_tac x rule: Abs_exhausts(3))
+ apply(case_tac x)
apply(simp add: supp_Abs finite_supp)
done
@@ -791,15 +753,14 @@
section {* Abstractions of single atoms *}
+
lemma Abs1_eq:
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
+by (auto simp add: supp_perm_singleton fresh_star_def fresh_zero_perm)
lemma Abs1_eq_iff_fresh:
fixes x y::"'a::fs"
@@ -850,29 +811,25 @@
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_iff_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_iff_fresh(1))
-apply(auto simp add: fresh_Pair)[1]
-apply(assumption)
+apply(auto simp add: fresh_Pair)[2]
apply(simp add: Abs1_eq_iff_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_iff_fresh(2))
-apply(auto simp add: fresh_Pair)[1]
-apply(assumption)
+apply(auto simp add: fresh_Pair)[2]
apply(simp add: Abs1_eq_iff_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_iff_fresh(3))
-apply(auto simp add: fresh_Pair)[1]
-apply(assumption)
+apply(auto simp add: fresh_Pair)[2]
done
lemma Abs1_eq_iff:
@@ -886,24 +843,24 @@
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 {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"
+ { assume *: "a \<noteq> b" and **: "[{atom a}]set. x = [{atom b}]set. y"
+ have #: "atom a \<sharp> [{atom b}]set. y" by (simp add: **[symmetric] Abs_fresh_iff)
+ have "[{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp)
+ also have "\<dots> = [{atom b}]set. y"
by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
- also have "\<dots> = Abs_set {atom a} x" using ** by simp
+ also have "\<dots> = [{atom a}]set. 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 \<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"
+ have "[{atom a}]set. x = [{atom a}]set. ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp
+ also have "\<dots> = (a \<leftrightarrow> b) \<bullet> ([{atom b}]set. y)" by (simp add: permute_set_def assms)
+ also have "\<dots> = [{atom b}]set. 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" .
+ finally have "[{atom a}]set. x = [{atom b}]set. y" .
}
ultimately
- 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)"
+ show "[{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)"
by blast
next
{ assume "a = b"
@@ -1130,5 +1087,10 @@
by (auto intro!: ext)
+
+
+
+
+
end