--- a/Nominal/Abs.thy	Fri Mar 19 21:04:24 2010 +0100
+++ b/Nominal/Abs.thy	Sat Mar 20 02:46:07 2010 +0100
@@ -1,19 +1,12 @@
 theory Abs
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" "Nominal2_FSet"
+imports "Nominal2_Atoms" 
+        "Nominal2_Eqvt" 
+        "Nominal2_Supp" 
+        "Nominal2_FSet"
+        "../Quotient" 
+        "../Quotient_Product" 
 begin
 
-lemma permute_boolI:
-  fixes P::"bool"
-  shows "p \<bullet> P \<Longrightarrow> P"
-apply(simp add: permute_bool_def)
-done
-
-lemma permute_boolE:
-  fixes P::"bool"
-  shows "P \<Longrightarrow> p \<bullet> P"
-apply(simp add: permute_bool_def)
-done
-
 fun
   alpha_gen 
 where
@@ -24,26 +17,59 @@
      R (pi \<bullet> x) y \<and>
      pi \<bullet> bs = cs"
 
-notation
-  alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)
+fun
+  alpha_res
+where
+  alpha_res[simp del]:
+  "alpha_res (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+     f x - bs = f y - cs \<and> 
+     (f x - bs) \<sharp>* pi \<and> 
+     R (pi \<bullet> x) y"
 
-lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
-  by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
+fun
+  alpha_lst
+where
+  alpha_lst[simp del]:
+  "alpha_lst (bs, x) R f pi (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"
+
+lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
+
+notation
+  alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
+  alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
+  alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
+
+(* monos *)
+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"
+  and   "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
+  by (case_tac [!] bs, case_tac [!] cs) 
+     (auto simp add: le_fun_def le_bool_def alphas)
 
 lemma alpha_gen_refl:
   assumes a: "R x x"
   shows "(bs, x) \<approx>gen R f 0 (bs, x)"
-  using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)
+  and   "(bs, x) \<approx>res R f 0 (bs, x)"
+  and   "(cs, x) \<approx>lst R f 0 (cs, x)"
+  using a 
+  unfolding alphas
+  unfolding fresh_star_def
+  by (simp_all add: fresh_zero_perm)
 
 lemma alpha_gen_sym:
-  assumes a: "(bs, x) \<approx>gen R f p (cs, y)"
-  and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
-  shows "(cs, y) \<approx>gen R f (- p) (bs, x)"
-  using a b 
-  apply (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)
-  apply(clarify)
-  apply(simp)
-  done
+  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)"
+  using a
+  unfolding alphas
+  unfolding fresh_star_def
+  by (auto simp add:  fresh_minus_perm)
 
 lemma alpha_gen_trans:
   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"
@@ -155,8 +181,6 @@
 notation
   alpha_abs ("_ \<approx>abs _")
 
-
-
 lemma alpha_abs_swap:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
@@ -209,18 +233,18 @@
   apply(simp_all)
   (* refl *)
   apply(clarify)
-  apply(rule exI)
+  apply(rule_tac x="0" in exI)
   apply(rule alpha_gen_refl)
   apply(simp)
   (* symm *)
   apply(clarify)
-  apply(rule exI)
+  apply(rule_tac x="- p" in exI)
   apply(rule alpha_gen_sym)
+  apply(clarsimp)
   apply(assumption)
-  apply(clarsimp)
   (* trans *)
   apply(clarify)
-  apply(rule exI)
+  apply(rule_tac x="pa + p" in exI)
   apply(rule alpha_gen_trans)
   apply(assumption)
   apply(assumption)
@@ -618,7 +642,7 @@
   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"
 using a
 apply(auto)
-apply(rule_tac p="- p" in permute_boolI)
+apply(rule_tac p="- p" in permute_boolE)
 apply(simp add: mem_eqvt supp_eqvt)
 done
 
@@ -634,7 +658,7 @@
 apply(rule supp_supports)
 apply(auto)
 apply(rotate_tac 1)
-apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
+apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
 apply(simp add: mem_eqvt supp_eqvt)
 done
 
@@ -724,7 +748,7 @@
 apply(assumption)
 apply(drule alpha_equal)
 apply(simp)
-apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)
+apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)
 apply(simp add: fresh_eqvt)
 apply(simp add: fresh_def)
 done
@@ -782,10 +806,6 @@
   \<and> pi \<bullet> bs = cs)"
 by (simp add: alpha_gen)
 
-(* maybe should be added to Infinite.thy *)
-lemma infinite_Un:
-  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
-  by simp
 
 end