# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269625487 -3600
# Node ID 54becd55d83a46f9e192779c7611936db854cc24
# Parent  aacab5f67333e69fab9fef00f1e1cd75e401f596
simplification

diff -r aacab5f67333 -r 54becd55d83a Nominal/Abs.thy
--- a/Nominal/Abs.thy	Fri Mar 26 17:01:22 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 26 18:44:47 2010 +0100
@@ -117,33 +117,6 @@
   apply(rule_tac [!] x="p \<bullet> pa" in exI)
   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
-lemma alphas_abs_swap1:
-  assumes a1: "a \<notin> (supp x) - bs"
-  and     a2: "b \<notin> (supp x) - bs"
-  shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  and   "(bs, x) \<approx>abs_res ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  using a1 a2
-  unfolding alphas_abs
-  unfolding alphas
-  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
-  unfolding fresh_star_def fresh_def
-  unfolding swap_set_not_in[OF a1 a2] 
-  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
-
-lemma alphas_abs_swap2:
-  assumes a1: "a \<notin> (supp x) - (set bs)"
-  and     a2: "b \<notin> (supp x) - (set bs)"
-  shows "(bs, x) \<approx>abs_lst ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  using a1 a2
-  unfolding alphas_abs
-  unfolding alphas
-  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
-  unfolding fresh_star_def fresh_def
-  unfolding swap_set_not_in[OF a1 a2] 
-  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
-
 fun
   aux_set 
 where
@@ -227,10 +200,9 @@
   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"
-  apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
-  apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
-  apply(lifting prod.induct[where 'a="atom list" and 'b="'a"])
-  done
+  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"])
 
 instantiation abs_gen :: (pt) pt
 begin
@@ -317,10 +289,7 @@
   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)"
-  apply(lifting aux_set.simps)
-  apply(lifting aux_set.simps)
-  apply(lifting aux_list.simps)
-  done
+  by (lifting aux_set.simps aux_set.simps aux_list.simps)
 
 lemma aux_supp_eqvt[eqvt]:
   shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
@@ -342,21 +311,42 @@
   apply(simp_all add: eqvts_raw)
   done
 
+lemma abs_eq_iff:
+  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)"
+  apply(simp_all)
+  apply(lifting alphas_abs)
+  done
+
 lemma abs_swap1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
   shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
   and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
-  using a1 a2 
-  apply(lifting alphas_abs_swap1(1))
-  apply(lifting alphas_abs_swap1(2))
-  done
+  unfolding abs_eq_iff
+  unfolding alphas_abs
+  unfolding alphas
+  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
+  unfolding fresh_star_def fresh_def
+  unfolding swap_set_not_in[OF a1 a2] 
+  using a1 a2
+  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+     (auto simp add: supp_perm swap_atom)
 
 lemma abs_swap2:
   assumes a1: "a \<notin> (supp x) - (set bs)"
   and     a2: "b \<notin> (supp x) - (set bs)"
   shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
-  using a1 a2 by (lifting alphas_abs_swap2)
+  unfolding abs_eq_iff
+  unfolding alphas_abs
+  unfolding alphas
+  unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+  unfolding fresh_star_def fresh_def
+  unfolding swap_set_not_in[OF a1 a2]
+  using a1 a2
+  by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+     (auto simp add: supp_perm swap_atom)
 
 lemma abs_supports:
   shows "((supp x) - as) supports (Abs as x)"
@@ -430,14 +420,6 @@
   unfolding supp_abs
   by auto
 
-lemma abs_eq_iff:
-  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)"
-  apply(simp_all)
-  apply(lifting alphas_abs)
-  done
-
 
 section {* BELOW is stuff that may or may not be needed *}