# HG changeset patch
# User Andreas Lochbihler
# Date 1338362019 -7200
# Node ID 2f9584581cf20e0ac02a52aec0ed962da11c08be
# Parent  1c5171abe5cc16af81aedff8299d9356526a8fdf
replace FinFun application syntax with $

diff -r 1c5171abe5cc -r 2f9584581cf2 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Wed May 30 08:48:14 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Wed May 30 09:13:39 2012 +0200
@@ -858,7 +858,7 @@
 
 subsection {* Function application *}
 
-notation finfun_apply ("_\<^sub>f" [1000] 1000)
+notation finfun_apply (infixl "$" 999)
 
 interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
 by(unfold_locales) auto
@@ -875,40 +875,40 @@
   from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
 qed
 
-lemma finfun_apply_def: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
+lemma finfun_apply_def: "op $ = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
 proof(rule finfun_rec_unique)
-  fix c show "finfun_apply (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
+  fix c show "op $ (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
 next
-  fix g a b show "finfun_apply g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else finfun_apply g c)"
+  fix g a b show "op $ g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else g $ c)"
     by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply)
 qed auto
 
-lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
-  and finfun_upd_apply_code [code]: "(finfun_update_code f a b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
+lemma finfun_upd_apply: "f(\<^sup>fa := b) $ a' = (if a = a' then b else f $ a')"
+  and finfun_upd_apply_code [code]: "(finfun_update_code f a b) $ a' = (if a = a' then b else f $ a')"
 by(simp_all add: finfun_apply_def)
 
-lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
+lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b) $ a = b"
 by(simp add: finfun_apply_def)
 
 lemma finfun_upd_apply_same [simp]:
-  "f(\<^sup>fa := b)\<^sub>f a = b"
+  "f(\<^sup>fa := b) $ a = b"
 by(simp add: finfun_upd_apply)
 
 lemma finfun_upd_apply_other [simp]:
-  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
+  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b) $ a' = f $ a'"
 by(simp add: finfun_upd_apply)
 
-lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
+lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g"
 by(auto simp add: finfun_apply_inject[symmetric] simp del: finfun_apply_inject)
 
-lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
+lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
 by(auto intro: finfun_ext)
 
 lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
 by(simp add: expand_finfun_eq fun_eq_iff)
 
 lemma finfun_const_eq_update:
-  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
+  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
 by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
 
 subsection {* Function composition *}
@@ -941,8 +941,8 @@
 by(simp_all add: finfun_comp_def)
 
 lemma finfun_comp_apply [simp]:
-  "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
-by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
+  "op $ (g \<circ>\<^isub>f f) = g \<circ> op $ f"
+by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply)
 
 lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
 by(induct h rule: finfun_weak_induct) simp_all
@@ -958,13 +958,13 @@
 proof -
   have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
   proof(rule finfun_rec_unique)
-    { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
+    { fix c show "Abs_finfun (g \<circ> op $ (\<lambda>\<^isup>f c)) = (\<lambda>\<^isup>f g c)"
         by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
-    { fix g' a b show "Abs_finfun (g \<circ> g'(\<^sup>f a := b)\<^sub>f) = (Abs_finfun (g \<circ> g'\<^sub>f))(\<^sup>f a := g b)"
+    { fix g' a b show "Abs_finfun (g \<circ> op $ g'(\<^sup>f a := b)) = (Abs_finfun (g \<circ> op $ g'))(\<^sup>f a := g b)"
       proof -
         obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
-        moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_left_compose)
-        moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
+        moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
+        moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
         ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
       qed }
   qed auto
@@ -972,7 +972,7 @@
 qed
 
 definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "\<^sub>f\<circ>" 55)
-where [code del]: "finfun_comp2 g f = Abs_finfun (finfun_apply g \<circ> f)"
+where [code del]: "finfun_comp2 g f = Abs_finfun (op $ g \<circ> f)"
 
 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
   including finfun
@@ -984,18 +984,18 @@
   shows "finfun_comp2 (g(\<^sup>f b := c)) f = (if b \<in> range f then (finfun_comp2 g f)(\<^sup>f inv f b := c) else finfun_comp2 g f)"
 proof(cases "b \<in> range f")
   case True
-  from inj have "\<And>x. (finfun_apply g)(f x := c) \<circ> f = (finfun_apply g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
+  from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
   with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
 next
   case False
-  hence "(finfun_apply g)(b := c) \<circ> f = finfun_apply g \<circ> f" by(auto simp add: fun_eq_iff)
+  hence "(op $ g)(b := c) \<circ> f = op $ g \<circ> f" by(auto simp add: fun_eq_iff)
   with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
 qed
 
 subsection {* Universal quantification *}
 
 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
-where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
+where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a"
 
 lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
 by(auto simp add: finfun_All_except_def)
@@ -1004,7 +1004,7 @@
   "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
 by(simp add: finfun_All_except_const is_list_UNIV_iff)
 
-lemma finfun_All_except_update: 
+lemma finfun_All_except_update:
   "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
 by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
 
@@ -1022,14 +1022,14 @@
 lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
 by(simp add: finfun_All_def finfun_All_except_update)
 
-lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
+lemma finfun_All_All: "finfun_All P = All (op $ P)"
 by(simp add: finfun_All_def finfun_All_except_def)
 
 
 definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
 where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
 
-lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
+lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
 unfolding finfun_Ex_def finfun_All_All by simp
 
 lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
@@ -1039,23 +1039,23 @@
 subsection {* A diagonal operator for FinFuns *}
 
 definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
-where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))) f"
+where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g $ a))) f"
 
-interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
+interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g $ a))"
 by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
 
-interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
+interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g $ a))"
 proof
   fix b' b :: 'a
   assume fin: "finite (UNIV :: 'c set)"
   { fix A :: "'c set"
-    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
+    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
     from fin have "finite A" by(auto intro: finite_subset)
-    hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
-      Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
+    hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g $ a))) (Pair b \<circ>\<^isub>f g) A =
+      Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))"
       by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
                  auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
-  from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
+  from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g $ a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
     by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
 qed
 
@@ -1071,14 +1071,14 @@
   "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
 by(simp_all add: finfun_Diag_const1)
 
-lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
-  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
+lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))"
+  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))"
 by(simp_all add: finfun_Diag_def)
 
 lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
 
-lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
+lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f $ a, c))"
 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
 
 lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
@@ -1093,23 +1093,23 @@
 by(simp add: finfun_Diag_def)
 
 lemma finfun_Diag_update_update:
-  "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))(\<^sup>f a' := (f\<^sub>f a', c)))"
+  "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))(\<^sup>f a' := (f $ a', c)))"
 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
 
-lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
-by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
+lemma finfun_Diag_apply [simp]: "op $ (f, g)\<^sup>f = (\<lambda>x. (f $ x, g $ x))"
+by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply)
 
 lemma finfun_Diag_conv_Abs_finfun:
-  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x)))"
+  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (f $ x, g $ x)))"
   including finfun
 proof -
-  have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x))))"
+  have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
   proof(rule finfun_rec_unique)
-    { fix c show "Abs_finfun (\<lambda>x. (finfun_apply (\<lambda>\<^isup>f c) x, finfun_apply g x)) = Pair c \<circ>\<^isub>f g"
+    { fix c show "Abs_finfun (\<lambda>x. ((\<lambda>\<^isup>f c) $ x, g $ x)) = Pair c \<circ>\<^isub>f g"
         by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
     { fix g' a b
-      show "Abs_finfun (\<lambda>x. (finfun_apply g'(\<^sup>f a := b) x, finfun_apply g x)) =
-            (Abs_finfun (\<lambda>x. (finfun_apply g' x, finfun_apply g x)))(\<^sup>f a := (b, g\<^sub>f a))"
+      show "Abs_finfun (\<lambda>x. (g'(\<^sup>f a := b) $ x, g $ x)) =
+            (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(\<^sup>f a := (b, g $ a))"
         by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
   qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
   thus ?thesis by(auto simp add: fun_eq_iff)
@@ -1165,14 +1165,14 @@
 subsection {* Currying for FinFuns *}
 
 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
-where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c)))"
+where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c)))"
 
-interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
+interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))"
 apply(unfold_locales)
 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
 done
 
-interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
+interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))"
 proof(unfold_locales)
   fix b' b :: 'b
   assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
@@ -1181,13 +1181,13 @@
     by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
   note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
   { fix A :: "('c \<times> 'a) set"
-    interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'"
+    interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))) a b'"
       by(rule finfun_curry_aux.upd_left_comm)
     from fin have "finite A" by(auto intro: finite_subset)
-    hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))"
+    hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))"
       by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
   from this[of UNIV]
-  show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
+  show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
     by(simp add: finfun_const_def)
 qed
 
@@ -1195,9 +1195,9 @@
 by(simp add: finfun_curry_def)
 
 lemma finfun_curry_update [simp]:
-  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
+  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
   and finfun_curry_update_code [code]:
-  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
+  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
 by(simp_all add: finfun_curry_def)
 
 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
@@ -1222,15 +1222,15 @@
   proof(rule finfun_rec_unique)
     fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp
     fix f a
-    show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))"
+    show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := (finfun_curry f $ (fst a))(\<^sup>f snd a := c))"
       by(cases a) simp
     show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
       by(simp add: finfun_curry_def finfun_const_def curry_def)
     fix g b
-    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (finfun_apply g(\<^sup>f a := b)) aa)) =
-      (Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))(\<^sup>f
-      fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
-      by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_curry finfun_Abs_finfun_curry)
+    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(\<^sup>f a := b)) aa)) =
+      (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(\<^sup>f
+      fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(\<^sup>f snd a := b))"
+      by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_Abs_finfun_curry)
   qed
   thus ?thesis by(auto simp add: fun_eq_iff)
 qed
@@ -1263,7 +1263,7 @@
 subsection {* The domain of a FinFun as a FinFun *}
 
 definition finfun_dom :: "('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f bool)"
-where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
+where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)"
 
 lemma finfun_dom_const:
   "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
@@ -1281,7 +1281,7 @@
 unfolding card_UNIV_eq_0_infinite_UNIV
 by(simp add: finfun_dom_const)
 
-lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
+lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
 using finite_finfun_default[of f]
 by(simp add: finfun_def exI[where x=False])
 
@@ -1297,7 +1297,7 @@
   "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
 by(simp)
 
-lemma finite_finfun_dom: "finite {x. (finfun_dom f)\<^sub>f x}"
+lemma finite_finfun_dom: "finite {x. finfun_dom f $ x}"
 proof(induct f rule: finfun_weak_induct)
   case (const b)
   thus ?case
@@ -1305,8 +1305,8 @@
       (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
 next
   case (update f a b)
-  have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} =
-    (if b = finfun_default f then {x. (finfun_dom f)\<^sub>f x} - {a} else insert a {x. (finfun_dom f)\<^sub>f x})"
+  have "{x. finfun_dom f(\<^sup>f a := b) $ x} =
+    (if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
     by (auto simp add: finfun_upd_apply split: split_if_asm)
   thus ?case using update by simp
 qed
@@ -1316,9 +1316,9 @@
 
 definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list"
 where
-  "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
+  "finfun_to_list f = (THE xs. set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs)"
 
-lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. (finfun_dom f)\<^sub>f x}" (is ?thesis1)
+lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
   and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
   and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
 proof -
@@ -1328,10 +1328,10 @@
   thus ?thesis1 ?thesis2 ?thesis3 by simp_all
 qed
 
-lemma finfun_const_False_conv_bot: "(\<lambda>\<^isup>f False)\<^sub>f = bot"
+lemma finfun_const_False_conv_bot: "op $ (\<lambda>\<^isup>f False) = bot"
 by auto
 
-lemma finfun_const_True_conv_top: "(\<lambda>\<^isup>f True)\<^sub>f = top"
+lemma finfun_const_True_conv_top: "op $ (\<lambda>\<^isup>f True) = top"
 by auto
 
 lemma finfun_to_list_const:
@@ -1350,7 +1350,7 @@
 by (metis insort_insert_insort remove1_insort)
 
 lemma finfun_dom_conv:
-  "(finfun_dom f)\<^sub>f x \<longleftrightarrow> f\<^sub>f x \<noteq> finfun_default f"
+  "finfun_dom f $ x \<longleftrightarrow> f $ x \<noteq> finfun_default f"
 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
 
 lemma finfun_to_list_update:
@@ -1358,33 +1358,33 @@
   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
 proof(subst finfun_to_list_def, rule the_equality)
   fix xs
-  assume "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} \<and> sorted xs \<and> distinct xs"
-  hence eq: "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x}"
+  assume "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x} \<and> sorted xs \<and> distinct xs"
+  hence eq: "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x}"
     and [simp]: "sorted xs" "distinct xs" by simp_all
   show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
   proof(cases "b = finfun_default f")
     case True [simp]
     show ?thesis
-    proof(cases "(finfun_dom f)\<^sub>f a")
+    proof(cases "finfun_dom f $ a")
       case True
       have "finfun_to_list f = insort_insert a xs"
         unfolding finfun_to_list_def
       proof(rule the_equality)
         have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
         also note eq also
-        have "insert a {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} = {x. (finfun_dom f)\<^sub>f x}" using True
+        have "insert a {x. finfun_dom f(\<^sup>f a := b) $ x} = {x. finfun_dom f $ x}" using True
           by(auto simp add: finfun_upd_apply split: split_if_asm)
-        finally show 1: "set (insort_insert a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
+        finally show 1: "set (insort_insert a xs) = {x. finfun_dom f $ x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
           by(simp add: sorted_insort_insert distinct_insort_insert)
 
         fix xs'
-        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
+        assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
         thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
       qed
       with eq True show ?thesis by(simp add: remove1_insort_insert_same)
     next
       case False
-      hence "f\<^sub>f a = b" by(auto simp add: finfun_dom_conv)
+      hence "f $ a = b" by(auto simp add: finfun_dom_conv)
       hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
       from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
         by(auto elim: sorted_distinct_set_unique intro!: the_equality)
@@ -1393,18 +1393,18 @@
   next
     case False
     show ?thesis
-    proof(cases "(finfun_dom f)\<^sub>f a")
+    proof(cases "finfun_dom f $ a")
       case True
       have "finfun_to_list f = xs"
         unfolding finfun_to_list_def
       proof(rule the_equality)
         have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
           by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
-        with eq show 1: "set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs"
+        with eq show 1: "set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs"
           by(simp del: finfun_dom_update)
         
         fix xs'
-        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
+        assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
         thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
       qed
       thus ?thesis using False True eq by(simp add: insort_insert_triv)
@@ -1415,13 +1415,13 @@
       proof(rule the_equality)
         have "set (remove1 a xs) = set xs - {a}" by simp
         also note eq also
-        have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} - {a} = {x. (finfun_dom f)\<^sub>f x}" using False
+        have "{x. finfun_dom f(\<^sup>f a := b) $ x} - {a} = {x. finfun_dom f $ x}" using False
           by(auto simp add: finfun_upd_apply split: split_if_asm)
-        finally show 1: "set (remove1 a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
+        finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
           by(simp add: sorted_remove1)
         
         fix xs'
-        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
+        assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
         thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
       qed
       thus ?thesis using False eq `b \<noteq> finfun_default f` 
diff -r 1c5171abe5cc -r 2f9584581cf2 src/HOL/ex/FinFunPred.thy
--- a/src/HOL/ex/FinFunPred.thy	Wed May 30 08:48:14 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 09:13:39 2012 +0200
@@ -13,7 +13,7 @@
 instantiation "finfun" :: (type, ord) ord
 begin
 
-definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f\<^sub>f x \<le> g\<^sub>f x)"
+definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)"
 
 definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g"
 
@@ -36,7 +36,7 @@
 instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
 end
 
-lemma bot_finfun_apply [simp]: "bot\<^sub>f = (\<lambda>_. bot)"
+lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
 by(auto simp add: bot_finfun_def)
 
 instantiation "finfun" :: (type, top) top begin
@@ -44,7 +44,7 @@
 instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
 end
 
-lemma top_finfun_apply [simp]: "top\<^sub>f = (\<lambda>_. top)"
+lemma top_finfun_apply [simp]: "op $ top = (\<lambda>_. top)"
 by(auto simp add: top_finfun_def)
 
 instantiation "finfun" :: (type, inf) inf begin
@@ -52,7 +52,7 @@
 instance ..
 end
 
-lemma inf_finfun_apply [simp]: "(inf f g)\<^sub>f = inf f\<^sub>f g\<^sub>f"
+lemma inf_finfun_apply [simp]: "op $ (inf f g) = inf (op $ f) (op $ g)"
 by(auto simp add: inf_finfun_def o_def inf_fun_def)
 
 instantiation "finfun" :: (type, sup) sup begin
@@ -60,7 +60,7 @@
 instance ..
 end
 
-lemma sup_finfun_apply [simp]: "(sup f g)\<^sub>f = sup f\<^sub>f g\<^sub>f"
+lemma sup_finfun_apply [simp]: "op $ (sup f g) = sup (op $ f) (op $ g)"
 by(auto simp add: sup_finfun_def o_def sup_fun_def)
 
 instance "finfun" :: (type, semilattice_inf) semilattice_inf
@@ -82,7 +82,7 @@
 instance ..
 end
 
-lemma minus_finfun_apply [simp]: "(f - g)\<^sub>f = f\<^sub>f - g\<^sub>f"
+lemma minus_finfun_apply [simp]: "op $ (f - g) = op $ f - op $ g"
 by(simp add: minus_finfun_def o_def fun_diff_def)
 
 instantiation "finfun" :: (type, uminus) uminus begin
@@ -90,7 +90,7 @@
 instance ..
 end
 
-lemma uminus_finfun_apply [simp]: "(- g)\<^sub>f = - g\<^sub>f"
+lemma uminus_finfun_apply [simp]: "op $ (- g) = - op $ g"
 by(simp add: uminus_finfun_def o_def fun_Compl_def)
 
 instance "finfun" :: (type, boolean_algebra) boolean_algebra
@@ -111,7 +111,7 @@
 where [code]: "finfun_single x = finfun_empty(\<^sup>f x := True)"
 
 lemma finfun_single_apply [simp]:
-  "(finfun_single x)\<^sub>f y \<longleftrightarrow> x = y"
+  "finfun_single x $ y \<longleftrightarrow> x = y"
 by(simp add: finfun_single_def finfun_upd_apply)
 
 lemma [iff]:
@@ -119,10 +119,10 @@
   and bot_neq_finfun_single: "bot \<noteq> finfun_single x"
 by(simp_all add: expand_finfun_eq fun_eq_iff)
 
-lemma finfun_leI [intro!]: "(!!x. A\<^sub>f x \<Longrightarrow> B\<^sub>f x) \<Longrightarrow> A \<le> B"
+lemma finfun_leI [intro!]: "(!!x. A $ x \<Longrightarrow> B $ x) \<Longrightarrow> A \<le> B"
 by(simp add: le_finfun_def)
 
-lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A\<^sub>f x \<rbrakk> \<Longrightarrow> B\<^sub>f x"
+lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A $ x \<rbrakk> \<Longrightarrow> B $ x"
 by(simp add: le_finfun_def)
 
 text {* Bounded quantification.
@@ -130,7 +130,7 @@
 *}
 
 definition finfun_Ball_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A\<^sub>f a \<longrightarrow> a \<in> set xs \<or> P a)"
+where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A $ a \<longrightarrow> a \<in> set xs \<or> P a)"
 
 lemma finfun_Ball_except_const:
   "finfun_Ball_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (\<lambda>\<^isup>f b) P)"
@@ -150,14 +150,14 @@
 by(simp add: finfun_Ball_except_update)
 
 definition finfun_Ball :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Ball A P = Ball {x. A\<^sub>f x} P"
+where [code del]: "finfun_Ball A P = Ball {x. A $ x} P"
 
 lemma finfun_Ball_code [code]: "finfun_Ball = finfun_Ball_except []"
 by(auto intro!: ext simp add: finfun_Ball_except_def finfun_Ball_def)
 
 
 definition finfun_Bex_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A\<^sub>f a \<and> a \<notin> set xs \<and> P a)"
+where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A $ a \<and> a \<notin> set xs \<and> P a)"
 
 lemma finfun_Bex_except_const:
   "finfun_Bex_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (\<lambda>\<^isup>f b) P)"
@@ -177,7 +177,7 @@
 by(simp add: finfun_Bex_except_update)
 
 definition finfun_Bex :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where [code del]: "finfun_Bex A P = Bex {x. A\<^sub>f x} P"
+where [code del]: "finfun_Bex A P = Bex {x. A $ x} P"
 
 lemma finfun_Bex_code [code]: "finfun_Bex = finfun_Bex_except []"
 by(auto intro!: ext simp add: finfun_Bex_except_def finfun_Bex_def)
@@ -186,54 +186,54 @@
 text {* Automatically replace predicate operations by finfun predicate operations where possible *}
 
 lemma iso_finfun_le [code_unfold]:
-  "A\<^sub>f \<le> B\<^sub>f \<longleftrightarrow> A \<le> B"
+  "op $ A \<le> op $ B \<longleftrightarrow> A \<le> B"
 by (metis le_finfun_def le_funD le_funI)
 
 lemma iso_finfun_less [code_unfold]:
-  "A\<^sub>f < B\<^sub>f \<longleftrightarrow> A < B"
+  "op $ A < op $ B \<longleftrightarrow> A < B"
 by (metis iso_finfun_le less_finfun_def less_fun_def)
 
 lemma iso_finfun_eq [code_unfold]:
-  "A\<^sub>f = B\<^sub>f \<longleftrightarrow> A = B"
+  "op $ A = op $ B \<longleftrightarrow> A = B"
 by(simp only: expand_finfun_eq)
 
 lemma iso_finfun_sup [code_unfold]:
-  "sup A\<^sub>f B\<^sub>f = (sup A B)\<^sub>f"
+  "sup (op $ A) (op $ B) = op $ (sup A B)"
 by(simp)
 
 lemma iso_finfun_disj [code_unfold]:
-  "A\<^sub>f x \<or> B\<^sub>f x \<longleftrightarrow> (sup A B)\<^sub>f x"
+  "A $ x \<or> B $ x \<longleftrightarrow> sup A B $ x"
 by(simp add: sup_fun_def)
 
 lemma iso_finfun_inf [code_unfold]:
-  "inf A\<^sub>f B\<^sub>f = (inf A B)\<^sub>f"
+  "inf (op $ A) (op $ B) = op $ (inf A B)"
 by(simp)
 
 lemma iso_finfun_conj [code_unfold]:
-  "A\<^sub>f x \<and> B\<^sub>f x \<longleftrightarrow> (inf A B)\<^sub>f x"
+  "A $ x \<and> B $ x \<longleftrightarrow> inf A B $ x"
 by(simp add: inf_fun_def)
 
 lemma iso_finfun_empty_conv [code_unfold]:
-  "(\<lambda>_. False) = {}\<^isub>f\<^sub>f"
+  "(\<lambda>_. False) = op $ {}\<^isub>f"
 by simp
 
 lemma iso_finfun_UNIV_conv [code_unfold]:
-  "(\<lambda>_. True) = finfun_UNIV\<^sub>f"
+  "(\<lambda>_. True) = op $ finfun_UNIV"
 by simp
 
 lemma iso_finfun_upd [code_unfold]:
   fixes A :: "'a pred\<^isub>f"
-  shows "A\<^sub>f(x := b) = (A(\<^sup>f x := b))\<^sub>f"
+  shows "(op $ A)(x := b) = op $ (A(\<^sup>f x := b))"
 by(simp add: fun_eq_iff)
 
 lemma iso_finfun_uminus [code_unfold]:
   fixes A :: "'a pred\<^isub>f"
-  shows "- A\<^sub>f = (- A)\<^sub>f"
+  shows "- op $ A = op $ (- A)"
 by(simp)
 
 lemma iso_finfun_minus [code_unfold]:
   fixes A :: "'a pred\<^isub>f"
-  shows "A\<^sub>f - B\<^sub>f = (A - B)\<^sub>f"
+  shows "op $ A - op $ B = op $ (A - B)"
 by(simp)
 
 text {*
@@ -243,11 +243,11 @@
 *}
 
 lemma iso_finfun_Ball_Ball:
-  "(\<forall>x. A\<^sub>f x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
+  "(\<forall>x. A $ x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
 by(simp add: finfun_Ball_def)
 
 lemma iso_finfun_Bex_Bex:
-  "(\<exists>x. A\<^sub>f x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
+  "(\<exists>x. A $ x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
 by(simp add: finfun_Bex_def)
 
 text {* Test replacement setup *}