--- a/src/HOL/Nominal/Nominal.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Nominal/Nominal.thy Tue Sep 07 10:05:19 2010 +0200
@@ -148,11 +148,11 @@
(* permutation on sets *)
lemma empty_eqvt:
shows "pi\<bullet>{} = {}"
- by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] expand_fun_eq)
+ by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] ext_iff)
lemma union_eqvt:
shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
- by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] expand_fun_eq)
+ by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] ext_iff)
(* permutations on products *)
lemma fst_eqvt:
@@ -2069,7 +2069,7 @@
show "?LHS"
proof (rule ccontr)
assume "(pi\<bullet>f) \<noteq> f"
- hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: expand_fun_eq)
+ hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: ext_iff)
then obtain x where b1: "(pi\<bullet>f) x \<noteq> f x" by force
from b have "pi\<bullet>(f ((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" by force
hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))"
@@ -2763,7 +2763,7 @@
and at: "at TYPE ('x)"
shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
using c1 c2
-apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
+apply(auto simp add: cp_def perm_fun_def ext_iff)
apply(simp add: rev_eqvt[symmetric])
apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
done
@@ -2988,7 +2988,7 @@
and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
- apply(simp only: expand_fun_eq)
+ apply(simp only: ext_iff)
apply(rule allI)
apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*)
@@ -3029,7 +3029,7 @@
and a :: "'x"
shows "([a].x = [a].y) = (x = y)"
apply(auto simp add: abs_fun_def)
-apply(auto simp add: expand_fun_eq)
+apply(auto simp add: ext_iff)
apply(drule_tac x="a" in spec)
apply(simp)
done
@@ -3045,7 +3045,7 @@
and a2: "[a].x = [b].y"
shows "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
proof -
- from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: expand_fun_eq)
+ from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: ext_iff)
hence "([a].x) a = ([b].y) a" by simp
hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def)
show "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
@@ -3076,7 +3076,7 @@
shows "[a].x =[b].y"
proof -
show ?thesis
- proof (simp only: abs_fun_def expand_fun_eq, intro strip)
+ proof (simp only: abs_fun_def ext_iff, intro strip)
fix c::"'x"
let ?LHS = "if c=a then nSome(x) else if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone"
and ?RHS = "if c=b then nSome(y) else if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone"