12 projective limit. @{const extensional} functions are used for the representation in order to |
12 projective limit. @{const extensional} functions are used for the representation in order to |
13 stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra |
13 stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra |
14 @{const Pi\<^sub>M}.\<close> |
14 @{const Pi\<^sub>M}.\<close> |
15 |
15 |
16 typedef ('i, 'a) finmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21) = |
16 typedef ('i, 'a) finmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21) = |
17 "{(I::'i set, f::'i \<Rightarrow> 'a). finite I \<and> f \<in> extensional I}" by auto |
17 "{f::'i \<Rightarrow> 'a option. finite (dom f)}" |
|
18 by (auto intro!: exI[where x="\<lambda>_. None"]) |
|
19 |
|
20 setup_lifting type_definition_finmap |
|
21 |
18 |
22 |
19 subsection \<open>Domain and Application\<close> |
23 subsection \<open>Domain and Application\<close> |
20 |
24 |
21 definition domain where "domain P = fst (Rep_finmap P)" |
25 lift_definition domain::"('i, 'a) finmap \<Rightarrow> 'i set" is dom . |
22 |
26 |
23 lemma finite_domain[simp, intro]: "finite (domain P)" |
27 lemma finite_domain[simp, intro]: "finite (domain P)" |
24 by (cases P) (auto simp: domain_def Abs_finmap_inverse) |
28 by transfer simp |
25 |
29 |
26 definition proj ("'((_)')\<^sub>F" [0] 1000) where "proj P i = snd (Rep_finmap P) i" |
30 lift_definition proj :: "('i, 'a) finmap \<Rightarrow> 'i \<Rightarrow> 'a" ("'((_)')\<^sub>F" [0] 1000) is |
|
31 "\<lambda>f x. if x \<in> dom f then the (f x) else undefined" . |
27 |
32 |
28 declare [[coercion proj]] |
33 declare [[coercion proj]] |
29 |
34 |
30 lemma extensional_proj[simp, intro]: "(P)\<^sub>F \<in> extensional (domain P)" |
35 lemma extensional_proj[simp, intro]: "(P)\<^sub>F \<in> extensional (domain P)" |
31 by (cases P) (auto simp: domain_def Abs_finmap_inverse proj_def[abs_def]) |
36 by transfer (auto simp: extensional_def) |
32 |
37 |
33 lemma proj_undefined[simp, intro]: "i \<notin> domain P \<Longrightarrow> P i = undefined" |
38 lemma proj_undefined[simp, intro]: "i \<notin> domain P \<Longrightarrow> P i = undefined" |
34 using extensional_proj[of P] unfolding extensional_def by auto |
39 using extensional_proj[of P] unfolding extensional_def by auto |
35 |
40 |
36 lemma finmap_eq_iff: "P = Q \<longleftrightarrow> (domain P = domain Q \<and> (\<forall>i\<in>domain P. P i = Q i))" |
41 lemma finmap_eq_iff: "P = Q \<longleftrightarrow> (domain P = domain Q \<and> (\<forall>i\<in>domain P. P i = Q i))" |
37 by (cases P, cases Q) |
42 apply transfer |
38 (auto simp add: Abs_finmap_inject extensional_def domain_def proj_def Abs_finmap_inverse |
43 apply (safe intro!: ext) |
39 intro: extensionalityI) |
44 subgoal for P Q x |
|
45 by (cases "x \<in> dom P"; cases "P x") (auto dest!: bspec[where x=x]) |
|
46 done |
|
47 |
40 |
48 |
41 subsection \<open>Countable Finite Maps\<close> |
49 subsection \<open>Countable Finite Maps\<close> |
42 |
50 |
43 instance finmap :: (countable, countable) countable |
51 instance finmap :: (countable, countable) countable |
44 proof |
52 proof |
58 by (intro exI[of _ "to_nat \<circ> ?F"] inj_comp) auto |
66 by (intro exI[of _ "to_nat \<circ> ?F"] inj_comp) auto |
59 qed |
67 qed |
60 |
68 |
61 subsection \<open>Constructor of Finite Maps\<close> |
69 subsection \<open>Constructor of Finite Maps\<close> |
62 |
70 |
63 definition "finmap_of inds f = Abs_finmap (inds, restrict f inds)" |
71 lift_definition finmap_of::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) \<Rightarrow> ('i, 'a) finmap" is |
|
72 "\<lambda>I f x. if x \<in> I \<and> finite I then Some (f x) else None" |
|
73 by (simp add: dom_def) |
64 |
74 |
65 lemma proj_finmap_of[simp]: |
75 lemma proj_finmap_of[simp]: |
66 assumes "finite inds" |
76 assumes "finite inds" |
67 shows "(finmap_of inds f)\<^sub>F = restrict f inds" |
77 shows "(finmap_of inds f)\<^sub>F = restrict f inds" |
68 using assms |
78 using assms |
69 by (auto simp: Abs_finmap_inverse finmap_of_def proj_def) |
79 by transfer force |
70 |
80 |
71 lemma domain_finmap_of[simp]: |
81 lemma domain_finmap_of[simp]: |
72 assumes "finite inds" |
82 assumes "finite inds" |
73 shows "domain (finmap_of inds f) = inds" |
83 shows "domain (finmap_of inds f) = inds" |
74 using assms |
84 using assms |
75 by (auto simp: Abs_finmap_inverse finmap_of_def domain_def) |
85 by transfer (auto split: if_splits) |
76 |
86 |
77 lemma finmap_of_eq_iff[simp]: |
87 lemma finmap_of_eq_iff[simp]: |
78 assumes "finite i" "finite j" |
88 assumes "finite i" "finite j" |
79 shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> (\<forall>k\<in>i. m k= n k)" |
89 shows "finmap_of i m = finmap_of j n \<longleftrightarrow> i = j \<and> (\<forall>k\<in>i. m k= n k)" |
80 using assms by (auto simp: finmap_eq_iff) |
90 using assms by (auto simp: finmap_eq_iff) |