diff -r 542b36e1c390 -r a987b5acadc8 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Thu Jan 28 23:36:58 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Thu Jan 28 23:47:02 2010 +0100
@@ -55,16 +55,16 @@
 
 end  
 
-inductive
+fun
   alpha_abs :: "('a::pt) ABS_raw \<Rightarrow> 'a ABS_raw \<Rightarrow> bool"
 where
-  "\<lbrakk>\<exists>pi. (supp x) - as = (supp y) - bs \<and>  ((supp x) - as) \<sharp>* pi \<and> pi \<bullet> x = y\<rbrakk> 
-   \<Longrightarrow> alpha_abs (Abs_raw as x) (Abs_raw bs y)"
+  "alpha_abs (Abs_raw as x) (Abs_raw bs y) =
+    (\<exists>pi. (supp x) - as = (supp y) - bs \<and>  ((supp x) - as) \<sharp>* pi \<and> pi \<bullet> x = y)" 
 
 lemma alpha_reflp:
   shows "alpha_abs ab ab"
 apply(induct ab)
-apply(rule alpha_abs.intros)
+apply(simp)
 apply(rule_tac x="0" in exI)
 apply(simp add: fresh_star_def fresh_zero_perm)
 done
@@ -73,9 +73,9 @@
   assumes a: "alpha_abs ab1 ab2"
   shows "alpha_abs ab2 ab1"
 using a
-apply(erule_tac alpha_abs.cases)
+apply(induct rule: alpha_abs.induct)
+apply(simp)
 apply(clarify)
-apply(rule alpha_abs.intros)
 apply(rule_tac x="- pi" in exI)
 apply(auto)
 apply(auto simp add: fresh_star_def)
@@ -87,10 +87,10 @@
   and     a2: "alpha_abs ab2 ab3"
   shows "alpha_abs ab1 ab3"
 using a1 a2
-apply(erule_tac alpha_abs.cases)
-apply(erule_tac alpha_abs.cases)
+apply(induct rule: alpha_abs.induct)
+apply(induct rule: alpha_abs.induct)
+apply(simp)
 apply(clarify)
-apply(rule alpha_abs.intros)
 apply(rule_tac x="pia + pi" in exI)
 apply(simp)
 apply(auto simp add: fresh_star_def)
@@ -103,14 +103,13 @@
   assumes a: "alpha_abs ab1 ab2"
   shows "alpha_abs (p \<bullet> ab1) (p \<bullet> ab2)"
 using a
-apply(erule_tac alpha_abs.cases)
-apply(clarify)
+apply(induct ab1 ab2 rule: alpha_abs.induct)
 apply(simp)
-apply(rule alpha_abs.intros)
-apply(rule_tac x="p \<bullet> pi" in exI)
+apply(clarify)
 apply(rule conjI)
 apply(simp add: supp_eqvt[symmetric])
 apply(simp add: Diff_eqvt[symmetric])
+apply(rule_tac x="p \<bullet> pi" in exI)
 apply(rule conjI)
 apply(simp add: supp_eqvt[symmetric])
 apply(simp add: Diff_eqvt[symmetric])
@@ -122,7 +121,7 @@
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
   shows "alpha_abs (Abs_raw bs x) (Abs_raw ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"
-apply(rule alpha_abs.intros)
+unfolding alpha_abs.simps
 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
 apply(rule_tac conjI)
 apply(simp add: supp_eqvt[symmetric])
@@ -150,7 +149,7 @@
   assumes a: "alpha_abs x y" 
   shows "s_test x = s_test y"
 using a
-apply(induct)
+apply(induct rule: alpha_abs.induct)
 apply(simp)
 done
   
@@ -168,7 +167,7 @@
 
 lemma [quot_respect]:
   shows "((op =) ===> (op =) ===> alpha_abs) Abs_raw Abs_raw"
-apply(auto)
+apply(auto simp del: alpha_abs.simps)
 apply(rule alpha_reflp)
 done
 
@@ -310,7 +309,7 @@
 apply(simp add: finite_supp)
 done
 
-lemma fresh_abs1:
+lemma fresh_abs:
   fixes x::"'a::fs"
   shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))"
 apply(simp add: fresh_def)
@@ -318,5 +317,10 @@
 apply(auto)
 done
 
+lemma abs_eq:
+  shows "(Abs as x) = (Abs bs y) \<longleftrightarrow> (\<exists>pi. supp x - as = supp y - bs \<and> (supp x - as) \<sharp>* pi \<and> pi \<bullet> x = y)"
+apply(lifting alpha_abs.simps(1))
 done
 
+done
+