# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271859924 -7200
# Node ID 2389de5ba00a95cfc3f4e4879ade43f3b3307fbd
# Parent  7480845016373c03a51b6df4033201d9f374e799# Parent  94ed05fb090e9d0b31a759e29d64602ed85d6c4a
merged

diff -r 94ed05fb090e -r 2389de5ba00a Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 13:39:34 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 16:25:24 2010 +0200
@@ -433,6 +433,13 @@
   qed
 qed
 
+lemma perm_struct_induct2[case_names zero swap]:
+  assumes zero: "P 0"
+  assumes swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+  shows "P p"
+by (rule_tac S="supp p" in perm_struct_induct)
+   (auto intro: zero swap)
+
 lemma perm_subset_induct [consumes 1, case_names zero swap plus]:
   assumes S: "supp p \<subseteq> S"
   assumes zero: "P 0"
diff -r 94ed05fb090e -r 2389de5ba00a Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Apr 21 13:39:34 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 21 16:25:24 2010 +0200
@@ -397,150 +397,6 @@
 
 section {* BELOW is stuff that may or may not be needed *}
 
-lemma 
-  fixes t1 s1::"'a::fs"
-  and   t2 s2::"'b::fs"
-  shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma 
-  fixes t1 s1::"'a::fs"
-  and   t2 s2::"'b::fs"
-  shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2)"
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE)
-apply(simp add: supp_Pair)
-apply(simp add: Un_Diff)
-apply(simp add: fresh_star_union)
-apply(erule conjE)+
-apply(rule conjI)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-apply(rule trans)
-apply(rule sym)
-apply(rule_tac p="p" in supp_perm_eq)
-apply(simp add: supp_abs)
-apply(simp)
-done
-
-lemma fresh_star_eq:
-  assumes a: "as \<sharp>* p"
-  shows "\<forall>a \<in> as. p \<bullet> a = a"
-using a by (simp add: fresh_star_def fresh_def supp_perm)
-
-lemma fresh_star_set_eq:
-  assumes a: "as \<sharp>* p"
-  shows "p \<bullet> as = as"
-using a 
-apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)
-apply(auto)
-by (metis permute_atom_def)
-
-lemma 
-  fixes t1 s1::"'a::fs"
-  and   t2 s2::"'b::fs"
-  shows "Abs as t1 = Abs bs s1 \<longrightarrow> Abs (as \<union> cs) t1 = Abs (bs \<union> cs) s1"
-apply(subst abs_eq_iff)
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE | erule conjE)+
-apply(rule_tac x="p" in exI)
-apply(simp)
-apply(rule conjI)
-apply(auto)[1]
-apply(rule conjI)
-apply(auto)[1]
-apply(simp add: fresh_star_def)
-apply(auto)[1]
-apply(simp add: union_eqvt)
-oops
-
-
-lemma 
-  fixes t1 s1::"'a::fs"
-  and   t2 s2::"'b::fs"
-  shows "(Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"
-apply(subst abs_eq_iff)
-apply(subst abs_eq_iff)
-apply(subst alphas_abs)
-apply(subst alphas_abs)
-apply(subst alphas)
-apply(subst alphas)
-apply(rule impI)
-apply(erule exE | erule conjE)+
-apply(simp add: abs_eq_iff)
-apply(simp add: alphas_abs)
-apply(simp add: alphas)
-apply(rule conjI)
-apply(simp add: supp_Pair Un_Diff)
-oops
-
-
-
-(* support of concrete atom sets *)
-
-lemma
-  shows "Abs as t = Abs (supp t \<inter> as) t"
-apply(simp add: abs_eq_iff)
-apply(simp add: alphas_abs)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas)
-apply(auto)
-oops
-
-lemma
-  assumes "finite S"
-  shows "\<exists>q. supp q \<subseteq> S \<union> p \<bullet> S \<and> (\<forall>a \<in> S. q \<bullet> a = p \<bullet> a)"
-using assms
-apply(induct)
-apply(rule_tac x="0" in exI)
-apply(simp add: supp_zero_perm)
-apply(auto)
-apply(simp add: insert_eqvt)
-apply(rule_tac x="((p \<bullet> x) \<rightleftharpoons> x) + q" in exI)
-apply(rule conjI)
-apply(rule subset_trans)
-apply(rule supp_plus_perm)
-apply(simp add: supp_swap)
-apply(auto)[1]
-apply(simp)
-apply(rule conjI)
-apply(case_tac "q \<bullet> x = x")
-apply(simp)
-apply(simp add: supp_perm)
-apply(case_tac "x \<in> p \<bullet> F")
-sorry
-
 
 lemma supp_atom_image:
   fixes as::"'a::at_base set"