author | hoelzl |
Fri, 19 Feb 2016 13:40:50 +0100 | |
changeset 62378 | 85ed00c1fe7c |
parent 61955 | e96292f32c3c |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
48028 | 1 |
(* Author: Andreas Lochbihler, Uni Karlsruhe *) |
2 |
||
60500 | 3 |
section \<open>Almost everywhere constant functions\<close> |
48028 | 4 |
|
5 |
theory FinFun |
|
48051 | 6 |
imports Cardinality |
48028 | 7 |
begin |
8 |
||
60500 | 9 |
text \<open> |
48028 | 10 |
This theory defines functions which are constant except for finitely |
11 |
many points (FinFun) and introduces a type finfin along with a |
|
12 |
number of operators for them. The code generator is set up such that |
|
13 |
such functions can be represented as data in the generated code and |
|
14 |
all operators are executable. |
|
15 |
||
16 |
For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009. |
|
60500 | 17 |
\<close> |
48028 | 18 |
|
19 |
||
61585 | 20 |
subsection \<open>The \<open>map_default\<close> operation\<close> |
48028 | 21 |
|
22 |
definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
23 |
where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'" |
|
24 |
||
25 |
lemma map_default_delete [simp]: |
|
26 |
"map_default b (f(a := None)) = (map_default b f)(a := b)" |
|
27 |
by(simp add: map_default_def fun_eq_iff) |
|
28 |
||
29 |
lemma map_default_insert: |
|
30 |
"map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')" |
|
31 |
by(simp add: map_default_def fun_eq_iff) |
|
32 |
||
33 |
lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)" |
|
34 |
by(simp add: fun_eq_iff map_default_def) |
|
35 |
||
36 |
lemma map_default_inject: |
|
37 |
fixes g g' :: "'a \<rightharpoonup> 'b" |
|
38 |
assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'" |
|
39 |
and fin: "finite (dom g)" and b: "b \<notin> ran g" |
|
40 |
and fin': "finite (dom g')" and b': "b' \<notin> ran g'" |
|
41 |
and eq': "map_default b g = map_default b' g'" |
|
42 |
shows "b = b'" "g = g'" |
|
43 |
proof - |
|
44 |
from infin_eq show bb': "b = b'" |
|
45 |
proof |
|
46 |
assume infin: "\<not> finite (UNIV :: 'a set)" |
|
47 |
from fin fin' have "finite (dom g \<union> dom g')" by auto |
|
48 |
with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset) |
|
49 |
then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto |
|
50 |
hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def) |
|
51 |
with eq' show "b = b'" by simp |
|
52 |
qed |
|
53 |
||
54 |
show "g = g'" |
|
55 |
proof |
|
56 |
fix x |
|
57 |
show "g x = g' x" |
|
58 |
proof(cases "g x") |
|
59 |
case None |
|
60 |
hence "map_default b g x = b" by(simp add: map_default_def) |
|
61 |
with bb' eq' have "map_default b' g' x = b'" by simp |
|
62 |
with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm) |
|
63 |
with None show ?thesis by simp |
|
64 |
next |
|
65 |
case (Some c) |
|
66 |
with b have cb: "c \<noteq> b" by(auto simp add: ran_def) |
|
67 |
moreover from Some have "map_default b g x = c" by(simp add: map_default_def) |
|
68 |
with eq' have "map_default b' g' x = c" by simp |
|
69 |
ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits) |
|
70 |
with Some show ?thesis by simp |
|
71 |
qed |
|
72 |
qed |
|
73 |
qed |
|
74 |
||
60500 | 75 |
subsection \<open>The finfun type\<close> |
48028 | 76 |
|
77 |
definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}" |
|
78 |
||
61384 | 79 |
typedef ('a,'b) finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set" |
48029 | 80 |
morphisms finfun_apply Abs_finfun |
48028 | 81 |
proof - |
82 |
have "\<exists>f. finite {x. f x \<noteq> undefined}" |
|
83 |
proof |
|
84 |
show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto |
|
85 |
qed |
|
86 |
then show ?thesis unfolding finfun_def by auto |
|
87 |
qed |
|
88 |
||
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
89 |
type_notation finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) |
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
90 |
|
48028 | 91 |
setup_lifting type_definition_finfun |
92 |
||
93 |
lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun" |
|
94 |
proof - |
|
95 |
{ fix b' |
|
96 |
have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}" |
|
97 |
proof(cases "b = b'") |
|
98 |
case True |
|
99 |
hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto |
|
100 |
thus ?thesis by simp |
|
101 |
next |
|
102 |
case False |
|
103 |
hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto |
|
104 |
thus ?thesis by simp |
|
105 |
qed } |
|
106 |
thus ?thesis unfolding finfun_def by blast |
|
107 |
qed |
|
108 |
||
109 |
lemma const_finfun: "(\<lambda>x. a) \<in> finfun" |
|
110 |
by(auto simp add: finfun_def) |
|
111 |
||
112 |
lemma finfun_left_compose: |
|
113 |
assumes "y \<in> finfun" |
|
114 |
shows "g \<circ> y \<in> finfun" |
|
115 |
proof - |
|
116 |
from assms obtain b where "finite {a. y a \<noteq> b}" |
|
117 |
unfolding finfun_def by blast |
|
118 |
hence "finite {c. g (y c) \<noteq> g b}" |
|
119 |
proof(induct "{a. y a \<noteq> b}" arbitrary: y) |
|
120 |
case empty |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
121 |
hence "y = (\<lambda>a. b)" by(auto) |
48028 | 122 |
thus ?case by(simp) |
123 |
next |
|
124 |
case (insert x F) |
|
60500 | 125 |
note IH = \<open>\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}\<close> |
126 |
from \<open>insert x F = {a. y a \<noteq> b}\<close> \<open>x \<notin> F\<close> |
|
48028 | 127 |
have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto) |
128 |
show ?case |
|
129 |
proof(cases "g (y x) = g b") |
|
130 |
case True |
|
131 |
hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto |
|
132 |
with IH[OF F] show ?thesis by simp |
|
133 |
next |
|
134 |
case False |
|
135 |
hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto |
|
136 |
with IH[OF F] show ?thesis by(simp) |
|
137 |
qed |
|
138 |
qed |
|
139 |
thus ?thesis unfolding finfun_def by auto |
|
140 |
qed |
|
141 |
||
142 |
lemma assumes "y \<in> finfun" |
|
143 |
shows fst_finfun: "fst \<circ> y \<in> finfun" |
|
144 |
and snd_finfun: "snd \<circ> y \<in> finfun" |
|
145 |
proof - |
|
146 |
from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}" |
|
147 |
unfolding finfun_def by auto |
|
148 |
have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}" |
|
149 |
and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto |
|
150 |
hence "finite {a. fst (y a) \<noteq> b}" |
|
151 |
and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset) |
|
152 |
thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun" |
|
153 |
unfolding finfun_def by auto |
|
154 |
qed |
|
155 |
||
156 |
lemma map_of_finfun: "map_of xs \<in> finfun" |
|
157 |
unfolding finfun_def |
|
158 |
by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset) |
|
159 |
||
160 |
lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun" |
|
161 |
by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def) |
|
162 |
||
163 |
lemma finfun_right_compose: |
|
164 |
assumes g: "g \<in> finfun" and inj: "inj f" |
|
165 |
shows "g o f \<in> finfun" |
|
166 |
proof - |
|
167 |
from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast |
|
168 |
moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto |
|
169 |
moreover from inj have "inj_on f {a. g (f a) \<noteq> b}" by(rule subset_inj_on) blast |
|
170 |
ultimately have "finite {a. g (f a) \<noteq> b}" |
|
171 |
by(blast intro: finite_imageD[where f=f] finite_subset) |
|
172 |
thus ?thesis unfolding finfun_def by auto |
|
173 |
qed |
|
174 |
||
175 |
lemma finfun_curry: |
|
176 |
assumes fin: "f \<in> finfun" |
|
177 |
shows "curry f \<in> finfun" "curry f a \<in> finfun" |
|
178 |
proof - |
|
179 |
from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast |
|
180 |
moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force) |
|
181 |
hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}" |
|
182 |
by(auto simp add: curry_def fun_eq_iff) |
|
183 |
ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp |
|
184 |
thus "curry f \<in> finfun" unfolding finfun_def by blast |
|
185 |
||
186 |
have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force) |
|
187 |
hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto |
|
188 |
hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c]) |
|
189 |
thus "curry f a \<in> finfun" unfolding finfun_def by auto |
|
190 |
qed |
|
191 |
||
48030 | 192 |
bundle finfun = |
193 |
fst_finfun[simp] snd_finfun[simp] Abs_finfun_inverse[simp] |
|
194 |
finfun_apply_inverse[simp] Abs_finfun_inject[simp] finfun_apply_inject[simp] |
|
195 |
Diag_finfun[simp] finfun_curry[simp] |
|
196 |
const_finfun[iff] fun_upd_finfun[iff] finfun_apply[iff] map_of_finfun[iff] |
|
197 |
finfun_left_compose[intro] fst_finfun[intro] snd_finfun[intro] |
|
48028 | 198 |
|
199 |
lemma Abs_finfun_inject_finite: |
|
200 |
fixes x y :: "'a \<Rightarrow> 'b" |
|
201 |
assumes fin: "finite (UNIV :: 'a set)" |
|
202 |
shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y" |
|
203 |
proof |
|
204 |
assume "Abs_finfun x = Abs_finfun y" |
|
205 |
moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def |
|
206 |
by(auto intro: finite_subset[OF _ fin]) |
|
207 |
ultimately show "x = y" by(simp add: Abs_finfun_inject) |
|
208 |
qed simp |
|
209 |
||
210 |
lemma Abs_finfun_inject_finite_class: |
|
211 |
fixes x y :: "('a :: finite) \<Rightarrow> 'b" |
|
212 |
shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y" |
|
213 |
using finite_UNIV |
|
214 |
by(simp add: Abs_finfun_inject_finite) |
|
215 |
||
216 |
lemma Abs_finfun_inj_finite: |
|
217 |
assumes fin: "finite (UNIV :: 'a set)" |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
218 |
shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'b)" |
48028 | 219 |
proof(rule inj_onI) |
220 |
fix x y :: "'a \<Rightarrow> 'b" |
|
221 |
assume "Abs_finfun x = Abs_finfun y" |
|
222 |
moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def |
|
223 |
by(auto intro: finite_subset[OF _ fin]) |
|
224 |
ultimately show "x = y" by(simp add: Abs_finfun_inject) |
|
225 |
qed |
|
226 |
||
227 |
lemma Abs_finfun_inverse_finite: |
|
228 |
fixes x :: "'a \<Rightarrow> 'b" |
|
229 |
assumes fin: "finite (UNIV :: 'a set)" |
|
48029 | 230 |
shows "finfun_apply (Abs_finfun x) = x" |
48030 | 231 |
including finfun |
48028 | 232 |
proof - |
233 |
from fin have "x \<in> finfun" |
|
234 |
by(auto simp add: finfun_def intro: finite_subset) |
|
235 |
thus ?thesis by simp |
|
236 |
qed |
|
237 |
||
238 |
lemma Abs_finfun_inverse_finite_class: |
|
239 |
fixes x :: "('a :: finite) \<Rightarrow> 'b" |
|
48029 | 240 |
shows "finfun_apply (Abs_finfun x) = x" |
48028 | 241 |
using finite_UNIV by(simp add: Abs_finfun_inverse_finite) |
242 |
||
243 |
lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV" |
|
244 |
unfolding finfun_def by(auto intro: finite_subset) |
|
245 |
||
246 |
lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)" |
|
247 |
by(simp add: finfun_eq_finite_UNIV) |
|
248 |
||
249 |
lemma map_default_in_finfun: |
|
250 |
assumes fin: "finite (dom f)" |
|
251 |
shows "map_default b f \<in> finfun" |
|
252 |
unfolding finfun_def |
|
253 |
proof(intro CollectI exI) |
|
254 |
from fin show "finite {a. map_default b f a \<noteq> b}" |
|
255 |
by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits) |
|
256 |
qed |
|
257 |
||
258 |
lemma finfun_cases_map_default: |
|
259 |
obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g" |
|
260 |
proof - |
|
261 |
obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f) |
|
262 |
from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto |
|
263 |
let ?g = "(\<lambda>a. if y a = b then None else Some (y a))" |
|
264 |
have "map_default b ?g = y" by(simp add: fun_eq_iff map_default_def) |
|
265 |
with f have "f = Abs_finfun (map_default b ?g)" by simp |
|
266 |
moreover from b have "finite (dom ?g)" by(auto simp add: dom_def) |
|
267 |
moreover have "b \<notin> ran ?g" by(auto simp add: ran_def) |
|
268 |
ultimately show ?thesis by(rule that) |
|
269 |
qed |
|
270 |
||
271 |
||
60500 | 272 |
subsection \<open>Kernel functions for type @{typ "'a \<Rightarrow>f 'b"}\<close> |
48028 | 273 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
274 |
lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("K$/ _" [0] 1) |
48028 | 275 |
is "\<lambda> b x. b" by (rule const_finfun) |
276 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
277 |
lift_definition finfun_update :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("_'(_ $:= _')" [1000,0,0] 1000) is "fun_upd" |
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
278 |
by (simp add: fun_upd_finfun) |
48028 | 279 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
280 |
lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(a $:= b)(a' $:= b') = f(a' $:= b')(a $:= b)" |
48028 | 281 |
by transfer (simp add: fun_upd_twist) |
282 |
||
283 |
lemma finfun_update_twice [simp]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
284 |
"f(a $:= b)(a $:= b') = f(a $:= b')" |
48028 | 285 |
by transfer simp |
286 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
287 |
lemma finfun_update_const_same: "(K$ b)(a $:= b) = (K$ b)" |
48028 | 288 |
by transfer (simp add: fun_eq_iff) |
289 |
||
60500 | 290 |
subsection \<open>Code generator setup\<close> |
48028 | 291 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
292 |
definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b" |
48028 | 293 |
where [simp, code del]: "finfun_update_code = finfun_update" |
294 |
||
295 |
code_datatype finfun_const finfun_update_code |
|
296 |
||
297 |
lemma finfun_update_const_code [code]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
298 |
"(K$ b)(a $:= b') = (if b = b' then (K$ b) else finfun_update_code (K$ b) a b')" |
48028 | 299 |
by(simp add: finfun_update_const_same) |
300 |
||
301 |
lemma finfun_update_update_code [code]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
302 |
"(finfun_update_code f a b)(a' $:= b') = (if a = a' then f(a $:= b') else finfun_update_code (f(a' $:= b')) a b)" |
48028 | 303 |
by(simp add: finfun_update_twist) |
304 |
||
305 |
||
60500 | 306 |
subsection \<open>Setup for quickcheck\<close> |
48028 | 307 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
308 |
quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b" |
48028 | 309 |
|
61585 | 310 |
subsection \<open>\<open>finfun_update\<close> as instance of \<open>comp_fun_commute\<close>\<close> |
48028 | 311 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
312 |
interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')" |
48030 | 313 |
including finfun |
48028 | 314 |
proof |
315 |
fix a a' :: 'a |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
316 |
show "(\<lambda>f. f(a $:= b')) \<circ> (\<lambda>f. f(a' $:= b')) = (\<lambda>f. f(a' $:= b')) \<circ> (\<lambda>f. f(a $:= b'))" |
48028 | 317 |
proof |
318 |
fix b |
|
48029 | 319 |
have "(finfun_apply b)(a := b', a' := b') = (finfun_apply b)(a' := b', a := b')" |
48028 | 320 |
by(cases "a = a'")(auto simp add: fun_upd_twist) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
321 |
then have "b(a $:= b')(a' $:= b') = b(a' $:= b')(a $:= b')" |
48028 | 322 |
by(auto simp add: finfun_update_def fun_upd_twist) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
323 |
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" |
48028 | 324 |
by (simp add: fun_eq_iff) |
325 |
qed |
|
326 |
qed |
|
327 |
||
328 |
lemma fold_finfun_update_finite_univ: |
|
329 |
assumes fin: "finite (UNIV :: 'a set)" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
330 |
shows "Finite_Set.fold (\<lambda>a f. f(a $:= b')) (K$ b) (UNIV :: 'a set) = (K$ b')" |
48028 | 331 |
proof - |
332 |
{ fix A :: "'a set" |
|
333 |
from fin have "finite A" by(auto intro: finite_subset) |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
334 |
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)" |
48028 | 335 |
proof(induct) |
336 |
case (insert x F) |
|
337 |
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)" |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
338 |
by(auto) |
48028 | 339 |
with insert show ?case |
340 |
by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def) |
|
341 |
qed(simp add: finfun_const_def) } |
|
342 |
thus ?thesis by(simp add: finfun_const_def) |
|
343 |
qed |
|
344 |
||
345 |
||
60500 | 346 |
subsection \<open>Default value for FinFuns\<close> |
48028 | 347 |
|
348 |
definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" |
|
349 |
where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})" |
|
350 |
||
351 |
lemma finfun_default_aux_infinite: |
|
352 |
fixes f :: "'a \<Rightarrow> 'b" |
|
353 |
assumes infin: "\<not> finite (UNIV :: 'a set)" |
|
354 |
and fin: "finite {a. f a \<noteq> b}" |
|
355 |
shows "finfun_default_aux f = b" |
|
356 |
proof - |
|
357 |
let ?B = "{a. f a \<noteq> b}" |
|
358 |
from fin have "(THE b. finite {a. f a \<noteq> b}) = b" |
|
359 |
proof(rule the_equality) |
|
360 |
fix b' |
|
361 |
assume "finite {a. f a \<noteq> b'}" (is "finite ?B'") |
|
362 |
with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset) |
|
363 |
then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto |
|
364 |
thus "b' = b" by auto |
|
365 |
qed |
|
366 |
thus ?thesis using infin by(simp add: finfun_default_aux_def) |
|
367 |
qed |
|
368 |
||
369 |
||
370 |
lemma finite_finfun_default_aux: |
|
371 |
fixes f :: "'a \<Rightarrow> 'b" |
|
372 |
assumes fin: "f \<in> finfun" |
|
373 |
shows "finite {a. f a \<noteq> finfun_default_aux f}" |
|
374 |
proof(cases "finite (UNIV :: 'a set)") |
|
375 |
case True thus ?thesis using fin |
|
376 |
by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset) |
|
377 |
next |
|
378 |
case False |
|
379 |
from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B") |
|
380 |
unfolding finfun_def by blast |
|
381 |
with False show ?thesis by(simp add: finfun_default_aux_infinite) |
|
382 |
qed |
|
383 |
||
384 |
lemma finfun_default_aux_update_const: |
|
385 |
fixes f :: "'a \<Rightarrow> 'b" |
|
386 |
assumes fin: "f \<in> finfun" |
|
387 |
shows "finfun_default_aux (f(a := b)) = finfun_default_aux f" |
|
388 |
proof(cases "finite (UNIV :: 'a set)") |
|
389 |
case False |
|
390 |
from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast |
|
391 |
hence "finite {a'. (f(a := b)) a' \<noteq> b'}" |
|
392 |
proof(cases "b = b' \<and> f a \<noteq> b'") |
|
393 |
case True |
|
394 |
hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto |
|
395 |
thus ?thesis using b' by simp |
|
396 |
next |
|
397 |
case False |
|
398 |
moreover |
|
399 |
{ assume "b \<noteq> b'" |
|
400 |
hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto |
|
401 |
hence ?thesis using b' by simp } |
|
402 |
moreover |
|
403 |
{ assume "b = b'" "f a = b'" |
|
404 |
hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto |
|
405 |
hence ?thesis using b' by simp } |
|
406 |
ultimately show ?thesis by blast |
|
407 |
qed |
|
408 |
with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite) |
|
409 |
next |
|
410 |
case True thus ?thesis by(simp add: finfun_default_aux_def) |
|
411 |
qed |
|
412 |
||
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
413 |
lift_definition finfun_default :: "'a \<Rightarrow>f 'b \<Rightarrow> 'b" |
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
53374
diff
changeset
|
414 |
is "finfun_default_aux" . |
48028 | 415 |
|
48029 | 416 |
lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}" |
48031 | 417 |
by transfer (erule finite_finfun_default_aux) |
48028 | 418 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
419 |
lemma finfun_default_const: "finfun_default ((K$ b) :: 'a \<Rightarrow>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)" |
48031 | 420 |
by(transfer)(auto simp add: finfun_default_aux_infinite finfun_default_aux_def) |
48028 | 421 |
|
422 |
lemma finfun_default_update_const: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
423 |
"finfun_default (f(a $:= b)) = finfun_default f" |
48028 | 424 |
by transfer (simp add: finfun_default_aux_update_const) |
425 |
||
426 |
lemma finfun_default_const_code [code]: |
|
48070
02d64fd40852
more sort constraints for FinFun code generation
Andreas Lochbihler
parents:
48059
diff
changeset
|
427 |
"finfun_default ((K$ c) :: 'a :: card_UNIV \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)" |
48059 | 428 |
by(simp add: finfun_default_const) |
48028 | 429 |
|
430 |
lemma finfun_default_update_code [code]: |
|
431 |
"finfun_default (finfun_update_code f a b) = finfun_default f" |
|
432 |
by(simp add: finfun_default_update_const) |
|
433 |
||
60500 | 434 |
subsection \<open>Recursion combinator and well-formedness conditions\<close> |
48028 | 435 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
436 |
definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>f 'b) \<Rightarrow> 'c" |
48028 | 437 |
where [code del]: |
438 |
"finfun_rec cnst upd f \<equiv> |
|
439 |
let b = finfun_default f; |
|
440 |
g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g |
|
441 |
in Finite_Set.fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)" |
|
442 |
||
443 |
locale finfun_rec_wf_aux = |
|
444 |
fixes cnst :: "'b \<Rightarrow> 'c" |
|
445 |
and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c" |
|
446 |
assumes upd_const_same: "upd a b (cnst b) = cnst b" |
|
447 |
and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)" |
|
448 |
and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)" |
|
449 |
begin |
|
450 |
||
451 |
||
452 |
lemma upd_left_comm: "comp_fun_commute (\<lambda>a. upd a (f a))" |
|
453 |
by(unfold_locales)(auto intro: upd_commute simp add: fun_eq_iff) |
|
454 |
||
455 |
lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)" |
|
456 |
by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp) |
|
457 |
||
458 |
lemma map_default_update_const: |
|
459 |
assumes fin: "finite (dom f)" |
|
460 |
and anf: "a \<notin> dom f" |
|
461 |
and fg: "f \<subseteq>\<^sub>m g" |
|
462 |
shows "upd a d (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) = |
|
463 |
Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)" |
|
464 |
proof - |
|
465 |
let ?upd = "\<lambda>a. upd a (map_default d g a)" |
|
466 |
let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A" |
|
467 |
interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm) |
|
468 |
||
469 |
from fin anf fg show ?thesis |
|
470 |
proof(induct "dom f" arbitrary: f) |
|
471 |
case empty |
|
60500 | 472 |
from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def) |
48028 | 473 |
thus ?case by(simp add: finfun_const_def upd_const_same) |
474 |
next |
|
475 |
case (insert a' A) |
|
60500 | 476 |
note IH = \<open>\<And>f. \<lbrakk> A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g \<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)\<close> |
477 |
note fin = \<open>finite A\<close> note anf = \<open>a \<notin> dom f\<close> note a'nA = \<open>a' \<notin> A\<close> |
|
478 |
note domf = \<open>insert a' A = dom f\<close> note fg = \<open>f \<subseteq>\<^sub>m g\<close> |
|
48028 | 479 |
|
480 |
from domf obtain b where b: "f a' = Some b" by auto |
|
481 |
let ?f' = "f(a' := None)" |
|
482 |
have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))" |
|
483 |
by(subst gwf.fold_insert[OF fin a'nA]) rule |
|
484 |
also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec) |
|
485 |
hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def) |
|
486 |
also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this] |
|
487 |
also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def) |
|
60500 | 488 |
note A also note IH[OF A \<open>a \<notin> dom ?f'\<close> \<open>?f' \<subseteq>\<^sub>m g\<close>] |
48028 | 489 |
also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)" |
490 |
unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A .. |
|
491 |
also have "insert a' (dom ?f') = dom f" using domf by auto |
|
492 |
finally show ?case . |
|
493 |
qed |
|
494 |
qed |
|
495 |
||
496 |
lemma map_default_update_twice: |
|
497 |
assumes fin: "finite (dom f)" |
|
498 |
and anf: "a \<notin> dom f" |
|
499 |
and fg: "f \<subseteq>\<^sub>m g" |
|
500 |
shows "upd a d'' (upd a d' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) = |
|
501 |
upd a d'' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))" |
|
502 |
proof - |
|
503 |
let ?upd = "\<lambda>a. upd a (map_default d g a)" |
|
504 |
let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A" |
|
505 |
interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm) |
|
506 |
||
507 |
from fin anf fg show ?thesis |
|
508 |
proof(induct "dom f" arbitrary: f) |
|
509 |
case empty |
|
60500 | 510 |
from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def) |
48028 | 511 |
thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice) |
512 |
next |
|
513 |
case (insert a' A) |
|
60500 | 514 |
note IH = \<open>\<And>f. \<lbrakk>A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))\<close> |
515 |
note fin = \<open>finite A\<close> note anf = \<open>a \<notin> dom f\<close> note a'nA = \<open>a' \<notin> A\<close> |
|
516 |
note domf = \<open>insert a' A = dom f\<close> note fg = \<open>f \<subseteq>\<^sub>m g\<close> |
|
48028 | 517 |
|
518 |
from domf obtain b where b: "f a' = Some b" by auto |
|
519 |
let ?f' = "f(a' := None)" |
|
520 |
let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b" |
|
521 |
from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp |
|
522 |
also note gwf.fold_insert[OF fin a'nA] |
|
523 |
also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec) |
|
524 |
hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def) |
|
525 |
also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this] |
|
526 |
also note upd_commute[OF ana'] |
|
527 |
also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def) |
|
60500 | 528 |
note A also note IH[OF A \<open>a \<notin> dom ?f'\<close> \<open>?f' \<subseteq>\<^sub>m g\<close>] |
48028 | 529 |
also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric] |
530 |
also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf |
|
531 |
finally show ?case . |
|
532 |
qed |
|
533 |
qed |
|
534 |
||
535 |
lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f" |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
536 |
by(auto simp add: map_default_def restrict_map_def) |
48028 | 537 |
|
538 |
lemma finite_rec_cong1: |
|
539 |
assumes f: "comp_fun_commute f" and g: "comp_fun_commute g" |
|
540 |
and fin: "finite A" |
|
541 |
and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a" |
|
542 |
shows "Finite_Set.fold f z A = Finite_Set.fold g z A" |
|
543 |
proof - |
|
544 |
interpret f: comp_fun_commute f by(rule f) |
|
545 |
interpret g: comp_fun_commute g by(rule g) |
|
546 |
{ fix B |
|
547 |
assume BsubA: "B \<subseteq> A" |
|
548 |
with fin have "finite B" by(blast intro: finite_subset) |
|
549 |
hence "B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B" |
|
550 |
proof(induct) |
|
551 |
case empty thus ?case by simp |
|
552 |
next |
|
553 |
case (insert a B) |
|
60500 | 554 |
note finB = \<open>finite B\<close> note anB = \<open>a \<notin> B\<close> note sub = \<open>insert a B \<subseteq> A\<close> |
555 |
note IH = \<open>B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B\<close> |
|
48028 | 556 |
from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto |
557 |
from IH[OF BsubA] eq[OF aA] finB anB |
|
558 |
show ?case by(auto) |
|
559 |
qed |
|
560 |
with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast } |
|
561 |
thus ?thesis by blast |
|
562 |
qed |
|
563 |
||
564 |
lemma finfun_rec_upd [simp]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
565 |
"finfun_rec cnst upd (f(a' $:= b')) = upd a' b' (finfun_rec cnst upd f)" |
48030 | 566 |
including finfun |
48028 | 567 |
proof - |
568 |
obtain b where b: "b = finfun_default f" by auto |
|
569 |
let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g" |
|
570 |
obtain g where g: "g = The (?the f)" by blast |
|
571 |
obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f) |
|
572 |
from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux) |
|
573 |
||
574 |
let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}" |
|
575 |
from bfin have fing: "finite (dom ?g)" by auto |
|
576 |
have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def) |
|
577 |
have yg: "y = map_default b ?g" by simp |
|
578 |
have gg: "g = ?g" unfolding g |
|
579 |
proof(rule the_equality) |
|
580 |
from f y bfin show "?the f ?g" |
|
581 |
by(auto)(simp add: restrict_map_def ran_def split: split_if_asm) |
|
582 |
next |
|
583 |
fix g' |
|
584 |
assume "?the f g'" |
|
585 |
hence fin': "finite (dom g')" and ran': "b \<notin> ran g'" |
|
586 |
and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto |
|
587 |
from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+ |
|
588 |
with eq have "map_default b ?g = map_default b g'" by simp |
|
589 |
with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym]) |
|
590 |
qed |
|
591 |
||
592 |
show ?thesis |
|
593 |
proof(cases "b' = b") |
|
594 |
case True |
|
595 |
note b'b = True |
|
596 |
||
597 |
let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}" |
|
598 |
from bfin b'b have fing': "finite (dom ?g')" |
|
599 |
by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset) |
|
600 |
have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def) |
|
601 |
||
602 |
let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b" |
|
603 |
let ?b = "map_default b ?g" |
|
604 |
from upd_left_comm upd_left_comm fing' |
|
605 |
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')" |
|
606 |
by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def) |
|
607 |
also interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm) |
|
608 |
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))" |
|
609 |
proof(cases "y a' = b") |
|
610 |
case True |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
611 |
with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def) |
48028 | 612 |
from True have a'ndomg: "a' \<notin> dom ?g" by auto |
613 |
from f b'b b show ?thesis unfolding g' |
|
614 |
by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp |
|
615 |
next |
|
616 |
case False |
|
617 |
hence domg: "dom ?g = insert a' (dom ?g')" by auto |
|
618 |
from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto |
|
619 |
have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) = |
|
620 |
upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))" |
|
621 |
using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert) |
|
622 |
hence "upd a' b (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) = |
|
623 |
upd a' b (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp |
|
624 |
also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def) |
|
625 |
note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b] |
|
626 |
also note map_default_update_const[OF fing' a'ndomg' g'leg, of b] |
|
627 |
finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym) |
|
628 |
qed |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
629 |
also have "The (?the (f(a' $:= b'))) = ?g'" |
48028 | 630 |
proof(rule the_equality) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
631 |
from f y b b'b brang' fing' show "?the (f(a' $:= b')) ?g'" |
48028 | 632 |
by(auto simp del: fun_upd_apply simp add: finfun_update_def) |
633 |
next |
|
634 |
fix g' |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
635 |
assume "?the (f(a' $:= b')) g'" |
48028 | 636 |
hence fin': "finite (dom g')" and ran': "b \<notin> ran g'" |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
637 |
and eq: "f(a' $:= b') = Abs_finfun (map_default b g')" |
48028 | 638 |
by(auto simp del: fun_upd_apply) |
639 |
from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun" |
|
640 |
by(blast intro: map_default_in_finfun)+ |
|
641 |
with eq f b'b b have "map_default b ?g' = map_default b g'" |
|
642 |
by(simp del: fun_upd_apply add: finfun_update_def) |
|
643 |
with fing' brang' fin' ran' show "g' = ?g'" |
|
644 |
by(rule map_default_inject[OF disjI2[OF refl], THEN sym]) |
|
645 |
qed |
|
646 |
ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b |
|
647 |
by(simp only: finfun_default_update_const map_default_def) |
|
648 |
next |
|
649 |
case False |
|
650 |
note b'b = this |
|
651 |
let ?g' = "?g(a' \<mapsto> b')" |
|
652 |
let ?b' = "map_default b ?g'" |
|
653 |
let ?b = "map_default b ?g" |
|
654 |
from fing have fing': "finite (dom ?g')" by auto |
|
655 |
from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def) |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
656 |
have ffmg': "map_default b ?g' = y(a' := b')" by(auto simp add: map_default_def restrict_map_def) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
657 |
with f y have f_Abs: "f(a' $:= b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def) |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
658 |
have g': "The (?the (f(a' $:= b'))) = ?g'" |
48028 | 659 |
proof (rule the_equality) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
660 |
from fing' bnrang' f_Abs show "?the (f(a' $:= b')) ?g'" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
661 |
by(auto simp add: finfun_update_def restrict_map_def) |
48028 | 662 |
next |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
663 |
fix g' assume "?the (f(a' $:= b')) g'" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
664 |
hence f': "f(a' $:= b') = Abs_finfun (map_default b g')" |
48028 | 665 |
and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto |
666 |
from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun" |
|
667 |
by(auto intro: map_default_in_finfun) |
|
668 |
with f' f_Abs have "map_default b g' = map_default b ?g'" by simp |
|
669 |
with fin' brang' fing' bnrang' show "g' = ?g'" |
|
670 |
by(rule map_default_inject[OF disjI2[OF refl]]) |
|
671 |
qed |
|
672 |
have dom: "dom (((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b})(a' \<mapsto> b')) = insert a' (dom ((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}))" |
|
673 |
by auto |
|
674 |
show ?thesis |
|
675 |
proof(cases "y a' = b") |
|
676 |
case True |
|
677 |
hence a'ndomg: "a' \<notin> dom ?g" by auto |
|
678 |
from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)" |
|
679 |
by(auto simp add: restrict_map_def map_default_def intro!: ext) |
|
680 |
hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp |
|
681 |
interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm) |
|
682 |
from upd_left_comm upd_left_comm fing |
|
683 |
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)" |
|
684 |
by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def) |
|
685 |
thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] |
|
686 |
unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom] |
|
687 |
by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def) |
|
688 |
next |
|
689 |
case False |
|
690 |
hence "insert a' (dom ?g) = dom ?g" by auto |
|
691 |
moreover { |
|
692 |
let ?g'' = "?g(a' := None)" |
|
693 |
let ?b'' = "map_default b ?g''" |
|
694 |
from False have domg: "dom ?g = insert a' (dom ?g'')" by auto |
|
695 |
from False have a'ndomg'': "a' \<notin> dom ?g''" by auto |
|
696 |
have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto |
|
697 |
have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def) |
|
698 |
interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm) |
|
699 |
interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm) |
|
700 |
have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) = |
|
701 |
upd a' b' (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))" |
|
702 |
unfolding gwf.fold_insert[OF fing'' a'ndomg''] f .. |
|
703 |
also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def) |
|
704 |
have "dom (?g |` dom ?g'') = dom ?g''" by auto |
|
705 |
note map_default_update_twice[where d=b and f = "?g |` dom ?g''" and a=a' and d'="?b a'" and d''=b' and g="?g", |
|
706 |
unfolded this, OF fing'' a'ndomg'' g''leg] |
|
707 |
also have b': "b' = ?b' a'" by(auto simp add: map_default_def) |
|
708 |
from upd_left_comm upd_left_comm fing'' |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
709 |
have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
710 |
Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')" |
48028 | 711 |
by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def) |
712 |
with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) = |
|
713 |
upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp |
|
714 |
also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric] |
|
715 |
finally have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) = |
|
716 |
Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)" |
|
717 |
unfolding domg . } |
|
718 |
ultimately have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) = |
|
719 |
upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp |
|
720 |
thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric] |
|
721 |
using b'b gg by(simp add: map_default_insert) |
|
722 |
qed |
|
723 |
qed |
|
724 |
qed |
|
725 |
||
726 |
end |
|
727 |
||
728 |
locale finfun_rec_wf = finfun_rec_wf_aux + |
|
729 |
assumes const_update_all: |
|
730 |
"finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'" |
|
731 |
begin |
|
732 |
||
48030 | 733 |
lemma finfun_rec_const [simp]: includes finfun shows |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
734 |
"finfun_rec cnst upd (K$ c) = cnst c" |
48028 | 735 |
proof(cases "finite (UNIV :: 'a set)") |
736 |
case False |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
737 |
hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const) |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
738 |
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" |
48028 | 739 |
proof (rule the_equality) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
740 |
show "(K$ c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty" |
48028 | 741 |
by(auto simp add: finfun_const_def) |
742 |
next |
|
743 |
fix g :: "'a \<rightharpoonup> 'b" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
744 |
assume "(K$ c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
745 |
hence g: "(K$ c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+ |
48028 | 746 |
from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)" |
747 |
by(simp add: finfun_const_def) |
|
748 |
moreover have "map_default c empty = (\<lambda>a. c)" by simp |
|
749 |
ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto) |
|
750 |
qed |
|
751 |
ultimately show ?thesis by(simp add: finfun_rec_def) |
|
752 |
next |
|
753 |
case True |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
754 |
hence default: "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = undefined" by(simp add: finfun_default_const) |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
755 |
let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (K$ c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g" |
48028 | 756 |
show ?thesis |
757 |
proof(cases "c = undefined") |
|
758 |
case True |
|
759 |
have the: "The ?the = empty" |
|
760 |
proof (rule the_equality) |
|
761 |
from True show "?the empty" by(auto simp add: finfun_const_def) |
|
762 |
next |
|
763 |
fix g' |
|
764 |
assume "?the g'" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
765 |
hence fg: "(K$ c) = Abs_finfun (map_default undefined g')" |
48028 | 766 |
and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all |
767 |
from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun) |
|
768 |
with fg have "map_default undefined g' = (\<lambda>a. c)" |
|
48030 | 769 |
by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1, symmetric]) |
48028 | 770 |
with True show "g' = empty" |
771 |
by -(rule map_default_inject(2)[OF _ fin g], auto) |
|
772 |
qed |
|
60500 | 773 |
show ?thesis unfolding finfun_rec_def using \<open>finite UNIV\<close> True |
48028 | 774 |
unfolding Let_def the default by(simp) |
775 |
next |
|
776 |
case False |
|
777 |
have the: "The ?the = (\<lambda>a :: 'a. Some c)" |
|
778 |
proof (rule the_equality) |
|
779 |
from False True show "?the (\<lambda>a :: 'a. Some c)" |
|
780 |
by(auto simp add: map_default_def [abs_def] finfun_const_def dom_def ran_def) |
|
781 |
next |
|
782 |
fix g' :: "'a \<rightharpoonup> 'b" |
|
783 |
assume "?the g'" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
784 |
hence fg: "(K$ c) = Abs_finfun (map_default undefined g')" |
48028 | 785 |
and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all |
786 |
from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun) |
|
787 |
with fg have "map_default undefined g' = (\<lambda>a. c)" |
|
788 |
by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1]) |
|
789 |
with True False show "g' = (\<lambda>a::'a. Some c)" |
|
790 |
by - (rule map_default_inject(2)[OF _ fin g], |
|
791 |
auto simp add: dom_def ran_def map_default_def [abs_def]) |
|
792 |
qed |
|
793 |
show ?thesis unfolding finfun_rec_def using True False |
|
794 |
unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all) |
|
795 |
qed |
|
796 |
qed |
|
797 |
||
798 |
end |
|
799 |
||
60500 | 800 |
subsection \<open>Weak induction rule and case analysis for FinFuns\<close> |
48028 | 801 |
|
802 |
lemma finfun_weak_induct [consumes 0, case_names const update]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
803 |
assumes const: "\<And>b. P (K$ b)" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
804 |
and update: "\<And>f a b. P f \<Longrightarrow> P (f(a $:= b))" |
48028 | 805 |
shows "P x" |
48030 | 806 |
including finfun |
48028 | 807 |
proof(induct x rule: Abs_finfun_induct) |
808 |
case (Abs_finfun y) |
|
809 |
then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast |
|
60500 | 810 |
thus ?case using \<open>y \<in> finfun\<close> |
48028 | 811 |
proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct) |
812 |
case empty |
|
813 |
hence "\<And>a. y a = b" by blast |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
814 |
hence "y = (\<lambda>a. b)" by(auto) |
48028 | 815 |
hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp |
816 |
thus ?case by(simp add: const) |
|
817 |
next |
|
818 |
case (insert a A) |
|
60500 | 819 |
note IH = \<open>\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun \<rbrakk> \<Longrightarrow> P (Abs_finfun y)\<close> |
820 |
note y = \<open>y \<in> finfun\<close> |
|
821 |
with \<open>insert a A = {a. y a \<noteq> b}\<close> \<open>a \<notin> A\<close> |
|
48028 | 822 |
have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto |
823 |
from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update) |
|
824 |
thus ?case using y unfolding finfun_update_def by simp |
|
825 |
qed |
|
826 |
qed |
|
827 |
||
828 |
lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)" |
|
829 |
by(induct x rule: finfun_weak_induct) blast+ |
|
830 |
||
831 |
lemma finfun_exhaust: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
832 |
obtains b where "x = (K$ b)" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
833 |
| f a b where "x = f(a $:= b)" |
48028 | 834 |
by(atomize_elim)(rule finfun_exhaust_disj) |
835 |
||
836 |
lemma finfun_rec_unique: |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
837 |
fixes f :: "'a \<Rightarrow>f 'b \<Rightarrow> 'c" |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
838 |
assumes c: "\<And>c. f (K$ c) = cnst c" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
839 |
and u: "\<And>g a b. f (g(a $:= b)) = upd g a b (f g)" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
840 |
and c': "\<And>c. f' (K$ c) = cnst c" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
841 |
and u': "\<And>g a b. f' (g(a $:= b)) = upd g a b (f' g)" |
48028 | 842 |
shows "f = f'" |
843 |
proof |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
844 |
fix g :: "'a \<Rightarrow>f 'b" |
48028 | 845 |
show "f g = f' g" |
846 |
by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u') |
|
847 |
qed |
|
848 |
||
849 |
||
60500 | 850 |
subsection \<open>Function application\<close> |
48028 | 851 |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
852 |
notation finfun_apply (infixl "$" 999) |
48028 | 853 |
|
854 |
interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c" |
|
855 |
by(unfold_locales) auto |
|
856 |
||
857 |
interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c" |
|
858 |
proof(unfold_locales) |
|
859 |
fix b' b :: 'a |
|
860 |
assume fin: "finite (UNIV :: 'b set)" |
|
861 |
{ fix A :: "'b set" |
|
862 |
interpret comp_fun_commute "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm) |
|
863 |
from fin have "finite A" by(auto intro: finite_subset) |
|
864 |
hence "Finite_Set.fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)" |
|
865 |
by induct auto } |
|
866 |
from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp |
|
867 |
qed |
|
868 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
869 |
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)" |
48029 | 870 |
proof(rule finfun_rec_unique) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
871 |
fix c show "op $ (K$ c) = (\<lambda>a. c)" by(simp add: finfun_const.rep_eq) |
48029 | 872 |
next |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
873 |
fix g a b show "op $ g(a $:= b) = (\<lambda>c. if c = a then b else g $ c)" |
48029 | 874 |
by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse finfun_apply) |
875 |
qed auto |
|
48028 | 876 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
877 |
lemma finfun_upd_apply: "f(a $:= b) $ a' = (if a = a' then b else f $ a')" |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
878 |
and finfun_upd_apply_code [code]: "(finfun_update_code f a b) $ a' = (if a = a' then b else f $ a')" |
48028 | 879 |
by(simp_all add: finfun_apply_def) |
880 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
881 |
lemma finfun_const_apply [simp, code]: "(K$ b) $ a = b" |
48029 | 882 |
by(simp add: finfun_apply_def) |
883 |
||
48028 | 884 |
lemma finfun_upd_apply_same [simp]: |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
885 |
"f(a $:= b) $ a = b" |
48028 | 886 |
by(simp add: finfun_upd_apply) |
887 |
||
888 |
lemma finfun_upd_apply_other [simp]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
889 |
"a \<noteq> a' \<Longrightarrow> f(a $:= b) $ a' = f $ a'" |
48028 | 890 |
by(simp add: finfun_upd_apply) |
891 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
892 |
lemma finfun_ext: "(\<And>a. f $ a = g $ a) \<Longrightarrow> f = g" |
58787 | 893 |
by(auto simp add: finfun_apply_inject[symmetric]) |
48028 | 894 |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
895 |
lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)" |
48028 | 896 |
by(auto intro: finfun_ext) |
897 |
||
48100 | 898 |
lemma finfun_upd_triv [simp]: "f(x $:= f $ x) = f" |
899 |
by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply) |
|
900 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
901 |
lemma finfun_const_inject [simp]: "(K$ b) = (K$ b') \<equiv> b = b'" |
48028 | 902 |
by(simp add: expand_finfun_eq fun_eq_iff) |
903 |
||
904 |
lemma finfun_const_eq_update: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
905 |
"((K$ b) = f(a $:= b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))" |
48028 | 906 |
by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply) |
907 |
||
60500 | 908 |
subsection \<open>Function composition\<close> |
48028 | 909 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
910 |
definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "\<circ>$" 55) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
911 |
where [code del]: "g \<circ>$ f = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f" |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
912 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
913 |
notation (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
914 |
finfun_comp (infixr "o$" 55) |
48028 | 915 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
916 |
interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))" |
48028 | 917 |
by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext) |
918 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
919 |
interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))" |
48028 | 920 |
proof |
921 |
fix b' b :: 'a |
|
922 |
assume fin: "finite (UNIV :: 'c set)" |
|
923 |
{ fix A :: "'c set" |
|
924 |
from fin have "finite A" by(auto intro: finite_subset) |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
925 |
hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) A = |
48028 | 926 |
Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)" |
927 |
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) } |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
928 |
from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(a $:= g b')) (K$ g b) UNIV = (K$ g b')" |
48028 | 929 |
by(simp add: finfun_const_def) |
930 |
qed |
|
931 |
||
932 |
lemma finfun_comp_const [simp, code]: |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
933 |
"g \<circ>$ (K$ c) = (K$ g c)" |
48028 | 934 |
by(simp add: finfun_comp_def) |
935 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
936 |
lemma finfun_comp_update [simp]: "g \<circ>$ (f(a $:= b)) = (g \<circ>$ f)(a $:= g b)" |
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
937 |
and finfun_comp_update_code [code]: |
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
938 |
"g \<circ>$ (finfun_update_code f a b) = finfun_update_code (g \<circ>$ f) a (g b)" |
48028 | 939 |
by(simp_all add: finfun_comp_def) |
940 |
||
941 |
lemma finfun_comp_apply [simp]: |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
942 |
"op $ (g \<circ>$ f) = g \<circ> op $ f" |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
943 |
by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply) |
48028 | 944 |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
945 |
lemma finfun_comp_comp_collapse [simp]: "f \<circ>$ g \<circ>$ h = (f \<circ> g) \<circ>$ h" |
48028 | 946 |
by(induct h rule: finfun_weak_induct) simp_all |
947 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
948 |
lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>$ f = (K$ c)" |
48028 | 949 |
by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply) |
950 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
951 |
lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>$ f = f" "id \<circ>$ f = f" |
48028 | 952 |
by(induct f rule: finfun_weak_induct) auto |
953 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
954 |
lemma finfun_comp_conv_comp: "g \<circ>$ f = Abs_finfun (g \<circ> op $ f)" |
48030 | 955 |
including finfun |
48028 | 956 |
proof - |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
957 |
have "(\<lambda>f. g \<circ>$ f) = (\<lambda>f. Abs_finfun (g \<circ> op $ f))" |
48028 | 958 |
proof(rule finfun_rec_unique) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
959 |
{ fix c show "Abs_finfun (g \<circ> op $ (K$ c)) = (K$ g c)" |
48028 | 960 |
by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) } |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
961 |
{ fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)" |
48028 | 962 |
proof - |
963 |
obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g') |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52916
diff
changeset
|
964 |
moreover from g' have "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose) |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
965 |
moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto) |
48029 | 966 |
ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def) |
48028 | 967 |
qed } |
968 |
qed auto |
|
969 |
thus ?thesis by(auto simp add: fun_eq_iff) |
|
970 |
qed |
|
971 |
||
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
972 |
definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "$\<circ>" 55) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
973 |
where [code del]: "g $\<circ> f = Abs_finfun (op $ g \<circ> f)" |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
974 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
975 |
notation (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
976 |
finfun_comp2 (infixr "$o" 55) |
48028 | 977 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
978 |
lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)" |
48030 | 979 |
including finfun |
48028 | 980 |
by(simp add: finfun_comp2_def finfun_const_def comp_def) |
981 |
||
982 |
lemma finfun_comp2_update: |
|
48030 | 983 |
includes finfun |
48028 | 984 |
assumes inj: "inj f" |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
985 |
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)" |
48028 | 986 |
proof(cases "b \<in> range f") |
987 |
case True |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
988 |
from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD) |
48028 | 989 |
with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose) |
990 |
next |
|
991 |
case False |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
992 |
hence "(op $ g)(b := c) \<circ> f = op $ g \<circ> f" by(auto simp add: fun_eq_iff) |
48028 | 993 |
with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def) |
994 |
qed |
|
995 |
||
60500 | 996 |
subsection \<open>Universal quantification\<close> |
48028 | 997 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
998 |
definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool" |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
999 |
where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a" |
48028 | 1000 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1001 |
lemma finfun_All_except_const: "finfun_All_except A (K$ b) \<longleftrightarrow> b \<or> set A = UNIV" |
48028 | 1002 |
by(auto simp add: finfun_All_except_def) |
1003 |
||
1004 |
lemma finfun_All_except_const_finfun_UNIV_code [code]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1005 |
"finfun_All_except A (K$ b) = (b \<or> is_list_UNIV A)" |
48028 | 1006 |
by(simp add: finfun_All_except_const is_list_UNIV_iff) |
1007 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1008 |
lemma finfun_All_except_update: |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1009 |
"finfun_All_except A f(a $:= b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)" |
48028 | 1010 |
by(fastforce simp add: finfun_All_except_def finfun_upd_apply) |
1011 |
||
1012 |
lemma finfun_All_except_update_code [code]: |
|
1013 |
fixes a :: "'a :: card_UNIV" |
|
1014 |
shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)" |
|
1015 |
by(simp add: finfun_All_except_update) |
|
1016 |
||
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1017 |
definition finfun_All :: "'a \<Rightarrow>f bool \<Rightarrow> bool" |
48028 | 1018 |
where "finfun_All = finfun_All_except []" |
1019 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1020 |
lemma finfun_All_const [simp]: "finfun_All (K$ b) = b" |
48028 | 1021 |
by(simp add: finfun_All_def finfun_All_except_def) |
1022 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1023 |
lemma finfun_All_update: "finfun_All f(a $:= b) = (b \<and> finfun_All_except [a] f)" |
48028 | 1024 |
by(simp add: finfun_All_def finfun_All_except_update) |
1025 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1026 |
lemma finfun_All_All: "finfun_All P = All (op $ P)" |
48028 | 1027 |
by(simp add: finfun_All_def finfun_All_except_def) |
1028 |
||
1029 |
||
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1030 |
definition finfun_Ex :: "'a \<Rightarrow>f bool \<Rightarrow> bool" |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1031 |
where "finfun_Ex P = Not (finfun_All (Not \<circ>$ P))" |
48028 | 1032 |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1033 |
lemma finfun_Ex_Ex: "finfun_Ex P = Ex (op $ P)" |
48028 | 1034 |
unfolding finfun_Ex_def finfun_All_All by simp |
1035 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1036 |
lemma finfun_Ex_const [simp]: "finfun_Ex (K$ b) = b" |
48028 | 1037 |
by(simp add: finfun_Ex_def) |
1038 |
||
1039 |
||
60500 | 1040 |
subsection \<open>A diagonal operator for FinFuns\<close> |
48028 | 1041 |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1042 |
definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'($_,/ _$'))" [0, 0] 1000) |
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1043 |
where [code del]: "($f, g$) = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f" |
48028 | 1044 |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1045 |
interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))" |
48028 | 1046 |
by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply) |
1047 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1048 |
interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>$ g" "\<lambda>a b c. c(a $:= (b, g $ a))" |
48028 | 1049 |
proof |
1050 |
fix b' b :: 'a |
|
1051 |
assume fin: "finite (UNIV :: 'c set)" |
|
1052 |
{ fix A :: "'c set" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1053 |
interpret comp_fun_commute "\<lambda>a c. c(a $:= (b', g $ a))" by(rule finfun_Diag_aux.upd_left_comm) |
48028 | 1054 |
from fin have "finite A" by(auto intro: finite_subset) |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1055 |
hence "Finite_Set.fold (\<lambda>a c. c(a $:= (b', g $ a))) (Pair b \<circ>$ g) A = |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1056 |
Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g $ a))" |
48028 | 1057 |
by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def, |
1058 |
auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) } |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1059 |
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" |
48028 | 1060 |
by(simp add: finfun_const_def finfun_comp_conv_comp o_def) |
1061 |
qed |
|
1062 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1063 |
lemma finfun_Diag_const1: "($K$ b, g$) = Pair b \<circ>$ g" |
48028 | 1064 |
by(simp add: finfun_Diag_def) |
1065 |
||
60500 | 1066 |
text \<open> |
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1067 |
Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{term "op \<circ>$"}. |
60500 | 1068 |
\<close> |
48028 | 1069 |
|
1070 |
lemma finfun_Diag_const_code [code]: |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1071 |
"($K$ b, K$ c$) = (K$ (b, c))" |
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1072 |
"($K$ b, finfun_update_code g a c$) = finfun_update_code ($K$ b, g$) a (b, c)" |
48028 | 1073 |
by(simp_all add: finfun_Diag_const1) |
1074 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1075 |
lemma finfun_Diag_update1: "($f(a $:= b), g$) = ($f, g$)(a $:= (b, g $ a))" |
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1076 |
and finfun_Diag_update1_code [code]: "($finfun_update_code f a b, g$) = ($f, g$)(a $:= (b, g $ a))" |
48028 | 1077 |
by(simp_all add: finfun_Diag_def) |
1078 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1079 |
lemma finfun_Diag_const2: "($f, K$ c$) = (\<lambda>b. (b, c)) \<circ>$ f" |
48028 | 1080 |
by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1) |
1081 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1082 |
lemma finfun_Diag_update2: "($f, g(a $:= c)$) = ($f, g$)(a $:= (f $ a, c))" |
48028 | 1083 |
by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1) |
1084 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1085 |
lemma finfun_Diag_const_const [simp]: "($K$ b, K$ c$) = (K$ (b, c))" |
48028 | 1086 |
by(simp add: finfun_Diag_const1) |
1087 |
||
1088 |
lemma finfun_Diag_const_update: |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1089 |
"($K$ b, g(a $:= c)$) = ($K$ b, g$)(a $:= (b, c))" |
48028 | 1090 |
by(simp add: finfun_Diag_const1) |
1091 |
||
1092 |
lemma finfun_Diag_update_const: |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1093 |
"($f(a $:= b), K$ c$) = ($f, K$ c$)(a $:= (b, c))" |
48028 | 1094 |
by(simp add: finfun_Diag_def) |
1095 |
||
1096 |
lemma finfun_Diag_update_update: |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1097 |
"($f(a $:= b), g(a' $:= c)$) = (if a = a' then ($f, g$)(a $:= (b, c)) else ($f, g$)(a $:= (b, g $ a))(a' $:= (f $ a', c)))" |
48028 | 1098 |
by(auto simp add: finfun_Diag_update1 finfun_Diag_update2) |
1099 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1100 |
lemma finfun_Diag_apply [simp]: "op $ ($f, g$) = (\<lambda>x. (f $ x, g $ x))" |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1101 |
by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply) |
48028 | 1102 |
|
1103 |
lemma finfun_Diag_conv_Abs_finfun: |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1104 |
"($f, g$) = Abs_finfun ((\<lambda>x. (f $ x, g $ x)))" |
48030 | 1105 |
including finfun |
48028 | 1106 |
proof - |
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1107 |
have "(\<lambda>f :: 'a \<Rightarrow>f 'b. ($f, g$)) = (\<lambda>f. Abs_finfun ((\<lambda>x. (f $ x, g $ x))))" |
48028 | 1108 |
proof(rule finfun_rec_unique) |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1109 |
{ fix c show "Abs_finfun (\<lambda>x. ((K$ c) $ x, g $ x)) = Pair c \<circ>$ g" |
48029 | 1110 |
by(simp add: finfun_comp_conv_comp o_def finfun_const_def) } |
48028 | 1111 |
{ fix g' a b |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1112 |
show "Abs_finfun (\<lambda>x. (g'(a $:= b) $ x, g $ x)) = |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1113 |
(Abs_finfun (\<lambda>x. (g' $ x, g $ x)))(a $:= (b, g $ a))" |
48029 | 1114 |
by(auto simp add: finfun_update_def fun_eq_iff simp del: fun_upd_apply) simp } |
48028 | 1115 |
qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1) |
1116 |
thus ?thesis by(auto simp add: fun_eq_iff) |
|
1117 |
qed |
|
1118 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1119 |
lemma finfun_Diag_eq: "($f, g$) = ($f', g'$) \<longleftrightarrow> f = f' \<and> g = g'" |
48028 | 1120 |
by(auto simp add: expand_finfun_eq fun_eq_iff) |
1121 |
||
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1122 |
definition finfun_fst :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'b" |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1123 |
where [code]: "finfun_fst f = fst \<circ>$ f" |
48028 | 1124 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1125 |
lemma finfun_fst_const: "finfun_fst (K$ bc) = (K$ fst bc)" |
48028 | 1126 |
by(simp add: finfun_fst_def) |
1127 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1128 |
lemma finfun_fst_update: "finfun_fst (f(a $:= bc)) = (finfun_fst f)(a $:= fst bc)" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1129 |
and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(a $:= fst bc)" |
48028 | 1130 |
by(simp_all add: finfun_fst_def) |
1131 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1132 |
lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>$ g) = (fst \<circ> f) \<circ>$ g" |
48028 | 1133 |
by(simp add: finfun_fst_def) |
1134 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1135 |
lemma finfun_fst_conv [simp]: "finfun_fst ($f, g$) = f" |
48028 | 1136 |
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) |
1137 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1138 |
lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst \<circ> op $ f))" |
48029 | 1139 |
by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp) |
48028 | 1140 |
|
1141 |
||
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1142 |
definition finfun_snd :: "'a \<Rightarrow>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>f 'c" |
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1143 |
where [code]: "finfun_snd f = snd \<circ>$ f" |
48028 | 1144 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1145 |
lemma finfun_snd_const: "finfun_snd (K$ bc) = (K$ snd bc)" |
48028 | 1146 |
by(simp add: finfun_snd_def) |
1147 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1148 |
lemma finfun_snd_update: "finfun_snd (f(a $:= bc)) = (finfun_snd f)(a $:= snd bc)" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1149 |
and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(a $:= snd bc)" |
48028 | 1150 |
by(simp_all add: finfun_snd_def) |
1151 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1152 |
lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>$ g) = (snd \<circ> f) \<circ>$ g" |
48028 | 1153 |
by(simp add: finfun_snd_def) |
1154 |
||
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1155 |
lemma finfun_snd_conv [simp]: "finfun_snd ($f, g$) = g" |
48028 | 1156 |
apply(induct f rule: finfun_weak_induct) |
1157 |
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) |
|
1158 |
done |
|
1159 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
1160 |
lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd \<circ> op $ f))" |
48029 | 1161 |
by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp) |
48028 | 1162 |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1163 |
lemma finfun_Diag_collapse [simp]: "($finfun_fst f, finfun_snd f$) = f" |
48028 | 1164 |
by(induct f rule: finfun_weak_induct)(simp_all add: finfun_fst_const finfun_snd_const finfun_fst_update finfun_snd_update finfun_Diag_update_update) |
1165 |
||
60500 | 1166 |
subsection \<open>Currying for FinFuns\<close> |
48028 | 1167 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1168 |
definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c" |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1169 |
where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c)))" |
48028 | 1170 |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1171 |
interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))" |
48028 | 1172 |
apply(unfold_locales) |
1173 |
apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same) |
|
1174 |
done |
|
1175 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1176 |
interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))" |
48028 | 1177 |
proof(unfold_locales) |
1178 |
fix b' b :: 'b |
|
1179 |
assume fin: "finite (UNIV :: ('c \<times> 'a) set)" |
|
1180 |
hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)" |
|
1181 |
unfolding UNIV_Times_UNIV[symmetric] |
|
1182 |
by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+ |
|
1183 |
note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2] |
|
1184 |
{ fix A :: "('c \<times> 'a) set" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1185 |
interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c))) a b'" |
48028 | 1186 |
by(rule finfun_curry_aux.upd_left_comm) |
1187 |
from fin have "finite A" by(auto intro: finite_subset) |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1188 |
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))" |
48029 | 1189 |
by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def intro!: arg_cong[where f="Abs_finfun"] ext) } |
48028 | 1190 |
from this[of UNIV] |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1191 |
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'" |
48028 | 1192 |
by(simp add: finfun_const_def) |
1193 |
qed |
|
1194 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1195 |
lemma finfun_curry_const [simp, code]: "finfun_curry (K$ c) = (K$ K$ c)" |
48028 | 1196 |
by(simp add: finfun_curry_def) |
1197 |
||
1198 |
lemma finfun_curry_update [simp]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1199 |
"finfun_curry (f((a, b) $:= c)) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))" |
48028 | 1200 |
and finfun_curry_update_code [code]: |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1201 |
"finfun_curry (finfun_update_code f (a, b) c) = (finfun_curry f)(a $:= (finfun_curry f $ a)(b $:= c))" |
48028 | 1202 |
by(simp_all add: finfun_curry_def) |
1203 |
||
1204 |
lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun" |
|
1205 |
shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun" |
|
48030 | 1206 |
including finfun |
48028 | 1207 |
proof - |
1208 |
from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast |
|
1209 |
have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force) |
|
1210 |
hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}" |
|
1211 |
by(auto simp add: curry_def fun_eq_iff) |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1212 |
with fin c have "finite {a. Abs_finfun (curry f a) \<noteq> (K$ c)}" |
48028 | 1213 |
by(simp add: finfun_const_def finfun_curry) |
1214 |
thus ?thesis unfolding finfun_def by auto |
|
1215 |
qed |
|
1216 |
||
1217 |
lemma finfun_curry_conv_curry: |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1218 |
fixes f :: "('a \<times> 'b) \<Rightarrow>f 'c" |
48029 | 1219 |
shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a))" |
48030 | 1220 |
including finfun |
48028 | 1221 |
proof - |
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1222 |
have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply f) a)))" |
48028 | 1223 |
proof(rule finfun_rec_unique) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1224 |
fix c show "finfun_curry (K$ c) = (K$ K$ c)" by simp |
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1225 |
fix f a |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1226 |
show "finfun_curry (f(a $:= c)) = (finfun_curry f)(fst a $:= (finfun_curry f $ (fst a))(snd a $:= c))" |
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1227 |
by(cases a) simp |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1228 |
show "Abs_finfun (\<lambda>a. Abs_finfun (curry (finfun_apply (K$ c)) a)) = (K$ K$ c)" |
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1229 |
by(simp add: finfun_curry_def finfun_const_def curry_def) |
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1230 |
fix g b |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1231 |
show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (op $ g(a $:= b)) aa)) = |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1232 |
(Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a)))( |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1233 |
fst a $:= ((Abs_finfun (\<lambda>a. Abs_finfun (curry (op $ g) a))) $ (fst a))(snd a $:= b))" |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1234 |
by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_Abs_finfun_curry) |
48028 | 1235 |
qed |
1236 |
thus ?thesis by(auto simp add: fun_eq_iff) |
|
1237 |
qed |
|
1238 |
||
60500 | 1239 |
subsection \<open>Executable equality for FinFuns\<close> |
48028 | 1240 |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1241 |
lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))" |
48028 | 1242 |
by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def) |
1243 |
||
1244 |
instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
1245 |
definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))" |
48028 | 1246 |
instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def) |
1247 |
end |
|
1248 |
||
1249 |
lemma [code nbe]: |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1250 |
"HOL.equal (f :: _ \<Rightarrow>f _) f \<longleftrightarrow> True" |
48028 | 1251 |
by (fact equal_refl) |
1252 |
||
60500 | 1253 |
subsection \<open>An operator that explicitly removes all redundant updates in the generated representations\<close> |
48028 | 1254 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1255 |
definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b" |
48028 | 1256 |
where [simp, code del]: "finfun_clearjunk = id" |
1257 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1258 |
lemma finfun_clearjunk_const [code]: "finfun_clearjunk (K$ b) = (K$ b)" |
48028 | 1259 |
by simp |
1260 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1261 |
lemma finfun_clearjunk_update [code]: |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1262 |
"finfun_clearjunk (finfun_update_code f a b) = f(a $:= b)" |
48028 | 1263 |
by simp |
1264 |
||
60500 | 1265 |
subsection \<open>The domain of a FinFun as a FinFun\<close> |
48028 | 1266 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1267 |
definition finfun_dom :: "('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f bool)" |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1268 |
where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)" |
48028 | 1269 |
|
1270 |
lemma finfun_dom_const: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1271 |
"finfun_dom ((K$ c) :: 'a \<Rightarrow>f 'b) = (K$ finite (UNIV :: 'a set) \<and> c \<noteq> undefined)" |
48028 | 1272 |
unfolding finfun_dom_def finfun_default_const |
1273 |
by(auto)(simp_all add: finfun_const_def) |
|
1274 |
||
60500 | 1275 |
text \<open> |
48028 | 1276 |
@{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type. |
1277 |
For such FinFuns, the default value (and as such the domain) is undefined. |
|
60500 | 1278 |
\<close> |
48028 | 1279 |
|
1280 |
lemma finfun_dom_const_code [code]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1281 |
"finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = |
52916
5f3faf72b62a
prefer Code.abort with explicit error message
Andreas Lochbihler
parents:
51995
diff
changeset
|
1282 |
(if CARD('a) = 0 then (K$ False) else Code.abort (STR ''finfun_dom called on finite type'') (\<lambda>_. finfun_dom (K$ c)))" |
48059 | 1283 |
by(simp add: finfun_dom_const card_UNIV card_eq_0_iff) |
48028 | 1284 |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1285 |
lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun" |
48028 | 1286 |
using finite_finfun_default[of f] |
48029 | 1287 |
by(simp add: finfun_def exI[where x=False]) |
48028 | 1288 |
|
1289 |
lemma finfun_dom_update [simp]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1290 |
"finfun_dom (f(a $:= b)) = (finfun_dom f)(a $:= (b \<noteq> finfun_default f))" |
48030 | 1291 |
including finfun unfolding finfun_dom_def finfun_update_def |
58787 | 1292 |
apply(simp add: finfun_default_update_const finfun_dom_finfunI) |
48028 | 1293 |
apply(fold finfun_update.rep_eq) |
48029 | 1294 |
apply(simp add: finfun_upd_apply fun_eq_iff fun_upd_def finfun_default_update_const) |
48028 | 1295 |
done |
1296 |
||
1297 |
lemma finfun_dom_update_code [code]: |
|
1298 |
"finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)" |
|
1299 |
by(simp) |
|
1300 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1301 |
lemma finite_finfun_dom: "finite {x. finfun_dom f $ x}" |
48028 | 1302 |
proof(induct f rule: finfun_weak_induct) |
1303 |
case (const b) |
|
1304 |
thus ?case |
|
1305 |
by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined") |
|
1306 |
(auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric]) |
|
1307 |
next |
|
1308 |
case (update f a b) |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1309 |
have "{x. finfun_dom f(a $:= b) $ x} = |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1310 |
(if b = finfun_default f then {x. finfun_dom f $ x} - {a} else insert a {x. finfun_dom f $ x})" |
48028 | 1311 |
by (auto simp add: finfun_upd_apply split: split_if_asm) |
1312 |
thus ?case using update by simp |
|
1313 |
qed |
|
1314 |
||
1315 |
||
60500 | 1316 |
subsection \<open>The domain of a FinFun as a sorted list\<close> |
48028 | 1317 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48031
diff
changeset
|
1318 |
definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list" |
48028 | 1319 |
where |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1320 |
"finfun_to_list f = (THE xs. set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs)" |
48028 | 1321 |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1322 |
lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1) |
48028 | 1323 |
and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2) |
1324 |
and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3) |
|
60583 | 1325 |
proof (atomize (full)) |
1326 |
show "?thesis1 \<and> ?thesis2 \<and> ?thesis3" |
|
48028 | 1327 |
unfolding finfun_to_list_def |
1328 |
by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+ |
|
1329 |
qed |
|
1330 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1331 |
lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot" |
48028 | 1332 |
by auto |
1333 |
||
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1334 |
lemma finfun_const_True_conv_top: "op $ (K$ True) = top" |
48028 | 1335 |
by auto |
1336 |
||
1337 |
lemma finfun_to_list_const: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1338 |
"finfun_to_list ((K$ c) :: ('a :: {linorder} \<Rightarrow>f 'b)) = |
48028 | 1339 |
(if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)" |
1340 |
by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const) |
|
1341 |
||
1342 |
lemma finfun_to_list_const_code [code]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1343 |
"finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) = |
52916
5f3faf72b62a
prefer Code.abort with explicit error message
Andreas Lochbihler
parents:
51995
diff
changeset
|
1344 |
(if CARD('a) = 0 then [] else Code.abort (STR ''finfun_to_list called on finite type'') (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))" |
48059 | 1345 |
by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff) |
48028 | 1346 |
|
1347 |
lemma remove1_insort_insert_same: |
|
1348 |
"x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs" |
|
1349 |
by (metis insort_insert_insort remove1_insort) |
|
1350 |
||
1351 |
lemma finfun_dom_conv: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1352 |
"finfun_dom f $ x \<longleftrightarrow> f $ x \<noteq> finfun_default f" |
48028 | 1353 |
by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply) |
1354 |
||
1355 |
lemma finfun_to_list_update: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1356 |
"finfun_to_list (f(a $:= b)) = |
48028 | 1357 |
(if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))" |
1358 |
proof(subst finfun_to_list_def, rule the_equality) |
|
1359 |
fix xs |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1360 |
assume "set xs = {x. finfun_dom f(a $:= b) $ x} \<and> sorted xs \<and> distinct xs" |
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1361 |
hence eq: "set xs = {x. finfun_dom f(a $:= b) $ x}" |
48028 | 1362 |
and [simp]: "sorted xs" "distinct xs" by simp_all |
1363 |
show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))" |
|
1364 |
proof(cases "b = finfun_default f") |
|
60565 | 1365 |
case [simp]: True |
48028 | 1366 |
show ?thesis |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1367 |
proof(cases "finfun_dom f $ a") |
48028 | 1368 |
case True |
1369 |
have "finfun_to_list f = insort_insert a xs" |
|
1370 |
unfolding finfun_to_list_def |
|
1371 |
proof(rule the_equality) |
|
1372 |
have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert) |
|
1373 |
also note eq also |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1374 |
have "insert a {x. finfun_dom f(a $:= b) $ x} = {x. finfun_dom f $ x}" using True |
48028 | 1375 |
by(auto simp add: finfun_upd_apply split: split_if_asm) |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1376 |
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)" |
48028 | 1377 |
by(simp add: sorted_insort_insert distinct_insort_insert) |
1378 |
||
1379 |
fix xs' |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1380 |
assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'" |
48028 | 1381 |
thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique) |
1382 |
qed |
|
1383 |
with eq True show ?thesis by(simp add: remove1_insort_insert_same) |
|
1384 |
next |
|
1385 |
case False |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1386 |
hence "f $ a = b" by(auto simp add: finfun_dom_conv) |
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1387 |
hence f: "f(a $:= b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply) |
48028 | 1388 |
from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def |
1389 |
by(auto elim: sorted_distinct_set_unique intro!: the_equality) |
|
1390 |
with eq False show ?thesis unfolding f by(simp add: remove1_idem) |
|
1391 |
qed |
|
1392 |
next |
|
1393 |
case False |
|
1394 |
show ?thesis |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1395 |
proof(cases "finfun_dom f $ a") |
48028 | 1396 |
case True |
1397 |
have "finfun_to_list f = xs" |
|
1398 |
unfolding finfun_to_list_def |
|
1399 |
proof(rule the_equality) |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1400 |
have "finfun_dom f = finfun_dom f(a $:= b)" using False True |
48028 | 1401 |
by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply) |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1402 |
with eq show 1: "set xs = {x. finfun_dom f $ x} \<and> sorted xs \<and> distinct xs" |
48028 | 1403 |
by(simp del: finfun_dom_update) |
1404 |
||
1405 |
fix xs' |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1406 |
assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'" |
48028 | 1407 |
thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique) |
1408 |
qed |
|
1409 |
thus ?thesis using False True eq by(simp add: insort_insert_triv) |
|
1410 |
next |
|
1411 |
case False |
|
1412 |
have "finfun_to_list f = remove1 a xs" |
|
1413 |
unfolding finfun_to_list_def |
|
1414 |
proof(rule the_equality) |
|
1415 |
have "set (remove1 a xs) = set xs - {a}" by simp |
|
1416 |
also note eq also |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
1417 |
have "{x. finfun_dom f(a $:= b) $ x} - {a} = {x. finfun_dom f $ x}" using False |
48028 | 1418 |
by(auto simp add: finfun_upd_apply split: split_if_asm) |
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1419 |
finally show 1: "set (remove1 a xs) = {x. finfun_dom f $ x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)" |
48028 | 1420 |
by(simp add: sorted_remove1) |
1421 |
||
1422 |
fix xs' |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
1423 |
assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'" |
48028 | 1424 |
thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique) |
1425 |
qed |
|
60500 | 1426 |
thus ?thesis using False eq \<open>b \<noteq> finfun_default f\<close> |
48028 | 1427 |
by (simp add: insort_insert_insort insort_remove1) |
1428 |
qed |
|
1429 |
qed |
|
1430 |
qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: split_if_asm) |
|
1431 |
||
1432 |
lemma finfun_to_list_update_code [code]: |
|
1433 |
"finfun_to_list (finfun_update_code f a b) = |
|
1434 |
(if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))" |
|
1435 |
by(simp add: finfun_to_list_update) |
|
1436 |
||
60500 | 1437 |
text \<open>More type class instantiations\<close> |
51124
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1438 |
|
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1439 |
lemma card_eq_1_iff: "card A = 1 \<longleftrightarrow> A \<noteq> {} \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1440 |
(is "?lhs \<longleftrightarrow> ?rhs") |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1441 |
proof |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1442 |
assume ?lhs |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1443 |
moreover { |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1444 |
fix x y |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1445 |
assume A: "x \<in> A" "y \<in> A" and neq: "x \<noteq> y" |
60500 | 1446 |
have "finite A" using \<open>?lhs\<close> by(simp add: card_ge_0_finite) |
51124
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1447 |
from neq have "2 = card {x, y}" by simp |
60500 | 1448 |
also have "\<dots> \<le> card A" using A \<open>finite A\<close> |
51124
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1449 |
by(auto intro: card_mono) |
60500 | 1450 |
finally have False using \<open>?lhs\<close> by simp } |
51124
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1451 |
ultimately show ?rhs by auto |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1452 |
next |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1453 |
assume ?rhs |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1454 |
hence "A = {THE x. x \<in> A}" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1455 |
by safe (auto intro: theI the_equality[symmetric]) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1456 |
also have "card \<dots> = 1" by simp |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1457 |
finally show ?lhs . |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1458 |
qed |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1459 |
|
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1460 |
lemma card_UNIV_finfun: |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1461 |
defines "F == finfun :: ('a \<Rightarrow> 'b) set" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1462 |
shows "CARD('a \<Rightarrow>f 'b) = (if CARD('a) \<noteq> 0 \<and> CARD('b) \<noteq> 0 \<or> CARD('b) = 1 then CARD('b) ^ CARD('a) else 0)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1463 |
proof(cases "0 < CARD('a) \<and> 0 < CARD('b) \<or> CARD('b) = 1") |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1464 |
case True |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1465 |
from True have "F = UNIV" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1466 |
proof |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1467 |
assume b: "CARD('b) = 1" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1468 |
hence "\<forall>x :: 'b. x = undefined" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1469 |
by(auto simp add: card_eq_1_iff simp del: One_nat_def) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1470 |
thus ?thesis by(auto simp add: finfun_def F_def intro: exI[where x=undefined]) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1471 |
qed(auto simp add: finfun_def card_gt_0_iff F_def intro: finite_subset[where B=UNIV]) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1472 |
moreover have "CARD('a \<Rightarrow>f 'b) = card F" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1473 |
unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric] |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1474 |
by(auto intro!: card_image inj_onI simp add: Abs_finfun_inject F_def) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1475 |
ultimately show ?thesis by(simp add: card_fun) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1476 |
next |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1477 |
case False |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1478 |
hence infinite: "\<not> (finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set))" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1479 |
and b: "CARD('b) \<noteq> 1" by(simp_all add: card_eq_0_iff) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1480 |
from b obtain b1 b2 :: 'b where "b1 \<noteq> b2" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1481 |
by(auto simp add: card_eq_1_iff simp del: One_nat_def) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1482 |
let ?f = "\<lambda>a a' :: 'a. if a = a' then b1 else b2" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1483 |
from infinite have "\<not> finite (UNIV :: ('a \<Rightarrow>f 'b) set)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1484 |
proof(rule contrapos_nn[OF _ conjI]) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1485 |
assume finite: "finite (UNIV :: ('a \<Rightarrow>f 'b) set)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1486 |
hence "finite F" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1487 |
unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric] F_def |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1488 |
by(rule finite_imageD)(auto intro: inj_onI simp add: Abs_finfun_inject) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1489 |
hence "finite (range ?f)" |
60500 | 1490 |
by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def \<open>b1 \<noteq> b2\<close> intro!: exI[where x=b2]) |
51124
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1491 |
thus "finite (UNIV :: 'a set)" |
60500 | 1492 |
by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: split_if_asm) |
51124
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1493 |
|
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1494 |
from finite have "finite (range (\<lambda>b. ((K$ b) :: 'a \<Rightarrow>f 'b)))" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1495 |
by(rule finite_subset[rotated 1]) simp |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1496 |
thus "finite (UNIV :: 'b set)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1497 |
by(rule finite_imageD)(auto intro!: inj_onI) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1498 |
qed |
58787 | 1499 |
with False show ?thesis by auto |
51124
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1500 |
qed |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1501 |
|
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1502 |
lemma finite_UNIV_finfun: |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1503 |
"finite (UNIV :: ('a \<Rightarrow>f 'b) set) \<longleftrightarrow> |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1504 |
(finite (UNIV :: 'a set) \<and> finite (UNIV :: 'b set) \<or> CARD('b) = 1)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1505 |
(is "?lhs \<longleftrightarrow> ?rhs") |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1506 |
proof - |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1507 |
have "?lhs \<longleftrightarrow> CARD('a \<Rightarrow>f 'b) > 0" by(simp add: card_gt_0_iff) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1508 |
also have "\<dots> \<longleftrightarrow> CARD('a) > 0 \<and> CARD('b) > 0 \<or> CARD('b) = 1" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1509 |
by(simp add: card_UNIV_finfun) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1510 |
also have "\<dots> = ?rhs" by(simp add: card_gt_0_iff) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1511 |
finally show ?thesis . |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1512 |
qed |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1513 |
|
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1514 |
instantiation finfun :: (finite_UNIV, card_UNIV) finite_UNIV begin |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1515 |
definition "finite_UNIV = Phantom('a \<Rightarrow>f 'b) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1516 |
(let cb = of_phantom (card_UNIV :: 'b card_UNIV) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1517 |
in cb = 1 \<or> of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> cb \<noteq> 0)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1518 |
instance |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1519 |
by intro_classes (auto simp add: finite_UNIV_finfun_def Let_def card_UNIV finite_UNIV finite_UNIV_finfun card_gt_0_iff) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1520 |
end |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1521 |
|
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1522 |
instantiation finfun :: (card_UNIV, card_UNIV) card_UNIV begin |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1523 |
definition "card_UNIV = Phantom('a \<Rightarrow>f 'b) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1524 |
(let ca = of_phantom (card_UNIV :: 'a card_UNIV); |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1525 |
cb = of_phantom (card_UNIV :: 'b card_UNIV) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1526 |
in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)" |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1527 |
instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun) |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1528 |
end |
8fd094d5b7b7
instantiate finite_UNIV and card_UNIV for finfun type
Andreas Lochbihler
parents:
49834
diff
changeset
|
1529 |
|
61585 | 1530 |
text \<open>Deactivate syntax again. Import theory \<open>FinFun_Syntax\<close> to reactivate it again\<close> |
48041
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1531 |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1532 |
no_type_notation |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1533 |
finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1534 |
|
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1535 |
no_notation |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1536 |
finfun_const ("K$/ _" [0] 1) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1537 |
finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1538 |
finfun_apply (infixl "$" 999) and |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
1539 |
finfun_comp (infixr "\<circ>$" 55) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
1540 |
finfun_comp2 (infixr "$\<circ>" 55) and |
48041
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1541 |
finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000) |
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1542 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
1543 |
no_notation (ASCII) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
1544 |
finfun_comp (infixr "o$" 55) and |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61585
diff
changeset
|
1545 |
finfun_comp2 (infixr "$o" 55) |
48041
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
1546 |
|
48028 | 1547 |
end |