src/HOL/Library/FinFun.thy
changeset 48036 1edcd5f73505
parent 48035 2f9584581cf2
child 48037 6c4b3e78f03e
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed May 30 09:13:39 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed May 30 09:36:39 2012 +0200
     1.3 @@ -278,35 +278,35 @@
     1.4  
     1.5  subsection {* Kernel functions for type @{typ "'a \<Rightarrow>f 'b"} *}
     1.6  
     1.7 -lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
     1.8 +lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("K$/ _" [0] 1)
     1.9  is "\<lambda> b x. b" by (rule const_finfun)
    1.10  
    1.11 -lift_definition finfun_update :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd"
    1.12 +lift_definition finfun_update :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(_ $:= _')" [1000,0,0] 1000) is "fun_upd"
    1.13  by (simp add: fun_upd_finfun)
    1.14  
    1.15 -lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(\<^sup>f a := b)(\<^sup>f a' := b') = f(\<^sup>f a' := b')(\<^sup>f a := b)"
    1.16 +lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(a $:= b)(a' $:= b') = f(a' $:= b')(a $:= b)"
    1.17  by transfer (simp add: fun_upd_twist)
    1.18  
    1.19  lemma finfun_update_twice [simp]:
    1.20 -  "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
    1.21 +  "f(a $:= b)(a $:= b') = f(a $:= b')"
    1.22  by transfer simp
    1.23  
    1.24 -lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
    1.25 +lemma finfun_update_const_same: "(K$ b)(a $:= b) = (K$ b)"
    1.26  by transfer (simp add: fun_eq_iff)
    1.27  
    1.28  subsection {* Code generator setup *}
    1.29  
    1.30 -definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
    1.31 +definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
    1.32  where [simp, code del]: "finfun_update_code = finfun_update"
    1.33  
    1.34  code_datatype finfun_const finfun_update_code
    1.35  
    1.36  lemma finfun_update_const_code [code]:
    1.37 -  "(\<lambda>\<^isup>f b)(\<^sup>f a := b') = (if b = b' then (\<lambda>\<^isup>f b) else finfun_update_code (\<lambda>\<^isup>f b) a b')"
    1.38 +  "(K$ b)(a $:= b') = (if b = b' then (K$ b) else finfun_update_code (K$ b) a b')"
    1.39  by(simp add: finfun_update_const_same)
    1.40  
    1.41  lemma finfun_update_update_code [code]:
    1.42 -  "(finfun_update_code f a b)(\<^sup>f a' := b') = (if a = a' then f(\<^sup>f a := b') else finfun_update_code (f(\<^sup>f a' := b')) a b)"
    1.43 +  "(finfun_update_code f a b)(a' $:= b') = (if a = a' then f(a $:= b') else finfun_update_code (f(a' $:= b')) a b)"
    1.44  by(simp add: finfun_update_twist)
    1.45  
    1.46  
    1.47 @@ -316,29 +316,29 @@
    1.48  
    1.49  subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
    1.50  
    1.51 -interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
    1.52 +interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')"
    1.53    including finfun
    1.54  proof
    1.55    fix a a' :: 'a
    1.56 -  show "(\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b')) = (\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))"
    1.57 +  show "(\<lambda>f. f(a $:= b')) \<circ> (\<lambda>f. f(a' $:= b')) = (\<lambda>f. f(a' $:= b')) \<circ> (\<lambda>f. f(a $:= b'))"
    1.58    proof
    1.59      fix b
    1.60      have "(finfun_apply b)(a := b', a' := b') = (finfun_apply b)(a' := b', a := b')"
    1.61        by(cases "a = a'")(auto simp add: fun_upd_twist)
    1.62 -    then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
    1.63 +    then have "b(a $:= b')(a' $:= b') = b(a' $:= b')(a $:= b')"
    1.64        by(auto simp add: finfun_update_def fun_upd_twist)
    1.65 -    then show "((\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b'))) b = ((\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))) b"
    1.66 +    then show "((\<lambda>f. f(a $:= b')) \<circ> (\<lambda>f. f(a' $:= b'))) b = ((\<lambda>f. f(a' $:= b')) \<circ> (\<lambda>f. f(a $:= b'))) b"
    1.67        by (simp add: fun_eq_iff)
    1.68    qed
    1.69  qed
    1.70  
    1.71  lemma fold_finfun_update_finite_univ:
    1.72    assumes fin: "finite (UNIV :: 'a set)"
    1.73 -  shows "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
    1.74 +  shows "Finite_Set.fold (\<lambda>a f. f(a $:= b')) (K$ b) (UNIV :: 'a set) = (K$ b')"
    1.75  proof -
    1.76    { fix A :: "'a set"
    1.77      from fin have "finite A" by(auto intro: finite_subset)
    1.78 -    hence "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)"
    1.79 +    hence "Finite_Set.fold (\<lambda>a f. f(a $:= b')) (K$ b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)"
    1.80      proof(induct)
    1.81        case (insert x F)
    1.82        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.83 @@ -427,15 +427,15 @@
    1.84  lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
    1.85  by transfer (erule finite_finfun_default_aux)
    1.86  
    1.87 -lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
    1.88 +lemma finfun_default_const: "finfun_default ((K$ b) :: 'a \<Rightarrow>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
    1.89  by(transfer)(auto simp add: finfun_default_aux_infinite finfun_default_aux_def)
    1.90  
    1.91  lemma finfun_default_update_const:
    1.92 -  "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
    1.93 +  "finfun_default (f(a $:= b)) = finfun_default f"
    1.94  by transfer (simp add: finfun_default_aux_update_const)
    1.95  
    1.96  lemma finfun_default_const_code [code]:
    1.97 -  "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
    1.98 +  "finfun_default ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
    1.99  by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
   1.100  
   1.101  lemma finfun_default_update_code [code]:
   1.102 @@ -573,7 +573,7 @@
   1.103  qed
   1.104  
   1.105  lemma finfun_rec_upd [simp]:
   1.106 -  "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
   1.107 +  "finfun_rec cnst upd (f(a' $:= b')) = upd a' b' (finfun_rec cnst upd f)"
   1.108    including finfun
   1.109  proof -
   1.110    obtain b where b: "b = finfun_default f" by auto
   1.111 @@ -637,15 +637,15 @@
   1.112        also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
   1.113        finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
   1.114      qed
   1.115 -    also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
   1.116 +    also have "The (?the (f(a' $:= b'))) = ?g'"
   1.117      proof(rule the_equality)
   1.118 -      from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
   1.119 +      from f y b b'b brang' fing' show "?the (f(a' $:= b')) ?g'"
   1.120          by(auto simp del: fun_upd_apply simp add: finfun_update_def)
   1.121      next
   1.122        fix g'
   1.123 -      assume "?the (f(\<^sup>f a' := b')) g'"
   1.124 +      assume "?the (f(a' $:= b')) g'"
   1.125        hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
   1.126 -        and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')" 
   1.127 +        and eq: "f(a' $:= b') = Abs_finfun (map_default b g')" 
   1.128          by(auto simp del: fun_upd_apply)
   1.129        from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
   1.130          by(blast intro: map_default_in_finfun)+
   1.131 @@ -665,13 +665,14 @@
   1.132      from fing have fing': "finite (dom ?g')" by auto
   1.133      from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
   1.134      have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
   1.135 -    with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
   1.136 -    have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
   1.137 +    with f y have f_Abs: "f(a' $:= b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
   1.138 +    have g': "The (?the (f(a' $:= b'))) = ?g'"
   1.139      proof (rule the_equality)
   1.140 -      from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
   1.141 +      from fing' bnrang' f_Abs show "?the (f(a' $:= b')) ?g'"
   1.142 +        by(auto simp add: finfun_update_def restrict_map_def)
   1.143      next
   1.144 -      fix g' assume "?the (f(\<^sup>f a' := b')) g'"
   1.145 -      hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
   1.146 +      fix g' assume "?the (f(a' $:= b')) g'"
   1.147 +      hence f': "f(a' $:= b') = Abs_finfun (map_default b g')"
   1.148          and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
   1.149        from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
   1.150          by(auto intro: map_default_in_finfun)
   1.151 @@ -716,7 +717,8 @@
   1.152                                       unfolded this, OF fing'' a'ndomg'' g''leg]
   1.153          also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
   1.154          from upd_left_comm upd_left_comm fing''
   1.155 -        have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
   1.156 +        have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') =
   1.157 +          Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
   1.158            by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
   1.159          with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
   1.160                       upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
   1.161 @@ -740,18 +742,18 @@
   1.162  begin
   1.163  
   1.164  lemma finfun_rec_const [simp]: includes finfun shows
   1.165 -  "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
   1.166 +  "finfun_rec cnst upd (K$ c) = cnst c"
   1.167  proof(cases "finite (UNIV :: 'a set)")
   1.168    case False
   1.169 -  hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
   1.170 -  moreover have "(THE g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
   1.171 +  hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
   1.172 +  moreover have "(THE g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
   1.173    proof (rule the_equality)
   1.174 -    show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
   1.175 +    show "(K$ c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
   1.176        by(auto simp add: finfun_const_def)
   1.177    next
   1.178      fix g :: "'a \<rightharpoonup> 'b"
   1.179 -    assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
   1.180 -    hence g: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
   1.181 +    assume "(K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
   1.182 +    hence g: "(K$ c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
   1.183      from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
   1.184        by(simp add: finfun_const_def)
   1.185      moreover have "map_default c empty = (\<lambda>a. c)" by simp
   1.186 @@ -760,8 +762,8 @@
   1.187    ultimately show ?thesis by(simp add: finfun_rec_def)
   1.188  next
   1.189    case True
   1.190 -  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = undefined" by(simp add: finfun_default_const)
   1.191 -  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
   1.192 +  hence default: "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = undefined" by(simp add: finfun_default_const)
   1.193 +  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
   1.194    show ?thesis
   1.195    proof(cases "c = undefined")
   1.196      case True
   1.197 @@ -771,7 +773,7 @@
   1.198      next
   1.199        fix g'
   1.200        assume "?the g'"
   1.201 -      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
   1.202 +      hence fg: "(K$ c) = Abs_finfun (map_default undefined g')"
   1.203          and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
   1.204        from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
   1.205        with fg have "map_default undefined g' = (\<lambda>a. c)"
   1.206 @@ -790,7 +792,7 @@
   1.207      next
   1.208        fix g' :: "'a \<rightharpoonup> 'b"
   1.209        assume "?the g'"
   1.210 -      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
   1.211 +      hence fg: "(K$ c) = Abs_finfun (map_default undefined g')"
   1.212          and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
   1.213        from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
   1.214        with fg have "map_default undefined g' = (\<lambda>a. c)"
   1.215 @@ -809,8 +811,8 @@
   1.216  subsection {* Weak induction rule and case analysis for FinFuns *}
   1.217  
   1.218  lemma finfun_weak_induct [consumes 0, case_names const update]:
   1.219 -  assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
   1.220 -  and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
   1.221 +  assumes const: "\<And>b. P (K$ b)"
   1.222 +  and update: "\<And>f a b. P f \<Longrightarrow> P (f(a $:= b))"
   1.223    shows "P x"
   1.224    including finfun
   1.225  proof(induct x rule: Abs_finfun_induct)
   1.226 @@ -838,16 +840,16 @@
   1.227  by(induct x rule: finfun_weak_induct) blast+
   1.228  
   1.229  lemma finfun_exhaust:
   1.230 -  obtains b where "x = (\<lambda>\<^isup>f b)"
   1.231 -        | f a b where "x = f(\<^sup>f a := b)"
   1.232 +  obtains b where "x = (K$ b)"
   1.233 +        | f a b where "x = f(a $:= b)"
   1.234  by(atomize_elim)(rule finfun_exhaust_disj)
   1.235  
   1.236  lemma finfun_rec_unique:
   1.237    fixes f :: "'a \<Rightarrow>f 'b \<Rightarrow> 'c"
   1.238 -  assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
   1.239 -  and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
   1.240 -  and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
   1.241 -  and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
   1.242 +  assumes c: "\<And>c. f (K$ c) = cnst c"
   1.243 +  and u: "\<And>g a b. f (g(a $:= b)) = upd g a b (f g)"
   1.244 +  and c': "\<And>c. f' (K$ c) = cnst c"
   1.245 +  and u': "\<And>g a b. f' (g(a $:= b)) = upd g a b (f' g)"
   1.246    shows "f = f'"
   1.247  proof
   1.248    fix g :: "'a \<Rightarrow>f 'b"
   1.249 @@ -877,25 +879,25 @@
   1.250  
   1.251  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.252  proof(rule finfun_rec_unique)
   1.253 -  fix c show "op $ (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
   1.254 +  fix c show "op $ (K$ c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
   1.255  next
   1.256 -  fix g a b show "op $ g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else g $ c)"
   1.257 +  fix g a b show "op $ g(a $:= b) = (\<lambda>c. if c = a then b else g $ c)"
   1.258      by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply)
   1.259  qed auto
   1.260  
   1.261 -lemma finfun_upd_apply: "f(\<^sup>fa := b) $ a' = (if a = a' then b else f $ a')"
   1.262 +lemma finfun_upd_apply: "f(a $:= b) $ a' = (if a = a' then b else f $ a')"
   1.263    and finfun_upd_apply_code [code]: "(finfun_update_code f a b) $ a' = (if a = a' then b else f $ a')"
   1.264  by(simp_all add: finfun_apply_def)
   1.265  
   1.266 -lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b) $ a = b"
   1.267 +lemma finfun_const_apply [simp, code]: "(K$ b) $ a = b"
   1.268  by(simp add: finfun_apply_def)
   1.269  
   1.270  lemma finfun_upd_apply_same [simp]:
   1.271 -  "f(\<^sup>fa := b) $ a = b"
   1.272 +  "f(a $:= b) $ a = b"
   1.273  by(simp add: finfun_upd_apply)
   1.274  
   1.275  lemma finfun_upd_apply_other [simp]:
   1.276 -  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b) $ a' = f $ a'"
   1.277 +  "a \<noteq> a' \<Longrightarrow> f(a $:= b) $ a' = f $ a'"
   1.278  by(simp add: finfun_upd_apply)
   1.279  
   1.280  lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g"
   1.281 @@ -904,39 +906,39 @@
   1.282  lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
   1.283  by(auto intro: finfun_ext)
   1.284  
   1.285 -lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
   1.286 +lemma finfun_const_inject [simp]: "(K$ b) = (K$ b') \<equiv> b = b'"
   1.287  by(simp add: expand_finfun_eq fun_eq_iff)
   1.288  
   1.289  lemma finfun_const_eq_update:
   1.290 -  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
   1.291 +  "((K$ b) = f(a $:= b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
   1.292  by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.293  
   1.294  subsection {* Function composition *}
   1.295  
   1.296  definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "\<circ>\<^isub>f" 55)
   1.297 -where [code del]: "g \<circ>\<^isub>f f  = finfun_rec (\<lambda>b. (\<lambda>\<^isup>f g b)) (\<lambda>a b c. c(\<^sup>f a := g b)) f"
   1.298 +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.299  
   1.300 -interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
   1.301 +interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
   1.302  by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
   1.303  
   1.304 -interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
   1.305 +interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
   1.306  proof
   1.307    fix b' b :: 'a
   1.308    assume fin: "finite (UNIV :: 'c set)"
   1.309    { fix A :: "'c set"
   1.310      from fin have "finite A" by(auto intro: finite_subset)
   1.311 -    hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
   1.312 +    hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) A =
   1.313        Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
   1.314        by induct (simp_all add: finfun_const_def, auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
   1.315 -  from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')"
   1.316 +  from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) UNIV = (K$ g b')"
   1.317      by(simp add: finfun_const_def)
   1.318  qed
   1.319  
   1.320  lemma finfun_comp_const [simp, code]:
   1.321 -  "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
   1.322 +  "g \<circ>\<^isub>f (K$ c) = (K$ g c)"
   1.323  by(simp add: finfun_comp_def)
   1.324  
   1.325 -lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
   1.326 +lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(a $:= b)) = (g \<circ>\<^isub>f f)(a $:= g b)"
   1.327    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.328  by(simp_all add: finfun_comp_def)
   1.329  
   1.330 @@ -947,7 +949,7 @@
   1.331  lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
   1.332  by(induct h rule: finfun_weak_induct) simp_all
   1.333  
   1.334 -lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
   1.335 +lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (K$ c)"
   1.336  by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
   1.337  
   1.338  lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
   1.339 @@ -958,9 +960,9 @@
   1.340  proof -
   1.341    have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
   1.342    proof(rule finfun_rec_unique)
   1.343 -    { fix c show "Abs_finfun (g \<circ> op $ (\<lambda>\<^isup>f c)) = (\<lambda>\<^isup>f g c)"
   1.344 +    { fix c show "Abs_finfun (g \<circ> op $ (K$ c)) = (K$ g c)"
   1.345          by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
   1.346 -    { 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.347 +    { fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
   1.348        proof -
   1.349          obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
   1.350          moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
   1.351 @@ -974,14 +976,14 @@
   1.352  definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "\<^sub>f\<circ>" 55)
   1.353  where [code del]: "finfun_comp2 g f = Abs_finfun (op $ g \<circ> f)"
   1.354  
   1.355 -lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
   1.356 +lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
   1.357    including finfun
   1.358  by(simp add: finfun_comp2_def finfun_const_def comp_def)
   1.359  
   1.360  lemma finfun_comp2_update:
   1.361    includes finfun
   1.362    assumes inj: "inj f"
   1.363 -  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.364 +  shows "finfun_comp2 (g(b $:= c)) f = (if b \<in> range f then (finfun_comp2 g f)(inv f b $:= c) else finfun_comp2 g f)"
   1.365  proof(cases "b \<in> range f")
   1.366    case True
   1.367    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.368 @@ -997,15 +999,15 @@
   1.369  definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.370  where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a"
   1.371  
   1.372 -lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
   1.373 +lemma finfun_All_except_const: "finfun_All_except A (K$ b) \<longleftrightarrow> b \<or> set A = UNIV"
   1.374  by(auto simp add: finfun_All_except_def)
   1.375  
   1.376  lemma finfun_All_except_const_finfun_UNIV_code [code]:
   1.377 -  "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
   1.378 +  "finfun_All_except A (K$ b) = (b \<or> is_list_UNIV A)"
   1.379  by(simp add: finfun_All_except_const is_list_UNIV_iff)
   1.380  
   1.381  lemma finfun_All_except_update:
   1.382 -  "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
   1.383 +  "finfun_All_except A f(a $:= b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
   1.384  by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
   1.385  
   1.386  lemma finfun_All_except_update_code [code]:
   1.387 @@ -1016,10 +1018,10 @@
   1.388  definition finfun_All :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.389  where "finfun_All = finfun_All_except []"
   1.390  
   1.391 -lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
   1.392 +lemma finfun_All_const [simp]: "finfun_All (K$ b) = b"
   1.393  by(simp add: finfun_All_def finfun_All_except_def)
   1.394  
   1.395 -lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
   1.396 +lemma finfun_All_update: "finfun_All f(a $:= b) = (b \<and> finfun_All_except [a] f)"
   1.397  by(simp add: finfun_All_def finfun_All_except_update)
   1.398  
   1.399  lemma finfun_All_All: "finfun_All P = All (op $ P)"
   1.400 @@ -1032,34 +1034,34 @@
   1.401  lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
   1.402  unfolding finfun_Ex_def finfun_All_All by simp
   1.403  
   1.404 -lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
   1.405 +lemma finfun_Ex_const [simp]: "finfun_Ex (K$ b) = b"
   1.406  by(simp add: finfun_Ex_def)
   1.407  
   1.408  
   1.409  subsection {* A diagonal operator for FinFuns *}
   1.410  
   1.411  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.412 -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.413 +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.414  
   1.415 -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.416 +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.417  by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.418  
   1.419 -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.420 +interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(a $:= (b, g $ a))"
   1.421  proof
   1.422    fix b' b :: 'a
   1.423    assume fin: "finite (UNIV :: 'c set)"
   1.424    { fix A :: "'c set"
   1.425 -    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
   1.426 +    interpret comp_fun_commute "\<lambda>a c. c(a $:= (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
   1.427      from fin have "finite A" by(auto intro: finite_subset)
   1.428 -    hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g $ a))) (Pair b \<circ>\<^isub>f g) A =
   1.429 +    hence "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>\<^isub>f g) A =
   1.430        Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))"
   1.431        by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
   1.432                   auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
   1.433 -  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.434 +  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.435      by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
   1.436  qed
   1.437  
   1.438 -lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
   1.439 +lemma finfun_Diag_const1: "(K$ b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
   1.440  by(simp add: finfun_Diag_def)
   1.441  
   1.442  text {*
   1.443 @@ -1067,33 +1069,33 @@
   1.444  *}
   1.445  
   1.446  lemma finfun_Diag_const_code [code]:
   1.447 -  "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
   1.448 -  "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
   1.449 +  "(K$ b, K$ c)\<^sup>f = (K$ (b, c))"
   1.450 +  "(K$ b, finfun_update_code g a c)\<^sup>f = finfun_update_code (K$ b, g)\<^sup>f a (b, c)"
   1.451  by(simp_all add: finfun_Diag_const1)
   1.452  
   1.453 -lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))"
   1.454 -  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.455 +lemma finfun_Diag_update1: "(f(a $:= b), g)\<^sup>f = (f, g)\<^sup>f(a $:= (b, g $ a))"
   1.456 +  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(a $:= (b, g $ a))"
   1.457  by(simp_all add: finfun_Diag_def)
   1.458  
   1.459 -lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
   1.460 +lemma finfun_Diag_const2: "(f, K$ c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
   1.461  by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
   1.462  
   1.463 -lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f $ a, c))"
   1.464 +lemma finfun_Diag_update2: "(f, g(a $:= c))\<^sup>f = (f, g)\<^sup>f(a $:= (f $ a, c))"
   1.465  by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
   1.466  
   1.467 -lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
   1.468 +lemma finfun_Diag_const_const [simp]: "(K$ b, K$ c)\<^sup>f = (K$ (b, c))"
   1.469  by(simp add: finfun_Diag_const1)
   1.470  
   1.471  lemma finfun_Diag_const_update:
   1.472 -  "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
   1.473 +  "(K$ b, g(a $:= c))\<^sup>f = (K$ b, g)\<^sup>f(a $:= (b, c))"
   1.474  by(simp add: finfun_Diag_const1)
   1.475  
   1.476  lemma finfun_Diag_update_const:
   1.477 -  "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
   1.478 +  "(f(a $:= b), K$ c)\<^sup>f = (f, K$ c)\<^sup>f(a $:= (b, c))"
   1.479  by(simp add: finfun_Diag_def)
   1.480  
   1.481  lemma finfun_Diag_update_update:
   1.482 -  "(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.483 +  "(f(a $:= b), g(a' $:= c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(a $:= (b, c)) else (f, g)\<^sup>f(a $:= (b, g $ a))(a' $:= (f $ a', c)))"
   1.484  by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
   1.485  
   1.486  lemma finfun_Diag_apply [simp]: "op $ (f, g)\<^sup>f = (\<lambda>x. (f $ x, g $ x))"
   1.487 @@ -1105,11 +1107,11 @@
   1.488  proof -
   1.489    have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
   1.490    proof(rule finfun_rec_unique)
   1.491 -    { fix c show "Abs_finfun (\<lambda>x. ((\<lambda>\<^isup>f c) $ x, g $ x)) = Pair c \<circ>\<^isub>f g"
   1.492 +    { fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>\<^isub>f g"
   1.493          by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
   1.494      { fix g' a b
   1.495 -      show "Abs_finfun (\<lambda>x. (g'(\<^sup>f a := b) $ x, g $ x)) =
   1.496 -            (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(\<^sup>f a := (b, g $ a))"
   1.497 +      show "Abs_finfun (\<lambda>x. (g'(a $:= b) $ x, g $ x)) =
   1.498 +            (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(a $:= (b, g $ a))"
   1.499          by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
   1.500    qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
   1.501    thus ?thesis by(auto simp add: fun_eq_iff)
   1.502 @@ -1121,11 +1123,11 @@
   1.503  definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
   1.504  where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
   1.505  
   1.506 -lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
   1.507 +lemma finfun_fst_const: "finfun_fst (K$ bc) = (K$ fst bc)"
   1.508  by(simp add: finfun_fst_def)
   1.509  
   1.510 -lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
   1.511 -  and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
   1.512 +lemma finfun_fst_update: "finfun_fst (f(a $:= bc)) = (finfun_fst f)(a $:= fst bc)"
   1.513 +  and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(a $:= fst bc)"
   1.514  by(simp_all add: finfun_fst_def)
   1.515  
   1.516  lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
   1.517 @@ -1141,11 +1143,11 @@
   1.518  definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
   1.519  where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
   1.520  
   1.521 -lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
   1.522 +lemma finfun_snd_const: "finfun_snd (K$ bc) = (K$ snd bc)"
   1.523  by(simp add: finfun_snd_def)
   1.524  
   1.525 -lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
   1.526 -  and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
   1.527 +lemma finfun_snd_update: "finfun_snd (f(a $:= bc)) = (finfun_snd f)(a $:= snd bc)"
   1.528 +  and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(a $:= snd bc)"
   1.529  by(simp_all add: finfun_snd_def)
   1.530  
   1.531  lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
   1.532 @@ -1165,14 +1167,14 @@
   1.533  subsection {* Currying for FinFuns *}
   1.534  
   1.535  definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
   1.536 -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.537 +where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c)))"
   1.538  
   1.539 -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.540 +interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
   1.541  apply(unfold_locales)
   1.542  apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
   1.543  done
   1.544  
   1.545 -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.546 +interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
   1.547  proof(unfold_locales)
   1.548    fix b' b :: 'b
   1.549    assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
   1.550 @@ -1181,23 +1183,23 @@
   1.551      by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
   1.552    note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
   1.553    { fix A :: "('c \<times> 'a) set"
   1.554 -    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.555 +    interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b'"
   1.556        by(rule finfun_curry_aux.upd_left_comm)
   1.557      from fin have "finite A" by(auto intro: finite_subset)
   1.558 -    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.559 +    hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(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.560        by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
   1.561    from this[of UNIV]
   1.562 -  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.563 +  show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
   1.564      by(simp add: finfun_const_def)
   1.565  qed
   1.566  
   1.567 -lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
   1.568 +lemma finfun_curry_const [simp, code]: "finfun_curry (K$ c) = (K$ K$ c)"
   1.569  by(simp add: finfun_curry_def)
   1.570  
   1.571  lemma finfun_curry_update [simp]:
   1.572 -  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
   1.573 +  "finfun_curry (f((a, b) $:= c)) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
   1.574    and finfun_curry_update_code [code]:
   1.575 -  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
   1.576 +  "finfun_curry (finfun_update_code f (a, b) c) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
   1.577  by(simp_all add: finfun_curry_def)
   1.578  
   1.579  lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
   1.580 @@ -1208,7 +1210,7 @@
   1.581    have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
   1.582    hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
   1.583      by(auto simp add: curry_def fun_eq_iff)
   1.584 -  with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
   1.585 +  with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (K$ c)}"
   1.586      by(simp add: finfun_const_def finfun_curry)
   1.587    thus ?thesis unfolding finfun_def by auto
   1.588  qed
   1.589 @@ -1220,16 +1222,16 @@
   1.590  proof -
   1.591    have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
   1.592    proof(rule finfun_rec_unique)
   1.593 -    fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp
   1.594 +    fix c show "finfun_curry (K$ c) = (K$ K$ c)" by simp
   1.595      fix f a
   1.596 -    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.597 +    show "finfun_curry (f(a $:= c)) = (finfun_curry f)(fst a $:= (finfun_curry f $ (fst a))(snd a $:= c))"
   1.598        by(cases a) simp
   1.599 -    show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
   1.600 +    show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (K$ c)) a)) = (K$ K$ c)"
   1.601        by(simp add: finfun_curry_def finfun_const_def curry_def)
   1.602      fix g b
   1.603 -    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(\<^sup>f a := b)) aa)) =
   1.604 -      (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(\<^sup>f
   1.605 -      fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(\<^sup>f snd a := b))"
   1.606 +    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(a $:= b)) aa)) =
   1.607 +      (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(
   1.608 +      fst a $:= ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(snd a $:= b))"
   1.609        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.610    qed
   1.611    thus ?thesis by(auto simp add: fun_eq_iff)
   1.612 @@ -1254,10 +1256,11 @@
   1.613  definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
   1.614  where [simp, code del]: "finfun_clearjunk = id"
   1.615  
   1.616 -lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
   1.617 +lemma finfun_clearjunk_const [code]: "finfun_clearjunk (K$ b) = (K$ b)"
   1.618  by simp
   1.619  
   1.620 -lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
   1.621 +lemma finfun_clearjunk_update [code]: 
   1.622 +  "finfun_clearjunk (finfun_update_code f a b) = f(a $:= b)"
   1.623  by simp
   1.624  
   1.625  subsection {* The domain of a FinFun as a FinFun *}
   1.626 @@ -1266,7 +1269,7 @@
   1.627  where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)"
   1.628  
   1.629  lemma finfun_dom_const:
   1.630 -  "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
   1.631 +  "finfun_dom ((K$ c) :: 'a \<Rightarrow>f 'b) = (K$ finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
   1.632  unfolding finfun_dom_def finfun_default_const
   1.633  by(auto)(simp_all add: finfun_const_def)
   1.634  
   1.635 @@ -1276,8 +1279,8 @@
   1.636  *}
   1.637  
   1.638  lemma finfun_dom_const_code [code]:
   1.639 -  "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
   1.640 -   (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
   1.641 +  "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
   1.642 +   (if card_UNIV (TYPE('a)) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
   1.643  unfolding card_UNIV_eq_0_infinite_UNIV
   1.644  by(simp add: finfun_dom_const)
   1.645  
   1.646 @@ -1286,7 +1289,7 @@
   1.647  by(simp add: finfun_def exI[where x=False])
   1.648  
   1.649  lemma finfun_dom_update [simp]:
   1.650 -  "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
   1.651 +  "finfun_dom (f(a $:= b)) = (finfun_dom f)(a $:= (b \<noteq> finfun_default f))"
   1.652  including finfun unfolding finfun_dom_def finfun_update_def
   1.653  apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
   1.654  apply(fold finfun_update.rep_eq)
   1.655 @@ -1305,7 +1308,7 @@
   1.656        (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
   1.657  next
   1.658    case (update f a b)
   1.659 -  have "{x. finfun_dom f(\<^sup>f a := b) $ x} =
   1.660 +  have "{x. finfun_dom f(a $:= b) $ x} =
   1.661      (if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
   1.662      by (auto simp add: finfun_upd_apply split: split_if_asm)
   1.663    thus ?case using update by simp
   1.664 @@ -1328,20 +1331,20 @@
   1.665    thus ?thesis1 ?thesis2 ?thesis3 by simp_all
   1.666  qed
   1.667  
   1.668 -lemma finfun_const_False_conv_bot: "op $ (\<lambda>\<^isup>f False) = bot"
   1.669 +lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"
   1.670  by auto
   1.671  
   1.672 -lemma finfun_const_True_conv_top: "op $ (\<lambda>\<^isup>f True) = top"
   1.673 +lemma finfun_const_True_conv_top: "op $ (K$ True) = top"
   1.674  by auto
   1.675  
   1.676  lemma finfun_to_list_const:
   1.677 -  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>f 'b)) = 
   1.678 +  "finfun_to_list ((K$ c) :: ('a :: {linorder} \<Rightarrow>f 'b)) = 
   1.679    (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
   1.680  by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
   1.681  
   1.682  lemma finfun_to_list_const_code [code]:
   1.683 -  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
   1.684 -   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>f 'b))))"
   1.685 +  "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
   1.686 +   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
   1.687  unfolding card_UNIV_eq_0_infinite_UNIV
   1.688  by(auto simp add: finfun_to_list_const)
   1.689  
   1.690 @@ -1354,12 +1357,12 @@
   1.691  by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
   1.692  
   1.693  lemma finfun_to_list_update:
   1.694 -  "finfun_to_list (f(\<^sup>f a := b)) = 
   1.695 +  "finfun_to_list (f(a $:= b)) = 
   1.696    (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
   1.697  proof(subst finfun_to_list_def, rule the_equality)
   1.698    fix xs
   1.699 -  assume "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x} \<and> sorted xs \<and> distinct xs"
   1.700 -  hence eq: "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x}"
   1.701 +  assume "set xs = {x. finfun_dom f(a $:= b) $ x} \<and> sorted xs \<and> distinct xs"
   1.702 +  hence eq: "set xs = {x. finfun_dom f(a $:= b) $ x}"
   1.703      and [simp]: "sorted xs" "distinct xs" by simp_all
   1.704    show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
   1.705    proof(cases "b = finfun_default f")
   1.706 @@ -1372,7 +1375,7 @@
   1.707        proof(rule the_equality)
   1.708          have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
   1.709          also note eq also
   1.710 -        have "insert a {x. finfun_dom f(\<^sup>f a := b) $ x} = {x. finfun_dom f $ x}" using True
   1.711 +        have "insert a {x. finfun_dom f(a $:= b) $ x} = {x. finfun_dom f $ x}" using True
   1.712            by(auto simp add: finfun_upd_apply split: split_if_asm)
   1.713          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.714            by(simp add: sorted_insort_insert distinct_insort_insert)
   1.715 @@ -1385,7 +1388,7 @@
   1.716      next
   1.717        case False
   1.718        hence "f $ a = b" by(auto simp add: finfun_dom_conv)
   1.719 -      hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.720 +      hence f: "f(a $:= b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.721        from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
   1.722          by(auto elim: sorted_distinct_set_unique intro!: the_equality)
   1.723        with eq False show ?thesis unfolding f by(simp add: remove1_idem)
   1.724 @@ -1398,7 +1401,7 @@
   1.725        have "finfun_to_list f = xs"
   1.726          unfolding finfun_to_list_def
   1.727        proof(rule the_equality)
   1.728 -        have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
   1.729 +        have "finfun_dom f = finfun_dom f(a $:= b)" using False True
   1.730            by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.731          with eq show 1: "set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs"
   1.732            by(simp del: finfun_dom_update)
   1.733 @@ -1415,7 +1418,7 @@
   1.734        proof(rule the_equality)
   1.735          have "set (remove1 a xs) = set xs - {a}" by simp
   1.736          also note eq also
   1.737 -        have "{x. finfun_dom f(\<^sup>f a := b) $ x} - {a} = {x. finfun_dom f $ x}" using False
   1.738 +        have "{x. finfun_dom f(a $:= b) $ x} - {a} = {x. finfun_dom f $ x}" using False
   1.739            by(auto simp add: finfun_upd_apply split: split_if_asm)
   1.740          finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
   1.741            by(simp add: sorted_remove1)