diff -r 1edcd5f73505 -r 6c4b3e78f03e src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Wed May 30 09:36:39 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Wed May 30 09:46:58 2012 +0200
@@ -125,7 +125,7 @@
   hence "finite {c. g (y c) \<noteq> g b}"
   proof(induct "{a. y a \<noteq> b}" arbitrary: y)
     case empty
-    hence "y = (\<lambda>a. b)" by(auto intro: ext)
+    hence "y = (\<lambda>a. b)" by(auto)
     thus ?case by(simp)
   next
     case (insert x F)
@@ -342,7 +342,7 @@
     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)"
-        by(auto intro: ext)
+        by(auto)
       with insert show ?case
         by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
     qed(simp add: finfun_const_def) }
@@ -480,7 +480,7 @@
   from fin anf fg show ?thesis
   proof(induct "dom f" arbitrary: f)
     case empty
-    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
+    from `{} = dom f` have "f = empty" by(auto simp add: dom_def)
     thus ?case by(simp add: finfun_const_def upd_const_same)
   next
     case (insert a' A)
@@ -518,7 +518,7 @@
   from fin anf fg show ?thesis
   proof(induct "dom f" arbitrary: f)
     case empty
-    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
+    from `{} = dom f` have "f = empty" by(auto simp add: dom_def)
     thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
   next
     case (insert a' A)
@@ -544,7 +544,7 @@
 qed
 
 lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
-by(auto simp add: map_default_def restrict_map_def intro: ext)
+by(auto simp add: map_default_def restrict_map_def)
 
 lemma finite_rec_cong1:
   assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
@@ -619,7 +619,7 @@
     have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
     proof(cases "y a' = b")
       case True
-      with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
+      with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def)
       from True have a'ndomg: "a' \<notin> dom ?g" by auto
       from f b'b b show ?thesis unfolding g'
         by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
@@ -664,7 +664,7 @@
     let ?b = "map_default b ?g"
     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)
+    have ffmg': "map_default b ?g' = y(a' := b')" by(auto simp add: map_default_def restrict_map_def)
     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)
@@ -822,7 +822,7 @@
   proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
     case empty
     hence "\<And>a. y a = b" by blast
-    hence "y = (\<lambda>a. b)" by(auto intro: ext)
+    hence "y = (\<lambda>a. b)" by(auto)
     hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
     thus ?case by(simp add: const)
   next
@@ -915,8 +915,10 @@
 
 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. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
+definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "o$" 55)
+where [code del]: "g o$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
+
+notation (xsymbols) finfun_comp (infixr "\<circ>$" 55)
 
 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)
@@ -935,30 +937,31 @@
 qed
 
 lemma finfun_comp_const [simp, code]:
-  "g \<circ>\<^isub>f (K$ c) = (K$ g c)"
+  "g \<circ>$ (K$ c) = (K$ g c)"
 by(simp add: finfun_comp_def)
 
-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)"
+lemma finfun_comp_update [simp]: "g \<circ>$ (f(a $:= b)) = (g \<circ>$ f)(a $:= g b)"
+  and finfun_comp_update_code [code]: 
+  "g \<circ>$ (finfun_update_code f a b) = finfun_update_code (g \<circ>$ f) a (g b)"
 by(simp_all add: finfun_comp_def)
 
 lemma finfun_comp_apply [simp]:
-  "op $ (g \<circ>\<^isub>f f) = g \<circ> op $ f"
+  "op $ (g \<circ>$ f) = g \<circ> op $ f"
 by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply)
 
-lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
+lemma finfun_comp_comp_collapse [simp]: "f \<circ>$ g \<circ>$ h = (f \<circ> g) \<circ>$ h"
 by(induct h rule: finfun_weak_induct) simp_all
 
-lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (K$ c)"
+lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>$ 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"
+lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>$ f = f" "id \<circ>$ f = f"
 by(induct f rule: finfun_weak_induct) auto
 
-lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
+lemma finfun_comp_conv_comp: "g \<circ>$ f = Abs_finfun (g \<circ> op $ f)"
   including finfun
 proof -
-  have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
+  have "(\<lambda>f. g \<circ>$ f) = (\<lambda>f. Abs_finfun (g \<circ> op $ f))"
   proof(rule finfun_rec_unique)
     { 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) }
@@ -973,8 +976,10 @@
   thus ?thesis by(auto simp add: fun_eq_iff)
 qed
 
-definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "\<^sub>f\<circ>" 55)
-where [code del]: "finfun_comp2 g f = Abs_finfun (op $ g \<circ> f)"
+definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "$o" 55)
+where [code del]: "g $o f = Abs_finfun (op $ g \<circ> f)"
+
+notation (xsymbol) finfun_comp2 (infixr "$\<circ>" 55)
 
 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
   including finfun
@@ -1029,7 +1034,7 @@
 
 
 definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool"
-where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
+where "finfun_Ex P = Not (finfun_All (Not \<circ>$ P))"
 
 lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)"
 unfolding finfun_Ex_def finfun_All_All by simp
@@ -1041,27 +1046,27 @@
 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(a $:= (b, g $ a))) f"
+where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
 
-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))"
+interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>$ 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(a $:= (b, g $ a))"
+interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>$ 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(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(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>$ 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(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>$ g) UNIV = Pair b' \<circ>$ g"
     by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
 qed
 
-lemma finfun_Diag_const1: "(K$ b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
+lemma finfun_Diag_const1: "(K$ b, g)\<^sup>f = Pair b \<circ>$ g"
 by(simp add: finfun_Diag_def)
 
 text {*
@@ -1077,7 +1082,7 @@
   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, K$ 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>$ 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(a $:= c))\<^sup>f = (f, g)\<^sup>f(a $:= (f $ a, c))"
@@ -1107,7 +1112,7 @@
 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. ((K$ 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>$ g"
         by(simp add: finfun_comp_conv_comp o_def finfun_const_def) }
     { fix g' a b
       show "Abs_finfun (\<lambda>x. (g'(a $:= b) $ x, g $ x)) =
@@ -1121,7 +1126,7 @@
 by(auto simp add: expand_finfun_eq fun_eq_iff)
 
 definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b"
-where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
+where [code]: "finfun_fst f = fst \<circ>$ f"
 
 lemma finfun_fst_const: "finfun_fst (K$ bc) = (K$ fst bc)"
 by(simp add: finfun_fst_def)
@@ -1130,18 +1135,18 @@
   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"
+lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>$ g) = (fst \<circ> f) \<circ>$ g"
 by(simp add: finfun_fst_def)
 
 lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
 by(induct f rule: finfun_weak_induct)(simp_all add: finfun_Diag_const1 finfun_fst_comp_conv o_def finfun_Diag_update1 finfun_fst_update)
 
-lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o finfun_apply f))"
+lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst \<circ> op $ f))"
 by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp)
 
 
 definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c"
-where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
+where [code]: "finfun_snd f = snd \<circ>$ f"
 
 lemma finfun_snd_const: "finfun_snd (K$ bc) = (K$ snd bc)"
 by(simp add: finfun_snd_def)
@@ -1150,7 +1155,7 @@
   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"
+lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>$ g) = (snd \<circ> f) \<circ>$ g"
 by(simp add: finfun_snd_def)
 
 lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
@@ -1158,7 +1163,7 @@
 apply(auto simp add: finfun_Diag_const1 finfun_snd_comp_conv o_def finfun_Diag_update1 finfun_snd_update finfun_upd_apply intro: finfun_ext)
 done
 
-lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o finfun_apply f))"
+lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd \<circ> op $ f))"
 by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp)
 
 lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
@@ -1239,11 +1244,11 @@
 
 subsection {* Executable equality for FinFuns *}
 
-lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
+lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ (f, g)\<^sup>f)"
 by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
 
 instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
-definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
+definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ (f, g)\<^sup>f)"
 instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
 end