# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1284761383 -28800
# Node ID a9b6a00b1ba06a6ace62bb25b1edc99c5530d0b1
# Parent  9b673588244aade3c5ba9938a2f0f52378992fc5
updated to Isabelle Sept 16

diff -r 9b673588244a -r a9b6a00b1ba0 IsaMakefile
--- a/IsaMakefile	Sat Sep 18 05:13:42 2010 +0800
+++ b/IsaMakefile	Sat Sep 18 06:09:43 2010 +0800
@@ -20,15 +20,15 @@
 
 tests: $(LOG)/HOL-Nominal2.gz
 
-$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
-	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
+#$(LOG)/HOL-Nominal2.gz: Nominal/ROOT.ML Nominal/*.thy
+#	@cd Nominal; $(USEDIR) -b -d "" HOL Nominal
 
 ## Nominal2 Paper
 
 paper: $(LOG)/HOL-Nominal2-Paper.gz
 
 $(LOG)/HOL-Nominal2-Paper.gz: Paper/ROOT.ML Paper/document/root.* Paper/*.thy
-	@$(USEDIR) -D generated Nominal Paper
+	@$(USEDIR) -D generated HOL Paper
 	$(ISABELLE_TOOL) document -o pdf  Paper/generated
 	@cp Paper/document.pdf paper.pdf
 
diff -r 9b673588244a -r a9b6a00b1ba0 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal-General/Nominal2_Base.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -140,7 +140,7 @@
 
 lemma Rep_perm_ext:
   "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"
-  by (simp add: expand_fun_eq Rep_perm_inject [symmetric])
+  by (simp add: fun_eq_iff Rep_perm_inject [symmetric])
 
 
 subsection {* Permutations form a group *}
@@ -224,11 +224,11 @@
 lemma swap_cancel:
   "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
   by (rule Rep_perm_ext) 
-     (simp add: Rep_perm_simps expand_fun_eq)
+     (simp add: Rep_perm_simps fun_eq_iff)
 
 lemma swap_self [simp]:
   "(a \<rightleftharpoons> a) = 0"
-  by (rule Rep_perm_ext, simp add: Rep_perm_simps expand_fun_eq)
+  by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff)
 
 lemma minus_swap [simp]:
   "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)"
@@ -237,7 +237,7 @@
 lemma swap_commute:
   "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)"
   by (rule Rep_perm_ext)
-     (simp add: Rep_perm_swap expand_fun_eq)
+     (simp add: Rep_perm_swap fun_eq_iff)
 
 lemma swap_triple:
   assumes "a \<noteq> b" and "c \<noteq> b"
@@ -245,7 +245,7 @@
   shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)"
   using assms
   by (rule_tac Rep_perm_ext)
-     (auto simp add: Rep_perm_simps expand_fun_eq)
+     (auto simp add: Rep_perm_simps fun_eq_iff)
 
 
 section {* Permutation Types *}
@@ -1872,7 +1872,7 @@
     apply (cut_tac `atom a \<sharp> P`)
     apply (simp add: fresh_conv_MOST)
     apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+    apply (simp add: permute_fun_def permute_pure fun_eq_iff)
     apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
     apply (rule refl)
     done
@@ -1896,7 +1896,7 @@
     apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
     apply (simp add: fresh_conv_MOST)
     apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+    apply (simp add: permute_fun_def permute_pure fun_eq_iff)
     apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
     apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
     apply (rule refl)
diff -r 9b673588244a -r a9b6a00b1ba0 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -74,7 +74,7 @@
 (* the normal version of this lemma would cause loops *)
 lemma permute_eqvt_raw[eqvt_raw]:
   shows "p \<bullet> permute \<equiv> permute"
-apply(simp add: expand_fun_eq permute_fun_def)
+apply(simp add: fun_eq_iff permute_fun_def)
 apply(subst permute_eqvt)
 apply(simp)
 done
diff -r 9b673588244a -r a9b6a00b1ba0 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal/Abs.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -552,7 +552,7 @@
   assumes q1: "Quotient R1 abs1 rep1"
   and     q2: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
 lemma [mono]: 
   shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
diff -r 9b673588244a -r a9b6a00b1ba0 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -2,11 +2,6 @@
 imports "../Nominal2" 
 begin
 
-ML {*
-Inductive.unpartition_rules
-*}
-
-
 atom_decl name
 
 declare [[STEPS = 100]]
diff -r 9b673588244a -r a9b6a00b1ba0 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal/FSet.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -634,16 +634,16 @@
 lemma insert_preserve2:
   shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
          (id ---> rep_fset ---> abs_fset) op #"
-  by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+  by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
 
 lemma [quot_preserve]:
   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id finsert_def)
 
 lemma [quot_preserve]:
   "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
 
 lemma list_all2_app_l:
@@ -858,7 +858,7 @@
 
 lemma inj_map_eq_iff:
   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
-  by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
+  by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
 
 text {* alternate formulation with a different decomposition principle
   and a proof of equivalence *}
@@ -1271,7 +1271,7 @@
 lemma fminus_red_fnotin[simp]: "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
   by (simp add: fminus_red)
 
-lemma expand_fset_eq:
+lemma fset_eq_iff:
   "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])