Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Abs.thy
changeset 1673 e8cf0520c820
parent 1666 a99ae705b811
child 1675 d24f59f78a86
child 1686 7b3dd407f6b3 
--- a/Nominal/Abs.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -460,12 +460,16 @@
   shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
-lemma alpha_gen2:
+lemma alphas2:
   "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
   (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
   \<and> pi \<bullet> bs = cs)"
-by (simp add: alpha_gen)
-
+  "(bs, x1, x2) \<approx>res (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =
+  (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)"
+  "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) =
+  (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2
+  \<and> pi \<bullet> bsl = csl)"
+by (simp_all add: alphas)
 
 lemma alpha_gen_compose_sym:
   fixes pi
@@ -473,7 +477,7 @@
   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(simp add: alphas)
   apply(erule conjE)+
   apply(rule conjI)
   apply(simp add: fresh_star_def fresh_minus_perm)
@@ -485,6 +489,42 @@
   apply assumption
   done
 
+lemma alpha_res_compose_sym:
+  fixes pi
+  assumes b: "(aa, t) \<approx>res (\<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>res R f (- pi) (aa, t)"
+  using b apply -
+  apply(simp add: alphas)
+  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(rule a)
+  apply assumption
+  done
+
+lemma alpha_lst_compose_sym:
+  fixes pi
+  assumes b: "(aa, t) \<approx>lst (\<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>lst R f (- pi) (aa, t)"
+  using b apply -
+  apply(simp add: alphas)
+  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
+
+lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym
+
 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)"
@@ -492,7 +532,7 @@
   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(simp add: alphas)
   apply clarify
   apply (rule conjI)
   apply(simp add: fresh_star_def fresh_minus_perm)
@@ -506,6 +546,49 @@
   apply simp_all
   done
 
+lemma alpha_res_compose_sym2:
+  assumes a: "(aa, t1, t2) \<approx>res (\<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>res (\<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: alphas)
+  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 (rotate_tac -1)
+  apply (drule_tac pi="- pi" in r2)
+  apply simp
+  done
+
+lemma alpha_lst_compose_sym2:
+  assumes a: "(aa, t1, t2) \<approx>lst (\<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>lst (\<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: alphas)
+  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
+
+lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2
+
 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)"
@@ -513,7 +596,7 @@
   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)
+  apply(simp add: alphas)
   apply(erule conjE)+
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa" in spec)
@@ -526,6 +609,47 @@
   apply(simp)
   done
 
+lemma alpha_res_compose_trans:
+  fixes pi pia
+  assumes b: "(aa, t) \<approx>res (\<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>res 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>res R f (pia + pi) (ac, sa)"
+  using b c apply -
+  apply(simp add: alphas)
+  apply(erule conjE)+
+  apply(simp add: fresh_star_plus)
+  apply(drule_tac x="- pia \<bullet> sa" in spec)
+  apply(drule mp)
+  apply(drule_tac pi="- pia" in a)
+  apply(simp)
+  apply(rotate_tac 6)
+  apply(drule_tac pi="pia" in a)
+  apply(simp)
+  done
+
+lemma alpha_lst_compose_trans:
+  fixes pi pia
+  assumes b: "(aa, t) \<approx>lst (\<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>lst 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>lst R f (pia + pi) (ac, sa)"
+  using b c apply -
+  apply(simp add: alphas)
+  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
+
+lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans
+
 lemma alpha_gen_compose_trans2:
   fixes pi pia
   assumes b: "(aa, (t1, t2)) \<approx>gen
@@ -538,8 +662,8 @@
   shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
     (pia + pi) (ac, (sa1, sa2))"
   using b c apply -
-  apply(simp add: alpha_gen2)
-  apply(simp add: alpha_gen)
+  apply(simp add: alphas2)
+  apply(simp add: alphas)
   apply(erule conjE)+
   apply(simp add: fresh_star_plus)
   apply(drule_tac x="- pia \<bullet> sa1" in spec)
@@ -560,6 +684,76 @@
   apply(simp)
   done
 
+lemma alpha_res_compose_trans2:
+  fixes pi pia
+  assumes b: "(aa, (t1, t2)) \<approx>res
+    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
+    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
+  and c: "(ab, (ta1, ta2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    pia (ac, (sa1, sa2))"
+  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 "(aa, (t1, t2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    (pia + pi) (ac, (sa1, sa2))"
+  using b c apply -
+  apply(simp add: alphas2)
+  apply(simp add: alphas)
+  apply(erule conjE)+
+  apply(simp add: fresh_star_plus)
+  apply(drule_tac x="- pia \<bullet> sa1" in spec)
+  apply(drule mp)
+  apply(rotate_tac 5)
+  apply(drule_tac pi="- pia" in r1)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r1)
+  apply(simp)
+  apply(drule_tac x="- pia \<bullet> sa2" in spec)
+  apply(drule mp)
+  apply(rotate_tac 6)
+  apply(drule_tac pi="- pia" in r2)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r2)
+  apply(simp)
+  done
+
+lemma alpha_lst_compose_trans2:
+  fixes pi pia
+  assumes b: "(aa, (t1, t2)) \<approx>lst
+    (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z))
+    (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))"
+  and c: "(ab, (ta1, ta2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    pia (ac, (sa1, sa2))"
+  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 "(aa, (t1, t2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a)
+    (pia + pi) (ac, (sa1, sa2))"
+  using b c apply -
+  apply(simp add: alphas2)
+  apply(simp add: alphas)
+  apply(erule conjE)+
+  apply(simp add: fresh_star_plus)
+  apply(drule_tac x="- pia \<bullet> sa1" in spec)
+  apply(drule mp)
+  apply(rotate_tac 5)
+  apply(drule_tac pi="- pia" in r1)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r1)
+  apply(simp)
+  apply(drule_tac x="- pia \<bullet> sa2" in spec)
+  apply(drule mp)
+  apply(rotate_tac 6)
+  apply(drule_tac pi="- pia" in r2)
+  apply(simp)
+  apply(rotate_tac -1)
+  apply(drule_tac pi="pia" in r2)
+  apply(simp)
+  done
+
+lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2
+
 lemma alpha_gen_refl:
   assumes a: "R x x"
   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
@@ -571,36 +765,22 @@
   by (simp_all add: fresh_zero_perm)
 
 lemma alpha_gen_sym:
-  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
-  and     b: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
+  assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
   shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
   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
-  apply (erule_tac [1] conjE)+
-  apply (erule_tac [2] conjE)+
-  apply (erule_tac [3] conjE)+
   using a
-  apply (simp_all add: fresh_minus_perm)
-  apply (rotate_tac [!] -1)
-  apply (drule_tac [!] p="-p" in b)
-  apply (simp_all)
-  apply (metis permute_minus_cancel(2))
-  apply (metis permute_minus_cancel(2))
-  done
+  by (auto simp add:  fresh_minus_perm)
+
 lemma alpha_gen_trans:
-  assumes a: "(\<forall>c. R y c \<longrightarrow> R (p \<bullet> x) c)"
-  and b: "R (p \<bullet> x) y"
-  and c: "R (q \<bullet> y) z"
-  and d: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)"
+  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)"
-  unfolding alphas
-  unfolding fresh_star_def
-  apply (simp_all add: fresh_plus_perm)
-  apply (metis a c d permute_minus_cancel(2))+
-  done
+  using a
+  unfolding alphas fresh_star_def
+  by (simp_all add: fresh_plus_perm)
 
 lemma alpha_gen_eqvt:
   assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
nominal2