# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265631175 -3600
# Node ID bb7f4457091a78d2b9f6e585c07cf3a5ec2b5867
# Parent  40e3e6a6076f53dad0efc82197c77d12eb12f4dd
moved some lemmas to Nominal; updated all files

diff -r 40e3e6a6076f -r bb7f4457091a Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -3,24 +3,11 @@
 begin
 
 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-lemma in_permute_iff:
-  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-apply(unfold mem_def permute_fun_def)[1]
-apply(simp add: permute_bool_def) 
-done
-
-lemma fresh_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp> p;  a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)"
-  unfolding fresh_def
-  using supp_plus_perm
-  by(auto)
-
 lemma fresh_star_plus:
   fixes p q::perm
   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
   unfolding fresh_star_def
-  by (simp add: fresh_plus)
+  by (simp add: fresh_plus_perm)
 
 
 lemma fresh_star_permute_iff:
@@ -34,18 +21,11 @@
 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1])
 apply(simp)
 apply(drule_tac x="- p \<bullet> xa" in bspec)
-apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1])
+apply(rule_tac ?p1="p" in mem_permute_iff[THEN iffD1])
 apply(simp)
 apply(simp)
 done
 
-lemma fresh_minus_perm:
-  fixes p::perm
-  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
-  apply(simp add: fresh_def)
-  apply(simp only: supp_minus_perm)
-  done
-
 fun
   alpha_gen 
 where
diff -r 40e3e6a6076f -r bb7f4457091a Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -120,10 +120,11 @@
 apply(rule_tac x="pi \<bullet> pia" in exI)
 apply(rule conjI)
 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
+apply(simp only: Diff_eqvt rfv_eqvt insert_eqvt atom_eqvt empty_eqvt)
+apply(simp)
 apply(rule conjI)
 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-apply(simp add: eqvts atom_eqvt)
+apply(simp add: Diff_eqvt rfv_eqvt atom_eqvt insert_eqvt empty_eqvt)
 apply(subst permute_eqvt[symmetric])
 apply(simp)
 done
@@ -619,5 +620,5 @@
 
 
 
-end<
+end
 
diff -r 40e3e6a6076f -r bb7f4457091a Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -2,22 +2,6 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd"
 begin
 
-
-(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
-(* Currently not used, still needed needed? *)
-lemma supp_finite_set:
-  fixes S::"atom set"
-  assumes "finite S"
-  shows "supp S = S"
-  apply(rule finite_supp_unique)
-  apply(simp add: supports_def)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
-  apply(metis)
-  apply(rule assms)
-  apply(auto simp add: permute_set_eq swap_atom)[1]
-done
-  
-
 atom_decl name
 
 datatype rlam =
@@ -324,7 +308,6 @@
 apply auto
 done
 
-(*
 (* pi_abs would be also sufficient to prove the next lemma *)
 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)"
 apply (unfold rep_lam_def)
@@ -338,7 +321,7 @@
 apply (simp only: Quotient_abs_rep[OF Quotient_lam])
 apply auto
 done
-*)
+
 
 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)"
 apply (simp add: expand_fun_eq)
diff -r 40e3e6a6076f -r bb7f4457091a Quot/Nominal/Nominal2_Base.thy
--- a/Quot/Nominal/Nominal2_Base.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/Nominal2_Base.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -859,17 +859,32 @@
   shows "supp (0::perm) = {}"
   unfolding supp_perm by simp
 
+lemma fresh_plus_perm:
+  fixes p q::perm
+  assumes "a \<sharp> p" "a \<sharp> q"
+  shows "a \<sharp> (p + q)"
+  using assms
+  unfolding fresh_def
+  by (auto simp add: supp_perm)
+
 lemma supp_plus_perm:
   fixes p q::perm
   shows "supp (p + q) \<subseteq> supp p \<union> supp q"
   by (auto simp add: supp_perm)
 
+lemma fresh_minus_perm:
+  fixes p::perm
+  shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p"
+  unfolding fresh_def
+  apply(auto simp add: supp_perm)
+  apply(metis permute_minus_cancel)+
+  done
+
 lemma supp_minus_perm:
   fixes p::perm
   shows "supp (- p) = supp p"
-  apply(auto simp add: supp_perm)
-  apply(metis permute_minus_cancel)+
-  done
+  unfolding supp_conv_fresh
+  by (simp add: fresh_minus_perm)
 
 instance perm :: fs
 by default (simp add: supp_perm finite_perm_lemma)
diff -r 40e3e6a6076f -r bb7f4457091a Quot/Nominal/Nominal2_Eqvt.thy
--- a/Quot/Nominal/Nominal2_Eqvt.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -2,6 +2,7 @@
     Authors:    Brian Huffman, Christian Urban
 
     Equivariance, Supp and Fresh Lemmas for Operators. 
+    (Contains most, but not all such lemmas.)
 *)
 theory Nominal2_Eqvt
 imports Nominal2_Base
@@ -76,7 +77,7 @@
 
 lemma the_eqvt:
   assumes unique: "\<exists>!x. P x"
-  shows "p \<bullet> (THE x. P x) = (THE x. p \<bullet> P (- p \<bullet> x))"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
   apply(rule the1_equality [symmetric])
   apply(simp add: ex1_eqvt2[symmetric])
   apply(simp add: permute_bool_def unique)
@@ -86,9 +87,14 @@
 
 section {* Set Operations *}
 
+lemma mem_permute_iff:
+  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
+unfolding mem_def permute_fun_def permute_bool_def
+by simp
+
 lemma mem_eqvt:
   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def permute_fun_def by simp
+  unfolding mem_permute_iff permute_bool_def by simp
 
 lemma not_mem_eqvt:
   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
@@ -229,7 +235,7 @@
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
-  True_eqvt False_eqvt ex_eqvt all_eqvt
+  True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
@@ -237,12 +243,12 @@
   permute_pure
 
   (* datatypes *)
-  permute_prod.simps
+  permute_prod.simps append_eqvt rev_eqvt set_eqvt
   fst_eqvt snd_eqvt
 
   (* sets *)
-  empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
-  Diff_eqvt Compl_eqvt insert_eqvt
+  empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
+  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt
 
 thm eqvts
 thm eqvts_raw
diff -r 40e3e6a6076f -r bb7f4457091a Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/Test.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -110,12 +110,12 @@
     [] => set
   | B (s1, s2) :: tl => 
       if s2 = s then 
-        fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
+        fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
       else fv_bds s tl set
   | BS (s1, s2) :: tl =>
     (* TODO: This is just a copy *)
       if s2 = s then 
-        fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
+        fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
       else fv_bds s tl set
 *}