syntax for FinFun composition without subscripts
authorAndreas Lochbihler
Wed May 30 09:46:58 2012 +0200 (2012-05-30)
changeset 480376c4b3e78f03e
parent 48036 1edcd5f73505
child 48038 72a8506dd59b
syntax for FinFun composition without subscripts
tuned proofs
src/HOL/Library/FinFun.thy
src/HOL/ex/FinFunPred.thy
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 09:36:39 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed May 30 09:46:58 2012 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4    hence "finite {c. g (y c) \<noteq> g b}"
     1.5    proof(induct "{a. y a \<noteq> b}" arbitrary: y)
     1.6      case empty
     1.7 -    hence "y = (\<lambda>a. b)" by(auto intro: ext)
     1.8 +    hence "y = (\<lambda>a. b)" by(auto)
     1.9      thus ?case by(simp)
    1.10    next
    1.11      case (insert x F)
    1.12 @@ -342,7 +342,7 @@
    1.13      proof(induct)
    1.14        case (insert x F)
    1.15        have "(\<lambda>a. if a = x then b' else (if a \<in> F then b' else b)) = (\<lambda>a. if a = x \<or> a \<in> F then b' else b)"
    1.16 -        by(auto intro: ext)
    1.17 +        by(auto)
    1.18        with insert show ?case
    1.19          by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
    1.20      qed(simp add: finfun_const_def) }
    1.21 @@ -480,7 +480,7 @@
    1.22    from fin anf fg show ?thesis
    1.23    proof(induct "dom f" arbitrary: f)
    1.24      case empty
    1.25 -    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
    1.26 +    from `{} = dom f` have "f = empty" by(auto simp add: dom_def)
    1.27      thus ?case by(simp add: finfun_const_def upd_const_same)
    1.28    next
    1.29      case (insert a' A)
    1.30 @@ -518,7 +518,7 @@
    1.31    from fin anf fg show ?thesis
    1.32    proof(induct "dom f" arbitrary: f)
    1.33      case empty
    1.34 -    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
    1.35 +    from `{} = dom f` have "f = empty" by(auto simp add: dom_def)
    1.36      thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
    1.37    next
    1.38      case (insert a' A)
    1.39 @@ -544,7 +544,7 @@
    1.40  qed
    1.41  
    1.42  lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
    1.43 -by(auto simp add: map_default_def restrict_map_def intro: ext)
    1.44 +by(auto simp add: map_default_def restrict_map_def)
    1.45  
    1.46  lemma finite_rec_cong1:
    1.47    assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
    1.48 @@ -619,7 +619,7 @@
    1.49      have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
    1.50      proof(cases "y a' = b")
    1.51        case True
    1.52 -      with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
    1.53 +      with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def)
    1.54        from True have a'ndomg: "a' \<notin> dom ?g" by auto
    1.55        from f b'b b show ?thesis unfolding g'
    1.56          by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
    1.57 @@ -664,7 +664,7 @@
    1.58      let ?b = "map_default b ?g"
    1.59      from fing have fing': "finite (dom ?g')" by auto
    1.60      from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
    1.61 -    have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
    1.62 +    have ffmg': "map_default b ?g' = y(a' := b')" by(auto simp add: map_default_def restrict_map_def)
    1.63      with f y have f_Abs: "f(a' $:= b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
    1.64      have g': "The (?the (f(a' $:= b'))) = ?g'"
    1.65      proof (rule the_equality)
    1.66 @@ -822,7 +822,7 @@
    1.67    proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
    1.68      case empty
    1.69      hence "\<And>a. y a = b" by blast
    1.70 -    hence "y = (\<lambda>a. b)" by(auto intro: ext)
    1.71 +    hence "y = (\<lambda>a. b)" by(auto)
    1.72      hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
    1.73      thus ?case by(simp add: const)
    1.74    next
    1.75 @@ -915,8 +915,10 @@
    1.76  
    1.77  subsection {* Function composition *}
    1.78  
    1.79 -definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "\<circ>\<^isub>f" 55)
    1.80 -where [code del]: "g \<circ>\<^isub>f f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
    1.81 +definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "o$" 55)
    1.82 +where [code del]: "g o$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
    1.83 +
    1.84 +notation (xsymbols) finfun_comp (infixr "\<circ>$" 55)
    1.85  
    1.86  interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
    1.87  by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
    1.88 @@ -935,30 +937,31 @@
    1.89  qed
    1.90  
    1.91  lemma finfun_comp_const [simp, code]:
    1.92 -  "g \<circ>\<^isub>f (K$ c) = (K$ g c)"
    1.93 +  "g \<circ>$ (K$ c) = (K$ g c)"
    1.94  by(simp add: finfun_comp_def)
    1.95  
    1.96 -lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(a $:= b)) = (g \<circ>\<^isub>f f)(a $:= g b)"
    1.97 -  and finfun_comp_update_code [code]: "g \<circ>\<^isub>f (finfun_update_code f a b) = finfun_update_code (g \<circ>\<^isub>f f) a (g b)"
    1.98 +lemma finfun_comp_update [simp]: "g \<circ>$ (f(a $:= b)) = (g \<circ>$ f)(a $:= g b)"
    1.99 +  and finfun_comp_update_code [code]: 
   1.100 +  "g \<circ>$ (finfun_update_code f a b) = finfun_update_code (g \<circ>$ f) a (g b)"
   1.101  by(simp_all add: finfun_comp_def)
   1.102  
   1.103  lemma finfun_comp_apply [simp]:
   1.104 -  "op $ (g \<circ>\<^isub>f f) = g \<circ> op $ f"
   1.105 +  "op $ (g \<circ>$ f) = g \<circ> op $ f"
   1.106  by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply)
   1.107  
   1.108 -lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
   1.109 +lemma finfun_comp_comp_collapse [simp]: "f \<circ>$ g \<circ>$ h = (f \<circ> g) \<circ>$ h"
   1.110  by(induct h rule: finfun_weak_induct) simp_all
   1.111  
   1.112 -lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (K$ c)"
   1.113 +lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>$ f = (K$ c)"
   1.114  by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
   1.115  
   1.116 -lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
   1.117 +lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>$ f = f" "id \<circ>$ f = f"
   1.118  by(induct f rule: finfun_weak_induct) auto
   1.119  
   1.120 -lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
   1.121 +lemma finfun_comp_conv_comp: "g \<circ>$ f = Abs_finfun (g \<circ> op $ f)"
   1.122    including finfun
   1.123  proof -
   1.124 -  have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
   1.125 +  have "(\<lambda>f. g \<circ>$ f) = (\<lambda>f. Abs_finfun (g \<circ> op $ f))"
   1.126    proof(rule finfun_rec_unique)
   1.127      { fix c show "Abs_finfun (g \<circ> op $ (K$ c)) = (K$ g c)"
   1.128          by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
   1.129 @@ -973,8 +976,10 @@
   1.130    thus ?thesis by(auto simp add: fun_eq_iff)
   1.131  qed
   1.132  
   1.133 -definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "\<^sub>f\<circ>" 55)
   1.134 -where [code del]: "finfun_comp2 g f = Abs_finfun (op $ g \<circ> f)"
   1.135 +definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "$o" 55)
   1.136 +where [code del]: "g $o f = Abs_finfun (op $ g \<circ> f)"
   1.137 +
   1.138 +notation (xsymbol) finfun_comp2 (infixr "$\<circ>" 55)
   1.139  
   1.140  lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
   1.141    including finfun
   1.142 @@ -1029,7 +1034,7 @@
   1.143  
   1.144  
   1.145  definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.146 -where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
   1.147 +where "finfun_Ex P = Not (finfun_All (Not \<circ>$ P))"
   1.148  
   1.149  lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
   1.150  unfolding finfun_Ex_def finfun_All_All by simp
   1.151 @@ -1041,27 +1046,27 @@
   1.152  subsection {* A diagonal operator for FinFuns *}
   1.153  
   1.154  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)
   1.155 -where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
   1.156 +where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
   1.157  
   1.158 -interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(a $:= (b, g $ a))"
   1.159 +interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))"
   1.160  by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.161  
   1.162 -interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(a $:= (b, g $ a))"
   1.163 +interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))"
   1.164  proof
   1.165    fix b' b :: 'a
   1.166    assume fin: "finite (UNIV :: 'c set)"
   1.167    { fix A :: "'c set"
   1.168      interpret comp_fun_commute "\<lambda>a c. c(a $:= (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
   1.169      from fin have "finite A" by(auto intro: finite_subset)
   1.170 -    hence "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>\<^isub>f g) A =
   1.171 +    hence "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>$ g) A =
   1.172        Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))"
   1.173        by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
   1.174                   auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
   1.175 -  from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
   1.176 +  from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>$ g) UNIV = Pair b' \<circ>$ g"
   1.177      by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
   1.178  qed
   1.179  
   1.180 -lemma finfun_Diag_const1: "(K$ b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
   1.181 +lemma finfun_Diag_const1: "(K$ b, g)\<^sup>f = Pair b \<circ>$ g"
   1.182  by(simp add: finfun_Diag_def)
   1.183  
   1.184  text {*
   1.185 @@ -1077,7 +1082,7 @@
   1.186    and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(a $:= (b, g $ a))"
   1.187  by(simp_all add: finfun_Diag_def)
   1.188  
   1.189 -lemma finfun_Diag_const2: "(f, K$ c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
   1.190 +lemma finfun_Diag_const2: "(f, K$ c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>$ f"
   1.191  by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
   1.192  
   1.193  lemma finfun_Diag_update2: "(f, g(a $:= c))\<^sup>f = (f, g)\<^sup>f(a $:= (f $ a, c))"
   1.194 @@ -1107,7 +1112,7 @@
   1.195  proof -
   1.196    have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
   1.197    proof(rule finfun_rec_unique)
   1.198 -    { fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>\<^isub>f g"
   1.199 +    { fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>$ g"
   1.200          by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
   1.201      { fix g' a b
   1.202        show "Abs_finfun (\<lambda>x. (g'(a $:= b) $ x, g $ x)) =
   1.203 @@ -1121,7 +1126,7 @@
   1.204  by(auto simp add: expand_finfun_eq fun_eq_iff)
   1.205  
   1.206  definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
   1.207 -where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
   1.208 +where [code]: "finfun_fst f = fst \<circ>$ f"
   1.209  
   1.210  lemma finfun_fst_const: "finfun_fst (K$ bc) = (K$ fst bc)"
   1.211  by(simp add: finfun_fst_def)
   1.212 @@ -1130,18 +1135,18 @@
   1.213    and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(a $:= fst bc)"
   1.214  by(simp_all add: finfun_fst_def)
   1.215  
   1.216 -lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
   1.217 +lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>$ g) = (fst \<circ> f) \<circ>$ g"
   1.218  by(simp add: finfun_fst_def)
   1.219  
   1.220  lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
   1.221  by(induct f rule: finfun_weak_induct)(simp_all add: finfun_Diag_const1 finfun_fst_comp_conv o_def finfun_Diag_update1 finfun_fst_update)
   1.222  
   1.223 -lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o finfun_apply f))"
   1.224 +lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst \<circ> op $ f))"
   1.225  by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp)
   1.226  
   1.227  
   1.228  definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
   1.229 -where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
   1.230 +where [code]: "finfun_snd f = snd \<circ>$ f"
   1.231  
   1.232  lemma finfun_snd_const: "finfun_snd (K$ bc) = (K$ snd bc)"
   1.233  by(simp add: finfun_snd_def)
   1.234 @@ -1150,7 +1155,7 @@
   1.235    and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(a $:= snd bc)"
   1.236  by(simp_all add: finfun_snd_def)
   1.237  
   1.238 -lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
   1.239 +lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>$ g) = (snd \<circ> f) \<circ>$ g"
   1.240  by(simp add: finfun_snd_def)
   1.241  
   1.242  lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
   1.243 @@ -1158,7 +1163,7 @@
   1.244  apply(auto simp add: finfun_Diag_const1 finfun_snd_comp_conv o_def finfun_Diag_update1 finfun_snd_update finfun_upd_apply intro: finfun_ext)
   1.245  done
   1.246  
   1.247 -lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o finfun_apply f))"
   1.248 +lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd \<circ> op $ f))"
   1.249  by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp)
   1.250  
   1.251  lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
   1.252 @@ -1239,11 +1244,11 @@
   1.253  
   1.254  subsection {* Executable equality for FinFuns *}
   1.255  
   1.256 -lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
   1.257 +lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ (f, g)\<^sup>f)"
   1.258  by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
   1.259  
   1.260  instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
   1.261 -definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
   1.262 +definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ (f, g)\<^sup>f)"
   1.263  instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
   1.264  end
   1.265  
     2.1 --- a/src/HOL/ex/FinFunPred.thy	Wed May 30 09:36:39 2012 +0200
     2.2 +++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 09:46:58 2012 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  instance ..
     2.5  
     2.6  lemma le_finfun_code [code]:
     2.7 -  "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>\<^isub>f (f, g)\<^sup>f)"
     2.8 +  "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ (f, g)\<^sup>f)"
     2.9  by(simp add: le_finfun_def finfun_All_All o_def)
    2.10  
    2.11  end
    2.12 @@ -48,7 +48,7 @@
    2.13  by(auto simp add: top_finfun_def)
    2.14  
    2.15  instantiation "finfun" :: (type, inf) inf begin
    2.16 -definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>\<^isub>f (f, g)\<^sup>f"
    2.17 +definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ (f, g)\<^sup>f"
    2.18  instance ..
    2.19  end
    2.20  
    2.21 @@ -56,7 +56,7 @@
    2.22  by(auto simp add: inf_finfun_def o_def inf_fun_def)
    2.23  
    2.24  instantiation "finfun" :: (type, sup) sup begin
    2.25 -definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>\<^isub>f (f, g)\<^sup>f"
    2.26 +definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ (f, g)\<^sup>f"
    2.27  instance ..
    2.28  end
    2.29  
    2.30 @@ -78,7 +78,7 @@
    2.31  by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)
    2.32  
    2.33  instantiation "finfun" :: (type, minus) minus begin
    2.34 -definition "f - g = split (op -) \<circ>\<^isub>f (f, g)\<^sup>f"
    2.35 +definition "f - g = split (op -) \<circ>$ (f, g)\<^sup>f"
    2.36  instance ..
    2.37  end
    2.38  
    2.39 @@ -86,7 +86,7 @@
    2.40  by(simp add: minus_finfun_def o_def fun_diff_def)
    2.41  
    2.42  instantiation "finfun" :: (type, uminus) uminus begin
    2.43 -definition "- A = uminus \<circ>\<^isub>f A"
    2.44 +definition "- A = uminus \<circ>$ A"
    2.45  instance ..
    2.46  end
    2.47  
    2.48 @@ -250,7 +250,7 @@
    2.49    "(\<exists>x. A $ x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
    2.50  by(simp add: finfun_Bex_def)
    2.51  
    2.52 -text {* Test replacement setup *}
    2.53 +text {* Test code setup *}
    2.54  
    2.55  notepad begin
    2.56  have "inf ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) ((\<lambda>_. True)(3 := False)) \<le>