
diff -r 841b7e34e70a -r fe25a3ffeb14 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/Abs.thy	Tue Jul 27 14:37:59 2010 +0200
@@ -43,7 +43,8 @@
   alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
   alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
 
-(* monos *)
+section {* Mono *}
+
 lemma [mono]: 
   shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
   and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
@@ -51,8 +52,9 @@
   by (case_tac [!] bs, case_tac [!] cs) 
      (auto simp add: le_fun_def le_bool_def alphas)
 
-(* equivariance *)
-lemma alpha_gen_eqvt[eqvt]:
+section {* Equivariance *}
+
+lemma alpha_eqvt[eqvt]:
   shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> 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 (p \<bullet> R) (p \<bullet> 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 (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
@@ -63,8 +65,10 @@
   unfolding Diff_eqvt[symmetric]
   by (auto simp add: permute_bool_def fresh_star_permute_iff)
 
-(* equivalence *)
-lemma alpha_gen_refl:
+
+section {* Equivalence *}
+
+lemma alpha_refl:
   assumes a: "R x x"
   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
   and   "(bs, x) \<approx>res R f 0 (bs, x)"
@@ -74,7 +78,7 @@
   unfolding fresh_star_def
   by (simp_all add: fresh_zero_perm)
 
-lemma alpha_gen_sym:
+lemma alpha_sym:
   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)"
@@ -83,13 +87,22 @@
   using a
   by (auto simp add:  fresh_minus_perm)
 
-lemma alpha_gen_sym_eqvt:
+lemma alpha_trans:
+  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 fresh_star_def
+  by (simp_all add: fresh_plus_perm)
+
+lemma alpha_sym_eqvt:
   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 
   and     b: "p \<bullet> R = R"
   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)"
-apply(auto intro!: alpha_gen_sym)
+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)
@@ -100,23 +113,13 @@
 apply(assumption)
 done
 
-lemma alpha_gen_trans:
-  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 fresh_star_def
-  by (simp_all add: fresh_plus_perm)
-
-
 lemma alpha_gen_trans_eqvt:
   assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
   and     a: "(bs, x) \<approx>gen R f p (cs, y)" 
   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>gen R f (q + p) (ds, z)"
-apply(rule alpha_gen_trans)
+apply(rule alpha_trans)
 defer
 apply(rule a)
 apply(rule b)
@@ -136,7 +139,7 @@
   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_gen_trans)
+apply(rule alpha_trans)
 defer
 apply(rule a)
 apply(rule b)
@@ -156,7 +159,7 @@
   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_gen_trans)
+apply(rule alpha_trans)
 defer
 apply(rule a)
 apply(rule b)
@@ -172,12 +175,6 @@
 
 lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
-lemma test:
-  shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
-  and   "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
-  and   "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
-  by (simp_all add: alphas)
-
 
 section {* General Abstractions *}
 
@@ -206,6 +203,7 @@
 
 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
 
+
 lemma alphas_abs_refl:
   shows "(bs, x) \<approx>abs (bs, x)"
   and   "(bs, x) \<approx>abs_res (bs, x)"
@@ -284,7 +282,7 @@
   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
   unfolding fun_rel_def
-  by (auto intro: alphas_abs_refl simp only:)
+  by (auto intro: alphas_abs_refl)
 
 lemma [quot_respect]:
   shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
@@ -305,8 +303,7 @@
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
-  unfolding alphas_abs
-  by (lifting alphas_abs)
+  unfolding alphas_abs by (lifting alphas_abs)
 
 instantiation abs_gen :: (pt) pt
 begin
@@ -373,6 +370,7 @@
 
 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
 
+
 lemma abs_swap1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
@@ -405,7 +403,7 @@
 lemma abs_supports:
   shows "((supp x) - as) supports (Abs as x)"
   and   "((supp x) - as) supports (Abs_res as x)"
-  and   "((supp x) - (set bs)) supports (Abs_lst bs x)"
+  and   "((supp x) - set bs) supports (Abs_lst bs x)"
   unfolding supports_def
   unfolding permute_abs
   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
@@ -525,6 +523,54 @@
   unfolding supp_abs
   by auto
 
+fun
+  prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
+where
+  "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y"
+
+definition 
+  prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+where
+ "prod_alpha = prod_rel"
+
+
+lemma [quot_respect]:
+  shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  by auto
+
+lemma [quot_preserve]:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
+lemma [mono]: 
+  shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+  unfolding prod_alpha_def
+  by auto
+
+lemma [eqvt]: 
+  shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  unfolding prod_alpha_def
+  unfolding prod_rel.simps
+  by (perm_simp) (rule refl)
+
+lemma [eqvt]: 
+  shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+  unfolding prod_fv.simps
+  by (perm_simp) (rule refl)
+
+
+
+
+
+
+
+
+
+
+
+
 section {* BELOW is stuff that may or may not be needed *}
 
 lemma supp_atom_image:
@@ -579,97 +625,6 @@
      R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)"
 by (simp add: alphas)
 
-lemma alpha_gen_simpler:
-  assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
-  and fin_fv: "finite (f x)"
-  and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
-  shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
-     (f x - bs) \<sharp>* pi \<and>
-     R (pi \<bullet> x) y \<and>
-     pi \<bullet> bs = cs"
-  apply rule
-  unfolding alpha_gen
-  apply clarify
-  apply (erule conjE)+
-  apply (simp)
-  apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
-  apply (rule sym)
-  apply simp
-  apply (rule supp_perm_eq)
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (rule fin_fv)
-  apply (assumption)
-  apply (simp add: eqvts fv_eqvt)
-  apply (subst fv_rsp)
-  apply assumption
-  apply (simp)
-  done
-
-lemma alpha_lst_simpler:
-  assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
-  and fin_fv: "finite (f x)"
-  and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
-  shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
-     (f x - set bs) \<sharp>* pi \<and>
-     R (pi \<bullet> x) y \<and>
-     pi \<bullet> bs = cs"
-  apply rule
-  unfolding alpha_lst
-  apply clarify
-  apply (erule conjE)+
-  apply (simp)
-  apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
-  apply (rule sym)
-  apply simp
-  apply (rule supp_perm_eq)
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (rule fin_fv)
-  apply (assumption)
-  apply (simp add: eqvts fv_eqvt)
-  apply (subst fv_rsp)
-  apply assumption
-  apply (simp)
-  done
-
-fun
-  prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
-where
-  "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
-
-definition 
-  prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
-where
- "prod_alpha = prod_rel"
-
-
-lemma [quot_respect]:
-  shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
-  by auto
-
-lemma [quot_preserve]:
-  assumes q1: "Quotient R1 abs1 rep1"
-  and     q2: "Quotient R2 abs2 rep2"
-  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
-
-lemma [mono]: 
-  shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
-  unfolding prod_alpha_def
-  by auto
-
-lemma [eqvt]: 
-  shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
-  unfolding prod_alpha_def
-  unfolding prod_rel.simps
-  by (perm_simp) (rule refl)
-
-lemma [eqvt]: 
-  shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
-  unfolding prod_fv.simps
-  by (perm_simp) (rule refl)
-
 
 end
 




