# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271849974 -7200
# Node ID 94ed05fb090e9d0b31a759e29d64602ed85d6c4a
# Parent  e41b7046be2cad9782b73affdd74933878f1fc79# Parent  ec45c81d1ca6102cb9d81416c26579dfca3c97ac
merge

diff -r e41b7046be2c -r 94ed05fb090e Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 13:38:37 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Wed Apr 21 13:39:34 2010 +0200
@@ -392,15 +392,16 @@
 
 text {* Induction principle for permutations *}
 
-lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]:
+
+lemma perm_struct_induct[consumes 1, case_names zero swap]:
   assumes S: "supp p \<subseteq> S"
   assumes zero: "P 0"
-  assumes swap: "\<And>a b. supp (a \<rightleftharpoons> b) \<subseteq> S \<Longrightarrow> P (a \<rightleftharpoons> b)"
-  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  assumes swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> 
+    \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
   shows "P p"
 proof -
   have "finite (supp p)" by (simp add: finite_supp)
-  then show ?thesis using S
+  then show "P p" using S
   proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
     case (psubset p)
     then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
@@ -412,23 +413,20 @@
     moreover
     { assume "supp p \<noteq> {}"
       then obtain a where a0: "a \<in> supp p" by blast
-      then have a1: "supp (- p \<bullet> a \<rightleftharpoons> a) \<subseteq> S" using as
+      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a" using as
 	by (auto simp add: supp_atom supp_perm swap_atom)
-      let ?q = "p + (- p \<bullet> a \<rightleftharpoons> a)"
+      let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
       have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
       moreover
       have "a \<notin> supp ?q" by (simp add: supp_perm)
       then have "supp ?q \<noteq> supp p" using a0 by auto
-      ultimately have "supp ?q \<subset> supp p" using as by auto
+      ultimately have "supp ?q \<subset> supp p" using a2 by auto
       then have "P ?q" using ih by simp
       moreover
       have "supp ?q \<subseteq> S" using as a2 by simp
-      moreover
-      have "P (- p \<bullet> a \<rightleftharpoons> a)" using a1 swap by simp
-      ultimately 
-      have "P (?q + (- p \<bullet> a \<rightleftharpoons> a))" using a1 plus by simp
+      ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 
       moreover 
-      have "p = ?q + (- p \<bullet> a \<rightleftharpoons> a)" by (simp add: expand_perm_eq)
+      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
       ultimately have "P p" by simp
     }
     ultimately show "P p" by blast
@@ -441,9 +439,9 @@
   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
   assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
   shows "P p"
-apply(rule perm_subset_induct_aux[OF S])
-apply(auto simp add: zero swap plus supp_swap split: if_splits)
-done
+using S
+by (induct p rule: perm_struct_induct)
+   (auto intro: zero plus swap simp add: supp_swap)
 
 lemma supp_perm_eq:
   assumes "(supp x) \<sharp>* p"
@@ -452,6 +450,23 @@
   from assms have "supp p \<subseteq> {a. a \<sharp> x}"
     unfolding supp_perm fresh_star_def fresh_def by auto
   then show "p \<bullet> x = x"
+  proof (induct p rule: perm_struct_induct)
+    case zero
+    show "0 \<bullet> x = x" by simp
+  next
+    case (swap p a b)
+    then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all
+    then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+  qed
+qed
+
+lemma supp_perm_eq_test:
+  assumes "(supp x) \<sharp>* p"
+  shows "p \<bullet> x = x"
+proof -
+  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
+    unfolding supp_perm fresh_star_def fresh_def by auto
+  then show "p \<bullet> x = x"
   proof (induct p rule: perm_subset_induct)
     case zero
     show "0 \<bullet> x = x" by simp
diff -r e41b7046be2c -r 94ed05fb090e Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Apr 21 13:38:37 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 21 13:39:34 2010 +0200
@@ -465,7 +465,30 @@
 lemma 
   fixes t1 s1::"'a::fs"
   and   t2 s2::"'b::fs"
-  assumes asm: "finite as"
+  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)
@@ -486,6 +509,39 @@
 
 (* 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"
   shows "supp (atom ` as) = supp as"