--- a/Nominal/Abs.thy	Sat Mar 27 08:42:07 2010 +0100
+++ b/Nominal/Abs.thy	Sun Mar 28 22:54:38 2010 +0200
@@ -120,37 +120,6 @@
   apply(rule_tac [!] x="p \<bullet> pa" in exI)
   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
-fun
-  aux_set 
-where
-  "aux_set (bs, x) = (supp x) - bs"
-
-fun
-  aux_list
-where
-  "aux_list (cs, x) = (supp x) - (set cs)"
-
-lemma aux_abs_lemma:
-  assumes a: "(bs, x) \<approx>abs (cs, y)" 
-  shows "aux_set (bs, x) = aux_set (cs, y)"
-  using a
-  by (induct rule: alpha_abs.induct)
-     (simp add: alphas_abs alphas)
-
-lemma aux_abs_res_lemma:
-  assumes a: "(bs, x) \<approx>abs_res (cs, y)" 
-  shows "aux_set (bs, x) = aux_set (cs, y)"
-  using a
-  by (induct rule: alpha_abs_res.induct)
-     (simp add: alphas_abs alphas)
- 
-lemma aux_abs_list_lemma:
-  assumes a: "(bs, x) \<approx>abs_lst (cs, y)" 
-  shows "aux_list (bs, x) = aux_list (cs, y)"
-  using a
-  by (induct rule: alpha_abs_lst.induct)
-     (simp add: alphas_abs alphas)
-
 quotient_type 
     'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
@@ -188,24 +157,13 @@
   unfolding fun_rel_def
   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
-lemma [quot_respect]:
-  shows "(alpha_abs ===> op=) aux_set aux_set"
-  and   "(alpha_abs_res ===> op=) aux_set aux_set"
-  and   "(alpha_abs_lst ===> op=) aux_list aux_list"
-  unfolding fun_rel_def
-  apply(rule_tac [!] allI)
-  apply(rule_tac [!] allI)
-  apply(case_tac [!] x, case_tac [!] y)
-  apply(rule_tac [!] impI)
-  by (simp_all only: aux_abs_lemma aux_abs_res_lemma aux_abs_list_lemma)
-
-lemma abs_inducts:
-  shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1"
-  and   "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2"
-  and   "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3"
-  by (lifting prod.induct[where 'a="atom set" and 'b="'a"]
-              prod.induct[where 'a="atom set" and 'b="'a"]
-              prod.induct[where 'a="atom list" and 'b="'a"])
+lemma abs_exhausts:
+  shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
+  and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
+  and   "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
+  by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
+              prod.exhaust[where 'a="atom set" and 'b="'a"]
+              prod.exhaust[where 'a="atom list" and 'b="'a"])
 
 lemma abs_eq_iff:
   shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
@@ -230,7 +188,7 @@
 
 instance
   apply(default)
-  apply(induct_tac [!] x rule: abs_inducts(1))
+  apply(case_tac [!] x rule: abs_exhausts(1))
   apply(simp_all)
   done
 
@@ -251,7 +209,7 @@
 
 instance
   apply(default)
-  apply(induct_tac [!] x rule: abs_inducts(2))
+  apply(case_tac [!] x rule: abs_exhausts(2))
   apply(simp_all)
   done
 
@@ -272,7 +230,7 @@
 
 instance
   apply(default)
-  apply(induct_tac [!] x rule: abs_inducts(3))
+  apply(case_tac [!] x rule: abs_exhausts(3))
   apply(simp_all)
   done
 
@@ -317,37 +275,52 @@
   unfolding permute_abs
   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
-quotient_definition
-  "supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set"
-is
-  "aux_set"
+function
+  supp_gen  :: "('a::pt) abs_gen \<Rightarrow> atom set"
+where
+  "supp_gen (Abs as x) = supp x - as"
+apply(case_tac x rule: abs_exhausts(1))
+apply(simp)
+apply(simp add: abs_eq_iff alphas_abs alphas)
+done
 
-quotient_definition
-  "supp_res :: ('a::pt) abs_res \<Rightarrow> atom set"
-is
-  "aux_set"
+termination supp_gen 
+  by (auto intro!: local.termination)
 
-quotient_definition
-  "supp_lst :: ('a::pt) abs_lst \<Rightarrow> atom set"
-is
-  "aux_list"
+function
+  supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
+where
+  "supp_res (Abs_res as x) = supp x - as"
+apply(case_tac x rule: abs_exhausts(2))
+apply(simp)
+apply(simp add: abs_eq_iff alphas_abs alphas)
+done
+
+termination supp_res 
+  by (auto intro!: local.termination)
 
-lemma aux_supps:
-  shows "supp_gen (Abs bs x) = (supp x) - bs"
-  and   "supp_res (Abs_res bs x) = (supp x) - bs"
-  and   "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
-  by (lifting aux_set.simps aux_set.simps aux_list.simps)
+function
+  supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
+where
+  "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
+apply(case_tac x rule: abs_exhausts(3))
+apply(simp)
+apply(simp add: abs_eq_iff alphas_abs alphas)
+done
 
-lemma aux_supp_eqvt[eqvt]:
+termination supp_lst 
+  by (auto intro!: local.termination)
+
+lemma [eqvt]:
   shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
-  apply(induct_tac x rule: abs_inducts(1))
-  apply(simp add: aux_supps supp_eqvt Diff_eqvt)
-  apply(induct_tac y rule: abs_inducts(2))
-  apply(simp add: aux_supps supp_eqvt Diff_eqvt)
-  apply(induct_tac z rule: abs_inducts(3))
-  apply(simp add: aux_supps supp_eqvt Diff_eqvt set_eqvt)
+  apply(case_tac x rule: abs_exhausts(1))
+  apply(simp add: supp_eqvt Diff_eqvt)
+  apply(case_tac y rule: abs_exhausts(2))
+  apply(simp add: supp_eqvt Diff_eqvt)
+  apply(case_tac z rule: abs_exhausts(3))
+  apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
   done
 
 lemma aux_fresh:
@@ -364,7 +337,7 @@
   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
   and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
   unfolding supp_conv_fresh
-  apply(auto dest!: aux_fresh simp add: aux_supps)
+  apply(auto dest!: aux_fresh)
   apply(simp_all add: fresh_def supp_finite_atom_set a)
   done
 
@@ -397,19 +370,19 @@
 
 instance abs_gen :: (fs) fs
   apply(default)
-  apply(induct_tac x rule: abs_inducts(1))
+  apply(case_tac x rule: abs_exhausts(1))
   apply(simp add: supp_abs finite_supp)
   done
 
 instance abs_res :: (fs) fs
   apply(default)
-  apply(induct_tac x rule: abs_inducts(2))
+  apply(case_tac x rule: abs_exhausts(2))
   apply(simp add: supp_abs finite_supp)
   done
 
 instance abs_lst :: (fs) fs
   apply(default)
-  apply(induct_tac x rule: abs_inducts(3))
+  apply(case_tac x rule: abs_exhausts(3))
   apply(simp add: supp_abs finite_supp)
   done
 
@@ -422,7 +395,6 @@
   unfolding supp_abs
   by auto
 
-
 section {* BELOW is stuff that may or may not be needed *}
 
 (* support of concrete atom sets *)