--- 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
--- 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)
--- 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
--- 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"
--- 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]]
--- 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]])