src/HOL/Library/FinFun.thy
changeset 48035 2f9584581cf2
parent 48034 1c5171abe5cc
child 48036 1edcd5f73505
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 08:48:14 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed May 30 09:13:39 2012 +0200
     1.3 @@ -858,7 +858,7 @@
     1.4  
     1.5  subsection {* Function application *}
     1.6  
     1.7 -notation finfun_apply ("_\<^sub>f" [1000] 1000)
     1.8 +notation finfun_apply (infixl "$" 999)
     1.9  
    1.10  interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
    1.11  by(unfold_locales) auto
    1.12 @@ -875,40 +875,40 @@
    1.13    from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
    1.14  qed
    1.15  
    1.16 -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)"
    1.17 +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)"
    1.18  proof(rule finfun_rec_unique)
    1.19 -  fix c show "finfun_apply (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
    1.20 +  fix c show "op $ (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
    1.21  next
    1.22 -  fix g a b show "finfun_apply g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else finfun_apply g c)"
    1.23 +  fix g a b show "op $ g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else g $ c)"
    1.24      by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply)
    1.25  qed auto
    1.26  
    1.27 -lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
    1.28 -  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')"
    1.29 +lemma finfun_upd_apply: "f(\<^sup>fa := b) $ a' = (if a = a' then b else f $ a')"
    1.30 +  and finfun_upd_apply_code [code]: "(finfun_update_code f a b) $ a' = (if a = a' then b else f $ a')"
    1.31  by(simp_all add: finfun_apply_def)
    1.32  
    1.33 -lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
    1.34 +lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b) $ a = b"
    1.35  by(simp add: finfun_apply_def)
    1.36  
    1.37  lemma finfun_upd_apply_same [simp]:
    1.38 -  "f(\<^sup>fa := b)\<^sub>f a = b"
    1.39 +  "f(\<^sup>fa := b) $ a = b"
    1.40  by(simp add: finfun_upd_apply)
    1.41  
    1.42  lemma finfun_upd_apply_other [simp]:
    1.43 -  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
    1.44 +  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b) $ a' = f $ a'"
    1.45  by(simp add: finfun_upd_apply)
    1.46  
    1.47 -lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
    1.48 +lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g"
    1.49  by(auto simp add: finfun_apply_inject[symmetric] simp del: finfun_apply_inject)
    1.50  
    1.51 -lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
    1.52 +lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
    1.53  by(auto intro: finfun_ext)
    1.54  
    1.55  lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
    1.56  by(simp add: expand_finfun_eq fun_eq_iff)
    1.57  
    1.58  lemma finfun_const_eq_update:
    1.59 -  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
    1.60 +  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
    1.61  by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
    1.62  
    1.63  subsection {* Function composition *}
    1.64 @@ -941,8 +941,8 @@
    1.65  by(simp_all add: finfun_comp_def)
    1.66  
    1.67  lemma finfun_comp_apply [simp]:
    1.68 -  "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
    1.69 -by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
    1.70 +  "op $ (g \<circ>\<^isub>f f) = g \<circ> op $ f"
    1.71 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply)
    1.72  
    1.73  lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
    1.74  by(induct h rule: finfun_weak_induct) simp_all
    1.75 @@ -958,13 +958,13 @@
    1.76  proof -
    1.77    have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
    1.78    proof(rule finfun_rec_unique)
    1.79 -    { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
    1.80 +    { fix c show "Abs_finfun (g \<circ> op $ (\<lambda>\<^isup>f c)) = (\<lambda>\<^isup>f g c)"
    1.81          by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
    1.82 -    { 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)"
    1.83 +    { 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)"
    1.84        proof -
    1.85          obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
    1.86 -        moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_left_compose)
    1.87 -        moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
    1.88 +        moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
    1.89 +        moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
    1.90          ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
    1.91        qed }
    1.92    qed auto
    1.93 @@ -972,7 +972,7 @@
    1.94  qed
    1.95  
    1.96  definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "\<^sub>f\<circ>" 55)
    1.97 -where [code del]: "finfun_comp2 g f = Abs_finfun (finfun_apply g \<circ> f)"
    1.98 +where [code del]: "finfun_comp2 g f = Abs_finfun (op $ g \<circ> f)"
    1.99  
   1.100  lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
   1.101    including finfun
   1.102 @@ -984,18 +984,18 @@
   1.103    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)"
   1.104  proof(cases "b \<in> range f")
   1.105    case True
   1.106 -  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)
   1.107 +  from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
   1.108    with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
   1.109  next
   1.110    case False
   1.111 -  hence "(finfun_apply g)(b := c) \<circ> f = finfun_apply g \<circ> f" by(auto simp add: fun_eq_iff)
   1.112 +  hence "(op $ g)(b := c) \<circ> f = op $ g \<circ> f" by(auto simp add: fun_eq_iff)
   1.113    with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
   1.114  qed
   1.115  
   1.116  subsection {* Universal quantification *}
   1.117  
   1.118  definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.119 -where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
   1.120 +where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a"
   1.121  
   1.122  lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
   1.123  by(auto simp add: finfun_All_except_def)
   1.124 @@ -1004,7 +1004,7 @@
   1.125    "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
   1.126  by(simp add: finfun_All_except_const is_list_UNIV_iff)
   1.127  
   1.128 -lemma finfun_All_except_update: 
   1.129 +lemma finfun_All_except_update:
   1.130    "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
   1.131  by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
   1.132  
   1.133 @@ -1022,14 +1022,14 @@
   1.134  lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
   1.135  by(simp add: finfun_All_def finfun_All_except_update)
   1.136  
   1.137 -lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
   1.138 +lemma finfun_All_All: "finfun_All P = All (op $ P)"
   1.139  by(simp add: finfun_All_def finfun_All_except_def)
   1.140  
   1.141  
   1.142  definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.143  where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
   1.144  
   1.145 -lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
   1.146 +lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
   1.147  unfolding finfun_Ex_def finfun_All_All by simp
   1.148  
   1.149  lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
   1.150 @@ -1039,23 +1039,23 @@
   1.151  subsection {* A diagonal operator for FinFuns *}
   1.152  
   1.153  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.154 -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"
   1.155 +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"
   1.156  
   1.157 -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))"
   1.158 +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))"
   1.159  by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.160  
   1.161 -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))"
   1.162 +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))"
   1.163  proof
   1.164    fix b' b :: 'a
   1.165    assume fin: "finite (UNIV :: 'c set)"
   1.166    { fix A :: "'c set"
   1.167 -    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
   1.168 +    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f 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(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
   1.171 -      Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
   1.172 +    hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g $ a))) (Pair b \<circ>\<^isub>f g) A =
   1.173 +      Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))"
   1.174        by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
   1.175                   auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
   1.176 -  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"
   1.177 +  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"
   1.178      by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
   1.179  qed
   1.180  
   1.181 @@ -1071,14 +1071,14 @@
   1.182    "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
   1.183  by(simp_all add: finfun_Diag_const1)
   1.184  
   1.185 -lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
   1.186 -  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))"
   1.187 +lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))"
   1.188 +  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))"
   1.189  by(simp_all add: finfun_Diag_def)
   1.190  
   1.191  lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
   1.192  by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
   1.193  
   1.194 -lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
   1.195 +lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f $ a, c))"
   1.196  by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
   1.197  
   1.198  lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
   1.199 @@ -1093,23 +1093,23 @@
   1.200  by(simp add: finfun_Diag_def)
   1.201  
   1.202  lemma finfun_Diag_update_update:
   1.203 -  "(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)))"
   1.204 +  "(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)))"
   1.205  by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
   1.206  
   1.207 -lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
   1.208 -by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
   1.209 +lemma finfun_Diag_apply [simp]: "op $ (f, g)\<^sup>f = (\<lambda>x. (f $ x, g $ x))"
   1.210 +by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply)
   1.211  
   1.212  lemma finfun_Diag_conv_Abs_finfun:
   1.213 -  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (finfun_apply f x, finfun_apply g x)))"
   1.214 +  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (f $ x, g $ x)))"
   1.215    including finfun
   1.216  proof -
   1.217 -  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))))"
   1.218 +  have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
   1.219    proof(rule finfun_rec_unique)
   1.220 -    { fix c show "Abs_finfun (\<lambda>x. (finfun_apply (\<lambda>\<^isup>f c) x, finfun_apply g x)) = Pair c \<circ>\<^isub>f g"
   1.221 +    { fix c show "Abs_finfun (\<lambda>x. ((\<lambda>\<^isup>f c) $ x, g $ x)) = Pair c \<circ>\<^isub>f g"
   1.222          by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
   1.223      { fix g' a b
   1.224 -      show "Abs_finfun (\<lambda>x. (finfun_apply g'(\<^sup>f a := b) x, finfun_apply g x)) =
   1.225 -            (Abs_finfun (\<lambda>x. (finfun_apply g' x, finfun_apply g x)))(\<^sup>f a := (b, g\<^sub>f a))"
   1.226 +      show "Abs_finfun (\<lambda>x. (g'(\<^sup>f a := b) $ x, g $ x)) =
   1.227 +            (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(\<^sup>f a := (b, g $ a))"
   1.228          by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
   1.229    qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
   1.230    thus ?thesis by(auto simp add: fun_eq_iff)
   1.231 @@ -1165,14 +1165,14 @@
   1.232  subsection {* Currying for FinFuns *}
   1.233  
   1.234  definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
   1.235 -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)))"
   1.236 +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)))"
   1.237  
   1.238 -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))"
   1.239 +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))"
   1.240  apply(unfold_locales)
   1.241  apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
   1.242  done
   1.243  
   1.244 -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))"
   1.245 +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))"
   1.246  proof(unfold_locales)
   1.247    fix b' b :: 'b
   1.248    assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
   1.249 @@ -1181,13 +1181,13 @@
   1.250      by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
   1.251    note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
   1.252    { fix A :: "('c \<times> 'a) set"
   1.253 -    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'"
   1.254 +    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'"
   1.255        by(rule finfun_curry_aux.upd_left_comm)
   1.256      from fin have "finite A" by(auto intro: finite_subset)
   1.257 -    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))"
   1.258 +    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))"
   1.259        by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
   1.260    from this[of UNIV]
   1.261 -  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'"
   1.262 +  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'"
   1.263      by(simp add: finfun_const_def)
   1.264  qed
   1.265  
   1.266 @@ -1195,9 +1195,9 @@
   1.267  by(simp add: finfun_curry_def)
   1.268  
   1.269  lemma finfun_curry_update [simp]:
   1.270 -  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
   1.271 +  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
   1.272    and finfun_curry_update_code [code]:
   1.273 -  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
   1.274 +  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
   1.275  by(simp_all add: finfun_curry_def)
   1.276  
   1.277  lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
   1.278 @@ -1222,15 +1222,15 @@
   1.279    proof(rule finfun_rec_unique)
   1.280      fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp
   1.281      fix f a
   1.282 -    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))"
   1.283 +    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))"
   1.284        by(cases a) simp
   1.285      show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
   1.286        by(simp add: finfun_curry_def finfun_const_def curry_def)
   1.287      fix g b
   1.288 -    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (finfun_apply g(\<^sup>f a := b)) aa)) =
   1.289 -      (Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))(\<^sup>f
   1.290 -      fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
   1.291 -      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)
   1.292 +    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(\<^sup>f a := b)) aa)) =
   1.293 +      (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(\<^sup>f
   1.294 +      fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(\<^sup>f snd a := b))"
   1.295 +      by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_Abs_finfun_curry)
   1.296    qed
   1.297    thus ?thesis by(auto simp add: fun_eq_iff)
   1.298  qed
   1.299 @@ -1263,7 +1263,7 @@
   1.300  subsection {* The domain of a FinFun as a FinFun *}
   1.301  
   1.302  definition finfun_dom :: "('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f bool)"
   1.303 -where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
   1.304 +where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)"
   1.305  
   1.306  lemma finfun_dom_const:
   1.307    "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
   1.308 @@ -1281,7 +1281,7 @@
   1.309  unfolding card_UNIV_eq_0_infinite_UNIV
   1.310  by(simp add: finfun_dom_const)
   1.311  
   1.312 -lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
   1.313 +lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
   1.314  using finite_finfun_default[of f]
   1.315  by(simp add: finfun_def exI[where x=False])
   1.316  
   1.317 @@ -1297,7 +1297,7 @@
   1.318    "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
   1.319  by(simp)
   1.320  
   1.321 -lemma finite_finfun_dom: "finite {x. (finfun_dom f)\<^sub>f x}"
   1.322 +lemma finite_finfun_dom: "finite {x. finfun_dom f $ x}"
   1.323  proof(induct f rule: finfun_weak_induct)
   1.324    case (const b)
   1.325    thus ?case
   1.326 @@ -1305,8 +1305,8 @@
   1.327        (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
   1.328  next
   1.329    case (update f a b)
   1.330 -  have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} =
   1.331 -    (if b = finfun_default f then {x. (finfun_dom f)\<^sub>f x} - {a} else insert a {x. (finfun_dom f)\<^sub>f x})"
   1.332 +  have "{x. finfun_dom f(\<^sup>f a := b) $ x} =
   1.333 +    (if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
   1.334      by (auto simp add: finfun_upd_apply split: split_if_asm)
   1.335    thus ?case using update by simp
   1.336  qed
   1.337 @@ -1316,9 +1316,9 @@
   1.338  
   1.339  definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list"
   1.340  where
   1.341 -  "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
   1.342 +  "finfun_to_list f = (THE xs. set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs)"
   1.343  
   1.344 -lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. (finfun_dom f)\<^sub>f x}" (is ?thesis1)
   1.345 +lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
   1.346    and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
   1.347    and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
   1.348  proof -
   1.349 @@ -1328,10 +1328,10 @@
   1.350    thus ?thesis1 ?thesis2 ?thesis3 by simp_all
   1.351  qed
   1.352  
   1.353 -lemma finfun_const_False_conv_bot: "(\<lambda>\<^isup>f False)\<^sub>f = bot"
   1.354 +lemma finfun_const_False_conv_bot: "op $ (\<lambda>\<^isup>f False) = bot"
   1.355  by auto
   1.356  
   1.357 -lemma finfun_const_True_conv_top: "(\<lambda>\<^isup>f True)\<^sub>f = top"
   1.358 +lemma finfun_const_True_conv_top: "op $ (\<lambda>\<^isup>f True) = top"
   1.359  by auto
   1.360  
   1.361  lemma finfun_to_list_const:
   1.362 @@ -1350,7 +1350,7 @@
   1.363  by (metis insort_insert_insort remove1_insort)
   1.364  
   1.365  lemma finfun_dom_conv:
   1.366 -  "(finfun_dom f)\<^sub>f x \<longleftrightarrow> f\<^sub>f x \<noteq> finfun_default f"
   1.367 +  "finfun_dom f $ x \<longleftrightarrow> f $ x \<noteq> finfun_default f"
   1.368  by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
   1.369  
   1.370  lemma finfun_to_list_update:
   1.371 @@ -1358,33 +1358,33 @@
   1.372    (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
   1.373  proof(subst finfun_to_list_def, rule the_equality)
   1.374    fix xs
   1.375 -  assume "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} \<and> sorted xs \<and> distinct xs"
   1.376 -  hence eq: "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x}"
   1.377 +  assume "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x} \<and> sorted xs \<and> distinct xs"
   1.378 +  hence eq: "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x}"
   1.379      and [simp]: "sorted xs" "distinct xs" by simp_all
   1.380    show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
   1.381    proof(cases "b = finfun_default f")
   1.382      case True [simp]
   1.383      show ?thesis
   1.384 -    proof(cases "(finfun_dom f)\<^sub>f a")
   1.385 +    proof(cases "finfun_dom f $ a")
   1.386        case True
   1.387        have "finfun_to_list f = insort_insert a xs"
   1.388          unfolding finfun_to_list_def
   1.389        proof(rule the_equality)
   1.390          have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
   1.391          also note eq also
   1.392 -        have "insert a {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} = {x. (finfun_dom f)\<^sub>f x}" using True
   1.393 +        have "insert a {x. finfun_dom f(\<^sup>f a := b) $ x} = {x. finfun_dom f $ x}" using True
   1.394            by(auto simp add: finfun_upd_apply split: split_if_asm)
   1.395 -        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)"
   1.396 +        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)"
   1.397            by(simp add: sorted_insort_insert distinct_insort_insert)
   1.398  
   1.399          fix xs'
   1.400 -        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
   1.401 +        assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
   1.402          thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
   1.403        qed
   1.404        with eq True show ?thesis by(simp add: remove1_insort_insert_same)
   1.405      next
   1.406        case False
   1.407 -      hence "f\<^sub>f a = b" by(auto simp add: finfun_dom_conv)
   1.408 +      hence "f $ a = b" by(auto simp add: finfun_dom_conv)
   1.409        hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.410        from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
   1.411          by(auto elim: sorted_distinct_set_unique intro!: the_equality)
   1.412 @@ -1393,18 +1393,18 @@
   1.413    next
   1.414      case False
   1.415      show ?thesis
   1.416 -    proof(cases "(finfun_dom f)\<^sub>f a")
   1.417 +    proof(cases "finfun_dom f $ a")
   1.418        case True
   1.419        have "finfun_to_list f = xs"
   1.420          unfolding finfun_to_list_def
   1.421        proof(rule the_equality)
   1.422          have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
   1.423            by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.424 -        with eq show 1: "set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs"
   1.425 +        with eq show 1: "set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs"
   1.426            by(simp del: finfun_dom_update)
   1.427          
   1.428          fix xs'
   1.429 -        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
   1.430 +        assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
   1.431          thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
   1.432        qed
   1.433        thus ?thesis using False True eq by(simp add: insort_insert_triv)
   1.434 @@ -1415,13 +1415,13 @@
   1.435        proof(rule the_equality)
   1.436          have "set (remove1 a xs) = set xs - {a}" by simp
   1.437          also note eq also
   1.438 -        have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} - {a} = {x. (finfun_dom f)\<^sub>f x}" using False
   1.439 +        have "{x. finfun_dom f(\<^sup>f a := b) $ x} - {a} = {x. finfun_dom f $ x}" using False
   1.440            by(auto simp add: finfun_upd_apply split: split_if_asm)
   1.441 -        finally show 1: "set (remove1 a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
   1.442 +        finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
   1.443            by(simp add: sorted_remove1)
   1.444          
   1.445          fix xs'
   1.446 -        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
   1.447 +        assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
   1.448          thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
   1.449        qed
   1.450        thus ?thesis using False eq `b \<noteq> finfun_default f`