--- a/Nominal/Abs.thy Sat Mar 20 02:46:07 2010 +0100
+++ b/Nominal/Abs.thy Sat Mar 20 04:51:26 2010 +0100
@@ -72,111 +72,34 @@
by (auto simp add: fresh_minus_perm)
lemma alpha_gen_trans:
- assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
- and b: "(cs, y) \<approx>gen R f p2 (ds, z)"
- and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"
- shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"
- using a b c using supp_plus_perm
- apply(simp add: alpha_gen fresh_star_def fresh_def)
- apply(blast)
- done
+ assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
+ shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+ and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
+ and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
+ using a
+ unfolding alphas
+ unfolding fresh_star_def
+ by (simp_all add: fresh_plus_perm)
lemma alpha_gen_eqvt:
- assumes a: "(bs, x) \<approx>gen R f q (cs, y)"
- and b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
- and c: "p \<bullet> (f x) = f (p \<bullet> x)"
- and d: "p \<bullet> (f y) = f (p \<bullet> y)"
- shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
- using a b
- apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])
- apply(simp add: permute_eqvt[symmetric])
- apply(simp add: fresh_star_permute_iff)
- apply(clarsimp)
- done
-
-lemma alpha_gen_compose_sym:
- fixes pi
- assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
- using b apply -
- apply(simp add: alpha_gen)
- apply(erule conjE)+
- apply(rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
- apply simp
- apply(clarify)
- apply(simp)
- apply(rule a)
- apply assumption
- done
-
-lemma alpha_gen_compose_sym2:
- assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
- (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
- and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
- and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
- shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
+ assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
+ and b: "p \<bullet> (f x) = f (p \<bullet> x)"
+ and c: "p \<bullet> (f y) = f (p \<bullet> y)"
+ shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)"
+ unfolding alphas
+ unfolding set_eqvt[symmetric]
+ unfolding b[symmetric] c[symmetric]
+ unfolding Diff_eqvt[symmetric]
+ unfolding permute_eqvt[symmetric]
using a
- apply(simp add: alpha_gen)
- apply clarify
- apply (rule conjI)
- apply(simp add: fresh_star_def fresh_minus_perm)
- apply (rule conjI)
- apply (rotate_tac 3)
- apply (drule_tac pi="- pi" in r1)
- apply simp
- apply (rule conjI)
- apply (rotate_tac -1)
- apply (drule_tac pi="- pi" in r2)
- apply simp_all
- done
-
-lemma alpha_gen_compose_trans:
- fixes pi pia
- assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
- and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
- and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
- using b c apply -
- apply(simp add: alpha_gen.simps)
- apply(erule conjE)+
- apply(simp add: fresh_star_plus)
- apply(drule_tac x="- pia \<bullet> sa" in spec)
- apply(drule mp)
- apply(rotate_tac 5)
- apply(drule_tac pi="- pia" in a)
- apply(simp)
- apply(rotate_tac 7)
- apply(drule_tac pi="pia" in a)
- apply(simp)
- done
-
-lemma alpha_gen_compose_eqvt:
- fixes pia
- assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
- and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
- and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
- shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
- using b
- apply -
- apply(simp add: alpha_gen.simps)
- apply(erule conjE)+
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
- apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
- apply(rule conjI)
- apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
- apply(subst permute_eqvt[symmetric])
- apply(simp)
- sorry
+ by (auto simp add: fresh_star_permute_iff)
fun
alpha_abs
where
- "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+ "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
notation
alpha_abs ("_ \<approx>abs _")
@@ -185,17 +108,15 @@
assumes a1: "a \<notin> (supp x) - bs"
and a2: "b \<notin> (supp x) - bs"
shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
- apply(simp)
- apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
- apply(simp add: alpha_gen)
- apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])
- apply(simp add: swap_set_not_in[OF a1 a2])
- apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
using a1 a2
- apply(simp add: fresh_star_def fresh_def)
- apply(blast)
- apply(simp add: supp_swap)
- done
+ unfolding Diff_iff
+ unfolding alpha_abs.simps
+ unfolding alphas
+ unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ unfolding fresh_star_def fresh_def
+ unfolding swap_set_not_in[OF a1 a2]
+ by (rule_tac x="(a \<rightleftharpoons> b)" in exI)
+ (auto simp add: supp_perm swap_atom)
lemma alpha_gen_swap_fun:
assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"
@@ -213,12 +134,12 @@
apply(simp add: supp_swap)
done
-
fun
supp_abs_fun
where
"supp_abs_fun (bs, x) = (supp x) - bs"
+
lemma supp_abs_fun_lemma:
assumes a: "x \<approx>abs y"
shows "supp_abs_fun x = supp_abs_fun y"
@@ -227,7 +148,8 @@
apply(simp add: alpha_gen)
done
-quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"
+
+quotient_type 'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
apply(rule equivpI)
unfolding reflp_def symp_def transp_def
apply(simp_all)
@@ -246,13 +168,11 @@
apply(clarify)
apply(rule_tac x="pa + p" in exI)
apply(rule alpha_gen_trans)
- apply(assumption)
- apply(assumption)
- apply(simp)
+ apply(auto)
done
quotient_definition
- "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
+ "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
is
"Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
@@ -269,7 +189,6 @@
apply(clarsimp)
apply(rule exI)
apply(rule alpha_gen_eqvt)
- apply(assumption)
apply(simp_all add: supp_eqvt)
done
@@ -287,17 +206,19 @@
lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
thm abs_induct abs_induct2
-instantiation abs :: (pt) pt
+instantiation abs_gen :: (pt) pt
begin
quotient_definition
- "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"
+ "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
is
"permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
+(* ??? has to be 'a \<dots> 'b does not work *)
lemma permute_ABS [simp]:
- fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *)
+ fixes x::"'a::pt"
shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
+ thm permute_prod.simps
by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])
instance
@@ -309,7 +230,7 @@
end
quotient_definition
- "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
+ "supp_Abs_fun :: ('a::pt) abs_gen \<Rightarrow> atom \<Rightarrow> bool"
is
"supp_abs_fun"
@@ -379,7 +300,7 @@
apply(simp add: finite_supp)
done
-instance abs :: (fs) fs
+instance abs_gen :: (fs) fs
apply(default)
apply(induct_tac x rule: abs_induct)
apply(simp add: supp_Abs)
@@ -765,12 +686,6 @@
apply(simp)
done
-fun
- distinct_perms
-where
- "distinct_perms [] = True"
-| "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
-
(* support of concrete atom sets *)
lemma supp_atom_image:
@@ -807,5 +722,84 @@
by (simp add: alpha_gen)
+lemma alpha_gen_compose_sym:
+ fixes pi
+ assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+ and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"
+ using b apply -
+ apply(simp add: alpha_gen)
+ apply(erule conjE)+
+ apply(rule conjI)
+ apply(simp add: fresh_star_def fresh_minus_perm)
+ apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
+ apply simp
+ apply(clarify)
+ apply(simp)
+ apply(rule a)
+ apply assumption
+ done
+
+lemma alpha_gen_compose_sym2:
+ assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22).
+ (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)"
+ and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)"
+ and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)"
+ shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)"
+ using a
+ apply(simp add: alpha_gen)
+ apply clarify
+ apply (rule conjI)
+ apply(simp add: fresh_star_def fresh_minus_perm)
+ apply (rule conjI)
+ apply (rotate_tac 3)
+ apply (drule_tac pi="- pi" in r1)
+ apply simp
+ apply (rule conjI)
+ apply (rotate_tac -1)
+ apply (drule_tac pi="- pi" in r2)
+ apply simp_all
+ done
+
+lemma alpha_gen_compose_trans:
+ fixes pi pia
+ assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+ and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"
+ and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"
+ using b c apply -
+ apply(simp add: alpha_gen.simps)
+ apply(erule conjE)+
+ apply(simp add: fresh_star_plus)
+ apply(drule_tac x="- pia \<bullet> sa" in spec)
+ apply(drule mp)
+ apply(rotate_tac 5)
+ apply(drule_tac pi="- pia" in a)
+ apply(simp)
+ apply(rotate_tac 7)
+ apply(drule_tac pi="pia" in a)
+ apply(simp)
+ done
+
+lemma alpha_gen_compose_eqvt:
+ fixes pia
+ assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
+ and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
+ and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
+ shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"
+ using b
+ apply -
+ apply(simp add: alpha_gen.simps)
+ apply(erule conjE)+
+ apply(rule conjI)
+ apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
+ apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
+ apply(rule conjI)
+ apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
+ apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])
+ apply(subst permute_eqvt[symmetric])
+ apply(simp)
+ sorry
+
end