src/HOL/Nominal/Nominal.thy

   by (simp add: perm_bool)
 
 (* 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:
   "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
  by (cases x) simp

 next
   assume b: "?RHS"
   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))" 
       by (simp add: pt_fun_app_eq[OF pt, OF at])
     hence "(pi\<bullet>f) x = f x" by (simp add: pt_pi_rev[OF pt, OF at])

   and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
   and     pt: "pt TYPE ('y) TYPE('x)"
   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
 
 

   and     ptb: "pt TYPE('y) TYPE('x)"
   and     at:  "at TYPE('x)"
   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*)
   apply(subgoal_tac "pi\<bullet>([(a,(rev pi)\<bullet>xa)]\<bullet>x) = [(pi\<bullet>a,xa)]\<bullet>(pi\<bullet>x)")(*C*)
   apply(simp)

   fixes x  :: "'a"
   and   y  :: "'a"
   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
 
 lemma abs_fun_eq2:

       and at: "at TYPE('x)"
       and a1: "a\<noteq>b" 
       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"
   proof (cases "a\<sharp>y")
     assume a4: "a\<sharp>y"

       and a2: "x=[(a,b)]\<bullet>y" 
       and a3: "a\<sharp>y" 
   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"
     show "?LHS=?RHS"
     proof -