# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283552611 -28800
# Node ID 7b1470b559365effbf9bc0f1c8b99f1bcdf2080a
# Parent  67b3933c3190c0f727f3803aed3378286814818f
moved a proof to Abs

diff -r 67b3933c3190 -r 7b1470b55936 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Sep 04 06:10:04 2010 +0800
+++ b/Nominal/Abs.thy	Sat Sep 04 06:23:31 2010 +0800
@@ -461,7 +461,7 @@
   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
   by (rule_tac [!] fresh_fun_eqvt_app)
-     (simp_all add: eqvts_raw)
+     (simp_all only: eqvts_raw)
 
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
@@ -523,6 +523,15 @@
   unfolding supp_abs
   by auto
 
+lemma Abs_eq_iff:
+  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+  by (lifting alphas_abs)
+
+
+section {* Infrastructure for building tuples of relations and functions *}
+
 fun
   prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
 where
@@ -560,16 +569,5 @@
   by (perm_simp) (rule refl)
 
 
-(* Below seems to be not needed *)
-
-(*
-lemma Abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
-  by (lifting alphas_abs)
-*)
-
-
 end
 
diff -r 67b3933c3190 -r 7b1470b55936 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sat Sep 04 06:10:04 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sat Sep 04 06:23:31 2010 +0800
@@ -34,12 +34,6 @@
 thm single_let.supports
 thm single_let.fsupp
 
-lemma Abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
-  by (lifting alphas_abs)
-
 lemma test2:
   assumes "fv_trm t = supp t" 
   shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)"
diff -r 67b3933c3190 -r 7b1470b55936 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Sat Sep 04 06:10:04 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Sat Sep 04 06:23:31 2010 +0800
@@ -14,15 +14,39 @@
 and tys =
   All xs::"name fset" ty::"ty" bind (res) xs in ty
 
+thm ty_tys.distinct
+thm ty_tys.induct
+thm ty_tys.exhaust
+thm ty_tys.fv_defs
+thm ty_tys.bn_defs
+thm ty_tys.perm_simps
+thm ty_tys.eq_iff
+thm ty_tys.fv_bn_eqvt
+thm ty_tys.size_eqvt
+thm ty_tys.supports
+thm ty_tys.fsupp
 
 nominal_datatype ty2 =
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-
 nominal_datatype tys2 =
   All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 
+thm tys2.distinct
+thm tys2.induct
+thm tys2.exhaust
+thm tys2.fv_defs
+thm tys2.bn_defs
+thm tys2.perm_simps
+thm tys2.eq_iff
+thm tys2.fv_bn_eqvt
+thm tys2.size_eqvt
+thm tys2.supports
+thm tys2.fsupp
+
+
+text {* *}
 
 (*
 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *}
diff -r 67b3933c3190 -r 7b1470b55936 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Sat Sep 04 06:10:04 2010 +0800
+++ b/Nominal/Nominal2_FSet.thy	Sat Sep 04 06:23:31 2010 +0800
@@ -9,11 +9,8 @@
   shows "(op = ===> list_eq ===> list_eq) permute permute"
   apply(simp)
   apply(clarify)
-  apply(simp add: eqvts[symmetric])  
-  apply(subst permute_minus_cancel(1)[symmetric, of "xb"])
-  apply(subst mem_eqvt[symmetric])
-  apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
-  apply(subst mem_eqvt[symmetric])
+  apply(rule_tac p="-x" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
   apply(simp)
   done