# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1295453470 -3600
# Node ID e003e5e36bae3f59ee69710d56c3c3e565a9dae8
# Parent  494b859bfc162aeed28752f7b342a255a9c02912
added Minimal file to test things

diff -r 494b859bfc16 -r e003e5e36bae Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Jan 19 07:06:47 2011 +0100
+++ b/Nominal/Nominal2.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -653,7 +653,7 @@
 
   val bclauses' = complete dt_strs bclauses
 in
-  timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy)
+  nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy
 end
 *}
 
@@ -705,10 +705,11 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
+(*
 ML {*
 trace := true
 *}
-
+*)
 
 end
 
diff -r 494b859bfc16 -r e003e5e36bae Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Wed Jan 19 07:06:47 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -491,6 +491,7 @@
               prod.exhaust[where 'a="atom set" and 'b="'a"]
               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
+
 instantiation abs_set :: (pt) pt
 begin
 
@@ -723,6 +724,101 @@
   unfolding fresh_star_def
   by(auto simp add: Abs_fresh_iff)
 
+lemma Abs1_eq:
+  fixes x::"'a::fs"
+  shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y"
+  and   "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y"
+  and   "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y"
+unfolding Abs_eq_iff2 alphas
+apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm)
+apply(blast)+
+done
+
+
+lemma Abs1_eq_iff:
+  fixes x::"'a::fs"
+  assumes "sort_of a = sort_of b"
+  and     "sort_of c = sort_of d"
+  shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+  and   "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+  and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+proof -
+  { assume "a = b"
+    then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)"
+      by (simp add: Abs1_eq)
+  }
+  moreover
+  { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
+    have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+    have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms)
+    also have "\<dots> = Abs_set {b} y"
+      by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+    also have "\<dots> = Abs_set {a} x" using ** by simp
+    finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+  }
+  moreover 
+  { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
+    have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
+    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_eq assms)
+    also have "\<dots> = Abs_set {b} y"
+      by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+    finally have "Abs_set {a} x = Abs_set {b} y" .
+  }
+  ultimately 
+  show "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+    by blast
+next
+  { assume "a = b"
+    then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)"
+      by (simp add: Abs1_eq)
+  }
+  moreover
+  { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
+    have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
+    have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms)
+    also have "\<dots> = Abs_res {b} y"
+      by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+    also have "\<dots> = Abs_res {a} x" using ** by simp
+    finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+  }
+  moreover 
+  { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
+    have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
+    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_eq assms)
+    also have "\<dots> = Abs_res {b} y"
+      by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+    finally have "Abs_res {a} x = Abs_res {b} y" .
+  }
+  ultimately 
+  show "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"
+    by blast
+next
+  { assume "c = d"
+    then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)"
+      by (simp add: Abs1_eq)
+  }
+  moreover
+  { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y"
+    have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff)
+    have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms)
+    also have "\<dots> = Abs_lst [d] y"
+      by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
+    also have "\<dots> = Abs_lst [c] x" using ** by simp
+    finally have "c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff)
+  }
+  moreover 
+  { assume *: "c \<noteq> d" and **: "x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y"
+    have "Abs_lst [c] x = Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y)" using ** by simp
+    also have "\<dots> = (c \<rightleftharpoons> d) \<bullet> Abs_lst [d] y" by (simp add: assms)
+    also have "\<dots> = Abs_lst [d] y"
+      by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
+    finally have "Abs_lst [c] x = Abs_lst [d] y" .
+  }
+  ultimately 
+  show "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
+    by blast
+qed
+
 
 subsection {* Renaming of bodies of abstractions *}
 
diff -r 494b859bfc16 -r e003e5e36bae Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed Jan 19 07:06:47 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -225,9 +225,10 @@
   by (rule Rep_perm_ext) (simp add: Rep_perm_simps)
 
 lemma swap_cancel:
-  "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
-  by (rule Rep_perm_ext) 
-     (simp add: Rep_perm_simps fun_eq_iff)
+  shows "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
+  and   "(a \<rightleftharpoons> b) + (b \<rightleftharpoons> a) = 0"
+  by (rule_tac [!] Rep_perm_ext) 
+     (simp_all add: Rep_perm_simps fun_eq_iff)
 
 lemma swap_self [simp]:
   "(a \<rightleftharpoons> a) = 0"
@@ -235,7 +236,7 @@
 
 lemma minus_swap [simp]:
   "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)"
-  by (rule minus_unique [OF swap_cancel])
+  by (rule minus_unique [OF swap_cancel(1)])
 
 lemma swap_commute:
   "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)"
@@ -1396,6 +1397,14 @@
   unfolding fresh_def
   by (simp add: supp_finite_atom_set[OF assms])
 
+lemma fresh_minus_atom_set:
+  fixes S::"atom set"
+  assumes "finite S"
+  shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)"
+  unfolding fresh_def
+  by (auto simp add: supp_finite_atom_set assms)
+
+
 lemma Union_fresh:
   shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
   unfolding Union_image_eq[symmetric]
@@ -1610,6 +1619,15 @@
 apply(simp add: supp_finite_atom_set fin fresh)
 done
 
+lemma fresh_star_atom_set_conv:
+  fixes p::"perm"
+  assumes fresh: "as \<sharp>* bs"
+  and     fin: "finite as" "finite bs"
+  shows "bs \<sharp>* as"
+using fresh
+unfolding fresh_star_def fresh_def
+by (auto simp add: supp_finite_atom_set fin)
+
 
 lemma fresh_star_Pair:
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
@@ -1772,6 +1790,32 @@
 by (rule_tac S="supp p" in perm_struct_induct2)
    (auto intro: zero swap plus)
 
+lemma supp_perm_singleton:
+  fixes p::"perm"
+  shows "supp p \<subseteq> {b} \<longleftrightarrow> p = 0"
+proof -
+  { assume "supp p \<subseteq> {b}"
+    then have "p = 0"
+      by (induct p rule: perm_struct_induct) (simp_all)
+  }
+  then show "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" by (auto simp add: supp_zero_perm)
+qed
+
+lemma supp_perm_pair:
+  fixes p::"perm"
+  shows "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)"
+proof -
+  { assume "supp p \<subseteq> {a, b}"
+    then have "p = 0 \<or> p = (b \<rightleftharpoons> a)"
+      apply (induct p rule: perm_struct_induct) 
+      apply (auto simp add: swap_cancel supp_zero_perm supp_swap)
+      apply (simp add: swap_commute)
+      done
+  }
+  then show "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" 
+    by (auto simp add: supp_zero_perm supp_swap split: if_splits)
+qed
+
 lemma supp_perm_eq:
   assumes "(supp x) \<sharp>* p"
   shows "p \<bullet> x = x"
diff -r 494b859bfc16 -r e003e5e36bae Tutorial/Minimal.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Minimal.thy	Wed Jan 19 17:11:10 2011 +0100
@@ -0,0 +1,16 @@
+theory Minimal
+imports "../Nominal/Nominal2"
+begin
+
+atom_decl name
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
+
+lemma alpha_test:
+  shows "Lam [x]. (Var x) = Lam [y]. (Var y)"
+  by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
+
+end
\ No newline at end of file