# HG changeset patch
# User Andreas Lochbihler
# Date 1338363399 -7200
# Node ID 1edcd5f73505e0779fa906fc5d63c11d2076a083
# Parent  2f9584581cf20e0ac02a52aec0ed962da11c08be
FinFun pseudo-constructor syntax without superscripts

diff -r 2f9584581cf2 -r 1edcd5f73505 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Wed May 30 09:13:39 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Wed May 30 09:36:39 2012 +0200
@@ -278,35 +278,35 @@
 
 subsection {* Kernel functions for type @{typ "'a \<Rightarrow>f 'b"} *}
 
-lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
+lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("K$/ _" [0] 1)
 is "\<lambda> b x. b" by (rule const_finfun)
 
-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"
+lift_definition finfun_update :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(_ $:= _')" [1000,0,0] 1000) is "fun_upd"
 by (simp add: fun_upd_finfun)
 
-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)"
+lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(a $:= b)(a' $:= b') = f(a' $:= b')(a $:= b)"
 by transfer (simp add: fun_upd_twist)
 
 lemma finfun_update_twice [simp]:
-  "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
+  "f(a $:= b)(a $:= b') = f(a $:= b')"
 by transfer simp
 
-lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
+lemma finfun_update_const_same: "(K$ b)(a $:= b) = (K$ b)"
 by transfer (simp add: fun_eq_iff)
 
 subsection {* Code generator setup *}
 
-definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
+definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
 where [simp, code del]: "finfun_update_code = finfun_update"
 
 code_datatype finfun_const finfun_update_code
 
 lemma finfun_update_const_code [code]:
-  "(\<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')"
+  "(K$ b)(a $:= b') = (if b = b' then (K$ b) else finfun_update_code (K$ b) a b')"
 by(simp add: finfun_update_const_same)
 
 lemma finfun_update_update_code [code]:
-  "(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)"
+  "(finfun_update_code f a b)(a' $:= b') = (if a = a' then f(a $:= b') else finfun_update_code (f(a' $:= b')) a b)"
 by(simp add: finfun_update_twist)
 
 
@@ -316,29 +316,29 @@
 
 subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
 
-interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
+interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')"
   including finfun
 proof
   fix a a' :: 'a
-  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'))"
+  show "(\<lambda>f. f(a $:= b')) \<circ> (\<lambda>f. f(a' $:= b')) = (\<lambda>f. f(a' $:= b')) \<circ> (\<lambda>f. f(a $:= b'))"
   proof
     fix b
     have "(finfun_apply b)(a := b', a' := b') = (finfun_apply b)(a' := b', a := b')"
       by(cases "a = a'")(auto simp add: fun_upd_twist)
-    then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
+    then have "b(a $:= b')(a' $:= b') = b(a' $:= b')(a $:= b')"
       by(auto simp add: finfun_update_def fun_upd_twist)
-    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"
+    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"
       by (simp add: fun_eq_iff)
   qed
 qed
 
 lemma fold_finfun_update_finite_univ:
   assumes fin: "finite (UNIV :: 'a set)"
-  shows "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
+  shows "Finite_Set.fold (\<lambda>a f. f(a $:= b')) (K$ b) (UNIV :: 'a set) = (K$ b')"
 proof -
   { fix A :: "'a set"
     from fin have "finite A" by(auto intro: finite_subset)
-    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)"
+    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)"
     proof(induct)
       case (insert x F)
       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)"
@@ -427,15 +427,15 @@
 lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
 by transfer (erule finite_finfun_default_aux)
 
-lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
+lemma finfun_default_const: "finfun_default ((K$ b) :: 'a \<Rightarrow>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
 by(transfer)(auto simp add: finfun_default_aux_infinite finfun_default_aux_def)
 
 lemma finfun_default_update_const:
-  "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
+  "finfun_default (f(a $:= b)) = finfun_default f"
 by transfer (simp add: finfun_default_aux_update_const)
 
 lemma finfun_default_const_code [code]:
-  "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
+  "finfun_default ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
 by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
 
 lemma finfun_default_update_code [code]:
@@ -573,7 +573,7 @@
 qed
 
 lemma finfun_rec_upd [simp]:
-  "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
+  "finfun_rec cnst upd (f(a' $:= b')) = upd a' b' (finfun_rec cnst upd f)"
   including finfun
 proof -
   obtain b where b: "b = finfun_default f" by auto
@@ -637,15 +637,15 @@
       also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
       finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
     qed
-    also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
+    also have "The (?the (f(a' $:= b'))) = ?g'"
     proof(rule the_equality)
-      from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
+      from f y b b'b brang' fing' show "?the (f(a' $:= b')) ?g'"
         by(auto simp del: fun_upd_apply simp add: finfun_update_def)
     next
       fix g'
-      assume "?the (f(\<^sup>f a' := b')) g'"
+      assume "?the (f(a' $:= b')) g'"
       hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
-        and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')" 
+        and eq: "f(a' $:= b') = Abs_finfun (map_default b g')" 
         by(auto simp del: fun_upd_apply)
       from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
         by(blast intro: map_default_in_finfun)+
@@ -665,13 +665,14 @@
     from fing have fing': "finite (dom ?g')" by auto
     from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
     have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
-    with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
-    have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
+    with f y have f_Abs: "f(a' $:= b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
+    have g': "The (?the (f(a' $:= b'))) = ?g'"
     proof (rule the_equality)
-      from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
+      from fing' bnrang' f_Abs show "?the (f(a' $:= b')) ?g'"
+        by(auto simp add: finfun_update_def restrict_map_def)
     next
-      fix g' assume "?the (f(\<^sup>f a' := b')) g'"
-      hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
+      fix g' assume "?the (f(a' $:= b')) g'"
+      hence f': "f(a' $:= b') = Abs_finfun (map_default b g')"
         and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
       from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
         by(auto intro: map_default_in_finfun)
@@ -716,7 +717,8 @@
                                      unfolded this, OF fing'' a'ndomg'' g''leg]
         also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
         from upd_left_comm upd_left_comm fing''
-        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'')"
+        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'')"
           by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
         with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
                      upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
@@ -740,18 +742,18 @@
 begin
 
 lemma finfun_rec_const [simp]: includes finfun shows
-  "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
+  "finfun_rec cnst upd (K$ c) = cnst c"
 proof(cases "finite (UNIV :: 'a set)")
   case False
-  hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
-  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"
+  hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
+  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"
   proof (rule the_equality)
-    show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
+    show "(K$ c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
       by(auto simp add: finfun_const_def)
   next
     fix g :: "'a \<rightharpoonup> 'b"
-    assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
-    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+
+    assume "(K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
+    hence g: "(K$ c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
     from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
       by(simp add: finfun_const_def)
     moreover have "map_default c empty = (\<lambda>a. c)" by simp
@@ -760,8 +762,8 @@
   ultimately show ?thesis by(simp add: finfun_rec_def)
 next
   case True
-  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = undefined" by(simp add: finfun_default_const)
-  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"
+  hence default: "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = undefined" by(simp add: finfun_default_const)
+  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
   show ?thesis
   proof(cases "c = undefined")
     case True
@@ -771,7 +773,7 @@
     next
       fix g'
       assume "?the g'"
-      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
+      hence fg: "(K$ c) = Abs_finfun (map_default undefined g')"
         and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
       from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
       with fg have "map_default undefined g' = (\<lambda>a. c)"
@@ -790,7 +792,7 @@
     next
       fix g' :: "'a \<rightharpoonup> 'b"
       assume "?the g'"
-      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
+      hence fg: "(K$ c) = Abs_finfun (map_default undefined g')"
         and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
       from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
       with fg have "map_default undefined g' = (\<lambda>a. c)"
@@ -809,8 +811,8 @@
 subsection {* Weak induction rule and case analysis for FinFuns *}
 
 lemma finfun_weak_induct [consumes 0, case_names const update]:
-  assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
-  and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
+  assumes const: "\<And>b. P (K$ b)"
+  and update: "\<And>f a b. P f \<Longrightarrow> P (f(a $:= b))"
   shows "P x"
   including finfun
 proof(induct x rule: Abs_finfun_induct)
@@ -838,16 +840,16 @@
 by(induct x rule: finfun_weak_induct) blast+
 
 lemma finfun_exhaust:
-  obtains b where "x = (\<lambda>\<^isup>f b)"
-        | f a b where "x = f(\<^sup>f a := b)"
+  obtains b where "x = (K$ b)"
+        | f a b where "x = f(a $:= b)"
 by(atomize_elim)(rule finfun_exhaust_disj)
 
 lemma finfun_rec_unique:
   fixes f :: "'a \<Rightarrow>f 'b \<Rightarrow> 'c"
-  assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
-  and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
-  and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
-  and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
+  assumes c: "\<And>c. f (K$ c) = cnst c"
+  and u: "\<And>g a b. f (g(a $:= b)) = upd g a b (f g)"
+  and c': "\<And>c. f' (K$ c) = cnst c"
+  and u': "\<And>g a b. f' (g(a $:= b)) = upd g a b (f' g)"
   shows "f = f'"
 proof
   fix g :: "'a \<Rightarrow>f 'b"
@@ -877,25 +879,25 @@
 
 lemma finfun_apply_def: "op $ = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
 proof(rule finfun_rec_unique)
-  fix c show "op $ (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
+  fix c show "op $ (K$ c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq)
 next
-  fix g a b show "op $ g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else g $ c)"
+  fix g a b show "op $ g(a $:= b) = (\<lambda>c. if c = a then b else g $ c)"
     by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply)
 qed auto
 
-lemma finfun_upd_apply: "f(\<^sup>fa := b) $ a' = (if a = a' then b else f $ a')"
+lemma finfun_upd_apply: "f(a $:= b) $ a' = (if a = a' then b else f $ a')"
   and finfun_upd_apply_code [code]: "(finfun_update_code f a b) $ a' = (if a = a' then b else f $ a')"
 by(simp_all add: finfun_apply_def)
 
-lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b) $ a = b"
+lemma finfun_const_apply [simp, code]: "(K$ b) $ a = b"
 by(simp add: finfun_apply_def)
 
 lemma finfun_upd_apply_same [simp]:
-  "f(\<^sup>fa := b) $ a = b"
+  "f(a $:= b) $ a = b"
 by(simp add: finfun_upd_apply)
 
 lemma finfun_upd_apply_other [simp]:
-  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b) $ a' = f $ a'"
+  "a \<noteq> a' \<Longrightarrow> f(a $:= b) $ a' = f $ a'"
 by(simp add: finfun_upd_apply)
 
 lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g"
@@ -904,39 +906,39 @@
 lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
 by(auto intro: finfun_ext)
 
-lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
+lemma finfun_const_inject [simp]: "(K$ b) = (K$ b') \<equiv> b = b'"
 by(simp add: expand_finfun_eq fun_eq_iff)
 
 lemma finfun_const_eq_update:
-  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
+  "((K$ b) = f(a $:= b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
 by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
 
 subsection {* Function composition *}
 
 definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "\<circ>\<^isub>f" 55)
-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"
+where [code del]: "g \<circ>\<^isub>f f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
 
-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))"
+interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
 
-interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
+interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
 proof
   fix b' b :: 'a
   assume fin: "finite (UNIV :: 'c set)"
   { fix A :: "'c set"
     from fin have "finite A" by(auto intro: finite_subset)
-    hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
+    hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) A =
       Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
       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) }
-  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')"
+  from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) UNIV = (K$ g b')"
     by(simp add: finfun_const_def)
 qed
 
 lemma finfun_comp_const [simp, code]:
-  "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
+  "g \<circ>\<^isub>f (K$ c) = (K$ g c)"
 by(simp add: finfun_comp_def)
 
-lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
+lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(a $:= b)) = (g \<circ>\<^isub>f f)(a $:= g b)"
   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)"
 by(simp_all add: finfun_comp_def)
 
@@ -947,7 +949,7 @@
 lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
 by(induct h rule: finfun_weak_induct) simp_all
 
-lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
+lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (K$ c)"
 by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
 
 lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
@@ -958,9 +960,9 @@
 proof -
   have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
   proof(rule finfun_rec_unique)
-    { fix c show "Abs_finfun (g \<circ> op $ (\<lambda>\<^isup>f c)) = (\<lambda>\<^isup>f g c)"
+    { fix c show "Abs_finfun (g \<circ> op $ (K$ c)) = (K$ g c)"
         by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
-    { 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)"
+    { fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
       proof -
         obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
         moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
@@ -974,14 +976,14 @@
 definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "\<^sub>f\<circ>" 55)
 where [code del]: "finfun_comp2 g f = Abs_finfun (op $ g \<circ> f)"
 
-lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
+lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
   including finfun
 by(simp add: finfun_comp2_def finfun_const_def comp_def)
 
 lemma finfun_comp2_update:
   includes finfun
   assumes inj: "inj f"
-  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)"
+  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)"
 proof(cases "b \<in> range f")
   case True
   from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
@@ -997,15 +999,15 @@
 definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
 where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a"
 
-lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
+lemma finfun_All_except_const: "finfun_All_except A (K$ b) \<longleftrightarrow> b \<or> set A = UNIV"
 by(auto simp add: finfun_All_except_def)
 
 lemma finfun_All_except_const_finfun_UNIV_code [code]:
-  "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
+  "finfun_All_except A (K$ b) = (b \<or> is_list_UNIV A)"
 by(simp add: finfun_All_except_const is_list_UNIV_iff)
 
 lemma finfun_All_except_update:
-  "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
+  "finfun_All_except A f(a $:= b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
 by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
 
 lemma finfun_All_except_update_code [code]:
@@ -1016,10 +1018,10 @@
 definition finfun_All :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
 where "finfun_All = finfun_All_except []"
 
-lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
+lemma finfun_All_const [simp]: "finfun_All (K$ b) = b"
 by(simp add: finfun_All_def finfun_All_except_def)
 
-lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
+lemma finfun_All_update: "finfun_All f(a $:= b) = (b \<and> finfun_All_except [a] f)"
 by(simp add: finfun_All_def finfun_All_except_update)
 
 lemma finfun_All_All: "finfun_All P = All (op $ P)"
@@ -1032,34 +1034,34 @@
 lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
 unfolding finfun_Ex_def finfun_All_All by simp
 
-lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
+lemma finfun_Ex_const [simp]: "finfun_Ex (K$ b) = b"
 by(simp add: finfun_Ex_def)
 
 
 subsection {* A diagonal operator for FinFuns *}
 
 definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
-where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g $ a))) f"
+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"
 
-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))"
+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))"
 by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
 
-interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g $ a))"
+interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(a $:= (b, g $ a))"
 proof
   fix b' b :: 'a
   assume fin: "finite (UNIV :: 'c set)"
   { fix A :: "'c set"
-    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
+    interpret comp_fun_commute "\<lambda>a c. c(a $:= (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm)
     from fin have "finite A" by(auto intro: finite_subset)
-    hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g $ a))) (Pair b \<circ>\<^isub>f g) A =
+    hence "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>\<^isub>f g) A =
       Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))"
       by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
                  auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
-  from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g $ a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
+  from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
     by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
 qed
 
-lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
+lemma finfun_Diag_const1: "(K$ b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
 by(simp add: finfun_Diag_def)
 
 text {*
@@ -1067,33 +1069,33 @@
 *}
 
 lemma finfun_Diag_const_code [code]:
-  "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
-  "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
+  "(K$ b, K$ c)\<^sup>f = (K$ (b, c))"
+  "(K$ b, finfun_update_code g a c)\<^sup>f = finfun_update_code (K$ b, g)\<^sup>f a (b, c)"
 by(simp_all add: finfun_Diag_const1)
 
-lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))"
-  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))"
+lemma finfun_Diag_update1: "(f(a $:= b), g)\<^sup>f = (f, g)\<^sup>f(a $:= (b, g $ a))"
+  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(a $:= (b, g $ a))"
 by(simp_all add: finfun_Diag_def)
 
-lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
+lemma finfun_Diag_const2: "(f, K$ c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
 
-lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f $ a, c))"
+lemma finfun_Diag_update2: "(f, g(a $:= c))\<^sup>f = (f, g)\<^sup>f(a $:= (f $ a, c))"
 by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
 
-lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
+lemma finfun_Diag_const_const [simp]: "(K$ b, K$ c)\<^sup>f = (K$ (b, c))"
 by(simp add: finfun_Diag_const1)
 
 lemma finfun_Diag_const_update:
-  "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
+  "(K$ b, g(a $:= c))\<^sup>f = (K$ b, g)\<^sup>f(a $:= (b, c))"
 by(simp add: finfun_Diag_const1)
 
 lemma finfun_Diag_update_const:
-  "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
+  "(f(a $:= b), K$ c)\<^sup>f = (f, K$ c)\<^sup>f(a $:= (b, c))"
 by(simp add: finfun_Diag_def)
 
 lemma finfun_Diag_update_update:
-  "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g $ a))(\<^sup>f a' := (f $ a', c)))"
+  "(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)))"
 by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
 
 lemma finfun_Diag_apply [simp]: "op $ (f, g)\<^sup>f = (\<lambda>x. (f $ x, g $ x))"
@@ -1105,11 +1107,11 @@
 proof -
   have "(\<lambda>f :: 'a \<Rightarrow>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))"
   proof(rule finfun_rec_unique)
-    { fix c show "Abs_finfun (\<lambda>x. ((\<lambda>\<^isup>f c) $ x, g $ x)) = Pair c \<circ>\<^isub>f g"
+    { fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>\<^isub>f g"
         by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
     { fix g' a b
-      show "Abs_finfun (\<lambda>x. (g'(\<^sup>f a := b) $ x, g $ x)) =
-            (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(\<^sup>f a := (b, g $ a))"
+      show "Abs_finfun (\<lambda>x. (g'(a $:= b) $ x, g $ x)) =
+            (Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(a $:= (b, g $ a))"
         by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp }
   qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
   thus ?thesis by(auto simp add: fun_eq_iff)
@@ -1121,11 +1123,11 @@
 definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
 where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
 
-lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
+lemma finfun_fst_const: "finfun_fst (K$ bc) = (K$ fst bc)"
 by(simp add: finfun_fst_def)
 
-lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
-  and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
+lemma finfun_fst_update: "finfun_fst (f(a $:= bc)) = (finfun_fst f)(a $:= fst bc)"
+  and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(a $:= fst bc)"
 by(simp_all add: finfun_fst_def)
 
 lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
@@ -1141,11 +1143,11 @@
 definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
 where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
 
-lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
+lemma finfun_snd_const: "finfun_snd (K$ bc) = (K$ snd bc)"
 by(simp add: finfun_snd_def)
 
-lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
-  and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
+lemma finfun_snd_update: "finfun_snd (f(a $:= bc)) = (finfun_snd f)(a $:= snd bc)"
+  and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(a $:= snd bc)"
 by(simp_all add: finfun_snd_def)
 
 lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
@@ -1165,14 +1167,14 @@
 subsection {* Currying for FinFuns *}
 
 definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
-where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c)))"
+where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c)))"
 
-interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))"
+interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
 apply(unfold_locales)
 apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
 done
 
-interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))"
+interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))"
 proof(unfold_locales)
   fix b' b :: 'b
   assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
@@ -1181,23 +1183,23 @@
     by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
   note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
   { fix A :: "('c \<times> 'a) set"
-    interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))) a b'"
+    interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b'"
       by(rule finfun_curry_aux.upd_left_comm)
     from fin have "finite A" by(auto intro: finite_subset)
-    hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))"
+    hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(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))"
       by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) }
   from this[of UNIV]
-  show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f $ a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
+  show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
     by(simp add: finfun_const_def)
 qed
 
-lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
+lemma finfun_curry_const [simp, code]: "finfun_curry (K$ c) = (K$ K$ c)"
 by(simp add: finfun_curry_def)
 
 lemma finfun_curry_update [simp]:
-  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
+  "finfun_curry (f((a, b) $:= c)) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
   and finfun_curry_update_code [code]:
-  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := (finfun_curry f $ a)(\<^sup>f b := c))"
+  "finfun_curry (finfun_update_code f (a, b) c) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))"
 by(simp_all add: finfun_curry_def)
 
 lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
@@ -1208,7 +1210,7 @@
   have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
   hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
     by(auto simp add: curry_def fun_eq_iff)
-  with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
+  with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (K$ c)}"
     by(simp add: finfun_const_def finfun_curry)
   thus ?thesis unfolding finfun_def by auto
 qed
@@ -1220,16 +1222,16 @@
 proof -
   have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))"
   proof(rule finfun_rec_unique)
-    fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp
+    fix c show "finfun_curry (K$ c) = (K$ K$ c)" by simp
     fix f a
-    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))"
+    show "finfun_curry (f(a $:= c)) = (finfun_curry f)(fst a $:= (finfun_curry f $ (fst a))(snd a $:= c))"
       by(cases a) simp
-    show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
+    show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (K$ c)) a)) = (K$ K$ c)"
       by(simp add: finfun_curry_def finfun_const_def curry_def)
     fix g b
-    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(\<^sup>f a := b)) aa)) =
-      (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(\<^sup>f
-      fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(\<^sup>f snd a := b))"
+    show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(a $:= b)) aa)) =
+      (Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))(
+      fst a $:= ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(snd a $:= b))"
       by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_Abs_finfun_curry)
   qed
   thus ?thesis by(auto simp add: fun_eq_iff)
@@ -1254,10 +1256,11 @@
 definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
 where [simp, code del]: "finfun_clearjunk = id"
 
-lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
+lemma finfun_clearjunk_const [code]: "finfun_clearjunk (K$ b) = (K$ b)"
 by simp
 
-lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
+lemma finfun_clearjunk_update [code]: 
+  "finfun_clearjunk (finfun_update_code f a b) = f(a $:= b)"
 by simp
 
 subsection {* The domain of a FinFun as a FinFun *}
@@ -1266,7 +1269,7 @@
 where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)"
 
 lemma finfun_dom_const:
-  "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
+  "finfun_dom ((K$ c) :: 'a \<Rightarrow>f 'b) = (K$ finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
 unfolding finfun_dom_def finfun_default_const
 by(auto)(simp_all add: finfun_const_def)
 
@@ -1276,8 +1279,8 @@
 *}
 
 lemma finfun_dom_const_code [code]:
-  "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
-   (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
+  "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
+   (if card_UNIV (TYPE('a)) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
 unfolding card_UNIV_eq_0_infinite_UNIV
 by(simp add: finfun_dom_const)
 
@@ -1286,7 +1289,7 @@
 by(simp add: finfun_def exI[where x=False])
 
 lemma finfun_dom_update [simp]:
-  "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
+  "finfun_dom (f(a $:= b)) = (finfun_dom f)(a $:= (b \<noteq> finfun_default f))"
 including finfun unfolding finfun_dom_def finfun_update_def
 apply(simp add: finfun_default_update_const fun_upd_apply finfun_dom_finfunI)
 apply(fold finfun_update.rep_eq)
@@ -1305,7 +1308,7 @@
       (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
 next
   case (update f a b)
-  have "{x. finfun_dom f(\<^sup>f a := b) $ x} =
+  have "{x. finfun_dom f(a $:= b) $ x} =
     (if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})"
     by (auto simp add: finfun_upd_apply split: split_if_asm)
   thus ?case using update by simp
@@ -1328,20 +1331,20 @@
   thus ?thesis1 ?thesis2 ?thesis3 by simp_all
 qed
 
-lemma finfun_const_False_conv_bot: "op $ (\<lambda>\<^isup>f False) = bot"
+lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"
 by auto
 
-lemma finfun_const_True_conv_top: "op $ (\<lambda>\<^isup>f True) = top"
+lemma finfun_const_True_conv_top: "op $ (K$ True) = top"
 by auto
 
 lemma finfun_to_list_const:
-  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>f 'b)) = 
+  "finfun_to_list ((K$ c) :: ('a :: {linorder} \<Rightarrow>f 'b)) = 
   (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
 by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
 
 lemma finfun_to_list_const_code [code]:
-  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
-   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>f 'b))))"
+  "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
+   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
 unfolding card_UNIV_eq_0_infinite_UNIV
 by(auto simp add: finfun_to_list_const)
 
@@ -1354,12 +1357,12 @@
 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
 
 lemma finfun_to_list_update:
-  "finfun_to_list (f(\<^sup>f a := b)) = 
+  "finfun_to_list (f(a $:= b)) = 
   (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
 proof(subst finfun_to_list_def, rule the_equality)
   fix xs
-  assume "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x} \<and> sorted xs \<and> distinct xs"
-  hence eq: "set xs = {x. finfun_dom f(\<^sup>f a := b) $ x}"
+  assume "set xs = {x. finfun_dom f(a $:= b) $ x} \<and> sorted xs \<and> distinct xs"
+  hence eq: "set xs = {x. finfun_dom f(a $:= b) $ x}"
     and [simp]: "sorted xs" "distinct xs" by simp_all
   show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
   proof(cases "b = finfun_default f")
@@ -1372,7 +1375,7 @@
       proof(rule the_equality)
         have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
         also note eq also
-        have "insert a {x. finfun_dom f(\<^sup>f a := b) $ x} = {x. finfun_dom f $ x}" using True
+        have "insert a {x. finfun_dom f(a $:= b) $ x} = {x. finfun_dom f $ x}" using True
           by(auto simp add: finfun_upd_apply split: split_if_asm)
         finally show 1: "set (insort_insert a xs) = {x. finfun_dom f $ x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
           by(simp add: sorted_insort_insert distinct_insort_insert)
@@ -1385,7 +1388,7 @@
     next
       case False
       hence "f $ a = b" by(auto simp add: finfun_dom_conv)
-      hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
+      hence f: "f(a $:= b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
       from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
         by(auto elim: sorted_distinct_set_unique intro!: the_equality)
       with eq False show ?thesis unfolding f by(simp add: remove1_idem)
@@ -1398,7 +1401,7 @@
       have "finfun_to_list f = xs"
         unfolding finfun_to_list_def
       proof(rule the_equality)
-        have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
+        have "finfun_dom f = finfun_dom f(a $:= b)" using False True
           by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
         with eq show 1: "set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs"
           by(simp del: finfun_dom_update)
@@ -1415,7 +1418,7 @@
       proof(rule the_equality)
         have "set (remove1 a xs) = set xs - {a}" by simp
         also note eq also
-        have "{x. finfun_dom f(\<^sup>f a := b) $ x} - {a} = {x. finfun_dom f $ x}" using False
+        have "{x. finfun_dom f(a $:= b) $ x} - {a} = {x. finfun_dom f $ x}" using False
           by(auto simp add: finfun_upd_apply split: split_if_asm)
         finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
           by(simp add: sorted_remove1)
diff -r 2f9584581cf2 -r 1edcd5f73505 src/HOL/ex/FinFunPred.thy
--- a/src/HOL/ex/FinFunPred.thy	Wed May 30 09:13:39 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Wed May 30 09:36:39 2012 +0200
@@ -108,7 +108,7 @@
 where "finfun_UNIV \<equiv> top"
 
 definition finfun_single :: "'a \<Rightarrow> 'a pred\<^isub>f"
-where [code]: "finfun_single x = finfun_empty(\<^sup>f x := True)"
+where [code]: "finfun_single x = finfun_empty(x $:= True)"
 
 lemma finfun_single_apply [simp]:
   "finfun_single x $ y \<longleftrightarrow> x = y"
@@ -133,15 +133,15 @@
 where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A $ a \<longrightarrow> a \<in> set xs \<or> P a)"
 
 lemma finfun_Ball_except_const:
-  "finfun_Ball_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (\<lambda>\<^isup>f b) P)"
+  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
 by(auto simp add: finfun_Ball_except_def)
 
 lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
-  "finfun_Ball_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (\<lambda>\<^isup>f b) P)"
+  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
 by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff)
 
 lemma finfun_Ball_except_update:
-  "finfun_Ball_except xs (A(\<^sup>f a := b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)"
+  "finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)"
 by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: split_if_asm)
 
 lemma finfun_Ball_except_update_code [code]:
@@ -160,15 +160,15 @@
 where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A $ a \<and> a \<notin> set xs \<and> P a)"
 
 lemma finfun_Bex_except_const:
-  "finfun_Bex_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (\<lambda>\<^isup>f b) P)"
+  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
 by(auto simp add: finfun_Bex_except_def)
 
 lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
-  "finfun_Bex_except xs (\<lambda>\<^isup>f b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (\<lambda>\<^isup>f b) P)"
+  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
 by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff)
 
 lemma finfun_Bex_except_update: 
-  "finfun_Bex_except xs (A(\<^sup>f a := b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P"
+  "finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P"
 by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: split_if_asm)
 
 lemma finfun_Bex_except_update_code [code]:
@@ -223,7 +223,7 @@
 
 lemma iso_finfun_upd [code_unfold]:
   fixes A :: "'a pred\<^isub>f"
-  shows "(op $ A)(x := b) = op $ (A(\<^sup>f x := b))"
+  shows "(op $ A)(x := b) = op $ (A(x $:= b))"
 by(simp add: fun_eq_iff)
 
 lemma iso_finfun_uminus [code_unfold]: