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