author | wenzelm |
Sat, 17 Mar 2018 20:32:39 +0100 | |
changeset 67895 | cd00999d2d30 |
parent 67682 | 00c436488398 |
child 68358 | e761afd35baa |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Map_Functions.thy |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
3 |
*) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
4 |
|
62175 | 5 |
section \<open>Map functions for various types\<close> |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
6 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
7 |
theory Map_Functions |
67312 | 8 |
imports Deflation Sprod Ssum Sfun Up |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
9 |
begin |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
10 |
|
62175 | 11 |
subsection \<open>Map operator for continuous function space\<close> |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
12 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
13 |
default_sort cpo |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
14 |
|
67312 | 15 |
definition cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)" |
16 |
where "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
17 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
18 |
lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))" |
67312 | 19 |
by (simp add: cfun_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
20 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
21 |
lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID" |
67312 | 22 |
by (simp add: cfun_eq_iff) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
23 |
|
67312 | 24 |
lemma cfun_map_map: "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) = cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
25 |
by (rule cfun_eqI) simp |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
26 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
27 |
lemma ep_pair_cfun_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
28 |
assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
29 |
shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
30 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
31 |
interpret e1p1: ep_pair e1 p1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
32 |
interpret e2p2: ep_pair e2 p2 by fact |
67312 | 33 |
show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" for f |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
34 |
by (simp add: cfun_eq_iff) |
67312 | 35 |
show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" for g |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
36 |
apply (rule cfun_belowI, simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
37 |
apply (rule below_trans [OF e2p2.e_p_below]) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
38 |
apply (rule monofun_cfun_arg) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
39 |
apply (rule e1p1.e_p_below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
40 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
41 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
42 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
43 |
lemma deflation_cfun_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
44 |
assumes "deflation d1" and "deflation d2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
45 |
shows "deflation (cfun_map\<cdot>d1\<cdot>d2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
46 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
47 |
interpret d1: deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
48 |
interpret d2: deflation d2 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
49 |
fix f |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
50 |
show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
51 |
by (simp add: cfun_eq_iff d1.idem d2.idem) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
52 |
show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
53 |
apply (rule cfun_belowI, simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
54 |
apply (rule below_trans [OF d2.below]) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
55 |
apply (rule monofun_cfun_arg) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
56 |
apply (rule d1.below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
57 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
58 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
59 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
60 |
lemma finite_range_cfun_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
61 |
assumes a: "finite (range (\<lambda>x. a\<cdot>x))" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
62 |
assumes b: "finite (range (\<lambda>y. b\<cdot>y))" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
63 |
shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))" (is "finite (range ?h)") |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
64 |
proof (rule finite_imageD) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
65 |
let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
66 |
show "finite (?f ` range ?h)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
67 |
proof (rule finite_subset) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
68 |
let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
69 |
show "?f ` range ?h \<subseteq> ?B" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
70 |
by clarsimp |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
71 |
show "finite ?B" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
72 |
by (simp add: a b) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
73 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
74 |
show "inj_on ?f (range ?h)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
75 |
proof (rule inj_onI, rule cfun_eqI, clarsimp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
76 |
fix x f g |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
77 |
assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" |
67312 | 78 |
then have "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
79 |
by (rule equalityD1) |
67312 | 80 |
then have "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
81 |
by (simp add: subset_eq) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
82 |
then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
83 |
by (rule rangeE) |
67312 | 84 |
then show "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
85 |
by clarsimp |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
86 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
87 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
88 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
89 |
lemma finite_deflation_cfun_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
90 |
assumes "finite_deflation d1" and "finite_deflation d2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
91 |
shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
92 |
proof (rule finite_deflation_intro) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
93 |
interpret d1: finite_deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
94 |
interpret d2: finite_deflation d2 by fact |
67682
00c436488398
tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents:
67312
diff
changeset
|
95 |
from d1.deflation_axioms d2.deflation_axioms show "deflation (cfun_map\<cdot>d1\<cdot>d2)" |
67312 | 96 |
by (rule deflation_cfun_map) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
97 |
have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
98 |
using d1.finite_range d2.finite_range |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
99 |
by (rule finite_range_cfun_map) |
67312 | 100 |
then show "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
101 |
by (rule finite_range_imp_finite_fixes) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
102 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
103 |
|
62175 | 104 |
text \<open>Finite deflations are compact elements of the function space\<close> |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
105 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
106 |
lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d" |
67312 | 107 |
apply (frule finite_deflation_imp_deflation) |
108 |
apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)") |
|
109 |
apply (simp add: cfun_map_def deflation.idem eta_cfun) |
|
110 |
apply (rule finite_deflation.compact) |
|
111 |
apply (simp only: finite_deflation_cfun_map) |
|
112 |
done |
|
113 |
||
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
114 |
|
62175 | 115 |
subsection \<open>Map operator for product type\<close> |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
116 |
|
67312 | 117 |
definition prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd" |
118 |
where "prod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
119 |
|
41297 | 120 |
lemma prod_map_Pair [simp]: "prod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)" |
67312 | 121 |
by (simp add: prod_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
122 |
|
41297 | 123 |
lemma prod_map_ID: "prod_map\<cdot>ID\<cdot>ID = ID" |
67312 | 124 |
by (auto simp: cfun_eq_iff) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
125 |
|
67312 | 126 |
lemma prod_map_map: "prod_map\<cdot>f1\<cdot>g1\<cdot>(prod_map\<cdot>f2\<cdot>g2\<cdot>p) = prod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
127 |
by (induct p) simp |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
128 |
|
41297 | 129 |
lemma ep_pair_prod_map: |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
130 |
assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
41297 | 131 |
shows "ep_pair (prod_map\<cdot>e1\<cdot>e2) (prod_map\<cdot>p1\<cdot>p2)" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
132 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
133 |
interpret e1p1: ep_pair e1 p1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
134 |
interpret e2p2: ep_pair e2 p2 by fact |
67312 | 135 |
show "prod_map\<cdot>p1\<cdot>p2\<cdot>(prod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
136 |
by (induct x) simp |
67312 | 137 |
show "prod_map\<cdot>e1\<cdot>e2\<cdot>(prod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
138 |
by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
139 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
140 |
|
41297 | 141 |
lemma deflation_prod_map: |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
142 |
assumes "deflation d1" and "deflation d2" |
41297 | 143 |
shows "deflation (prod_map\<cdot>d1\<cdot>d2)" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
144 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
145 |
interpret d1: deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
146 |
interpret d2: deflation d2 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
147 |
fix x |
41297 | 148 |
show "prod_map\<cdot>d1\<cdot>d2\<cdot>(prod_map\<cdot>d1\<cdot>d2\<cdot>x) = prod_map\<cdot>d1\<cdot>d2\<cdot>x" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
149 |
by (induct x) (simp add: d1.idem d2.idem) |
41297 | 150 |
show "prod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
151 |
by (induct x) (simp add: d1.below d2.below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
152 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
153 |
|
41297 | 154 |
lemma finite_deflation_prod_map: |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
155 |
assumes "finite_deflation d1" and "finite_deflation d2" |
41297 | 156 |
shows "finite_deflation (prod_map\<cdot>d1\<cdot>d2)" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
157 |
proof (rule finite_deflation_intro) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
158 |
interpret d1: finite_deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
159 |
interpret d2: finite_deflation d2 by fact |
67682
00c436488398
tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents:
67312
diff
changeset
|
160 |
from d1.deflation_axioms d2.deflation_axioms show "deflation (prod_map\<cdot>d1\<cdot>d2)" |
00c436488398
tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents:
67312
diff
changeset
|
161 |
by (rule deflation_prod_map) |
41297 | 162 |
have "{p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}" |
67312 | 163 |
by auto |
164 |
then show "finite {p. prod_map\<cdot>d1\<cdot>d2\<cdot>p = p}" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
165 |
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
166 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
167 |
|
67312 | 168 |
|
62175 | 169 |
subsection \<open>Map function for lifted cpo\<close> |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
170 |
|
67312 | 171 |
definition u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u" |
172 |
where "u_map = (\<Lambda> f. fup\<cdot>(up oo f))" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
173 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
174 |
lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>" |
67312 | 175 |
by (simp add: u_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
176 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
177 |
lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)" |
67312 | 178 |
by (simp add: u_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
179 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
180 |
lemma u_map_ID: "u_map\<cdot>ID = ID" |
67312 | 181 |
by (simp add: u_map_def cfun_eq_iff eta_cfun) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
182 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
183 |
lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p" |
67312 | 184 |
by (induct p) simp_all |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
185 |
|
41291 | 186 |
lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g" |
67312 | 187 |
by (simp add: cfcomp1 u_map_map eta_cfun) |
41291 | 188 |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
189 |
lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)" |
67312 | 190 |
apply standard |
191 |
subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse) |
|
192 |
subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below) |
|
193 |
done |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
194 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
195 |
lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)" |
67312 | 196 |
apply standard |
197 |
subgoal for x by (cases x, simp, simp add: deflation.idem) |
|
198 |
subgoal for x by (cases x, simp, simp add: deflation.below) |
|
199 |
done |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
200 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
201 |
lemma finite_deflation_u_map: |
67312 | 202 |
assumes "finite_deflation d" |
203 |
shows "finite_deflation (u_map\<cdot>d)" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
204 |
proof (rule finite_deflation_intro) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
205 |
interpret d: finite_deflation d by fact |
67682
00c436488398
tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents:
67312
diff
changeset
|
206 |
from d.deflation_axioms show "deflation (u_map\<cdot>d)" |
67312 | 207 |
by (rule deflation_u_map) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
208 |
have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
209 |
by (rule subsetI, case_tac x, simp_all) |
67312 | 210 |
then show "finite {x. u_map\<cdot>d\<cdot>x = x}" |
211 |
by (rule finite_subset) (simp add: d.finite_fixes) |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
212 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
213 |
|
67312 | 214 |
|
62175 | 215 |
subsection \<open>Map function for strict products\<close> |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
216 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
217 |
default_sort pcpo |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
218 |
|
67312 | 219 |
definition sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd" |
220 |
where "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
221 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
222 |
lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
67312 | 223 |
by (simp add: sprod_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
224 |
|
67312 | 225 |
lemma sprod_map_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
226 |
by (simp add: sprod_map_def) |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
227 |
|
67312 | 228 |
lemma sprod_map_spair': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
229 |
by (cases "x = \<bottom> \<or> y = \<bottom>") auto |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
230 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
231 |
lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID" |
67312 | 232 |
by (simp add: sprod_map_def cfun_eq_iff eta_cfun) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
233 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
234 |
lemma sprod_map_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
235 |
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
236 |
sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) = |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
237 |
sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
67312 | 238 |
apply (induct p) |
239 |
apply simp |
|
240 |
apply (case_tac "f2\<cdot>x = \<bottom>", simp) |
|
241 |
apply (case_tac "g2\<cdot>y = \<bottom>", simp) |
|
242 |
apply simp |
|
243 |
done |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
244 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
245 |
lemma ep_pair_sprod_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
246 |
assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
247 |
shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
248 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
249 |
interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
250 |
interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
67312 | 251 |
show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
252 |
by (induct x) simp_all |
67312 | 253 |
show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
254 |
apply (induct y) |
|
255 |
apply simp |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
256 |
apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
257 |
apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
258 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
259 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
260 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
261 |
lemma deflation_sprod_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
262 |
assumes "deflation d1" and "deflation d2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
263 |
shows "deflation (sprod_map\<cdot>d1\<cdot>d2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
264 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
265 |
interpret d1: deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
266 |
interpret d2: deflation d2 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
267 |
fix x |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
268 |
show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
269 |
apply (induct x, simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
270 |
apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
271 |
apply (simp add: d1.idem d2.idem) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
272 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
273 |
show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
274 |
apply (induct x, simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
275 |
apply (simp add: monofun_cfun d1.below d2.below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
276 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
277 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
278 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
279 |
lemma finite_deflation_sprod_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
280 |
assumes "finite_deflation d1" and "finite_deflation d2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
281 |
shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
282 |
proof (rule finite_deflation_intro) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
283 |
interpret d1: finite_deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
284 |
interpret d2: finite_deflation d2 by fact |
67682
00c436488398
tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents:
67312
diff
changeset
|
285 |
from d1.deflation_axioms d2.deflation_axioms show "deflation (sprod_map\<cdot>d1\<cdot>d2)" |
67312 | 286 |
by (rule deflation_sprod_map) |
287 |
have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> |
|
288 |
insert \<bottom> ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
289 |
by (rule subsetI, case_tac x, auto simp add: spair_eq_iff) |
67312 | 290 |
then show "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
291 |
by (rule finite_subset) (simp add: d1.finite_fixes d2.finite_fixes) |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
292 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
293 |
|
67312 | 294 |
|
62175 | 295 |
subsection \<open>Map function for strict sums\<close> |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
296 |
|
67312 | 297 |
definition ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd" |
298 |
where "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))" |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
299 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
300 |
lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>" |
67312 | 301 |
by (simp add: ssum_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
302 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
303 |
lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
67312 | 304 |
by (simp add: ssum_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
305 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
306 |
lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
67312 | 307 |
by (simp add: ssum_map_def) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
308 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
309 |
lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
67312 | 310 |
by (cases "x = \<bottom>") simp_all |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
311 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
312 |
lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
67312 | 313 |
by (cases "x = \<bottom>") simp_all |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
314 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
315 |
lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID" |
67312 | 316 |
by (simp add: ssum_map_def cfun_eq_iff eta_cfun) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
317 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
318 |
lemma ssum_map_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
319 |
"\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
320 |
ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) = |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
321 |
ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
67312 | 322 |
apply (induct p) |
323 |
apply simp |
|
324 |
apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp) |
|
325 |
apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp) |
|
326 |
done |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
327 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
328 |
lemma ep_pair_ssum_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
329 |
assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
330 |
shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
331 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
332 |
interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
333 |
interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
67312 | 334 |
show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
335 |
by (induct x) simp_all |
67312 | 336 |
show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
337 |
apply (induct y) |
|
338 |
apply simp |
|
339 |
apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below) |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
340 |
apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
341 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
342 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
343 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
344 |
lemma deflation_ssum_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
345 |
assumes "deflation d1" and "deflation d2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
346 |
shows "deflation (ssum_map\<cdot>d1\<cdot>d2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
347 |
proof |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
348 |
interpret d1: deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
349 |
interpret d2: deflation d2 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
350 |
fix x |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
351 |
show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
352 |
apply (induct x, simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
353 |
apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
354 |
apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
355 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
356 |
show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
357 |
apply (induct x, simp) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
358 |
apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
359 |
apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
360 |
done |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
361 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
362 |
|
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
363 |
lemma finite_deflation_ssum_map: |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
364 |
assumes "finite_deflation d1" and "finite_deflation d2" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
365 |
shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
366 |
proof (rule finite_deflation_intro) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
367 |
interpret d1: finite_deflation d1 by fact |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
368 |
interpret d2: finite_deflation d2 by fact |
67682
00c436488398
tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents:
67312
diff
changeset
|
369 |
from d1.deflation_axioms d2.deflation_axioms show "deflation (ssum_map\<cdot>d1\<cdot>d2)" |
67312 | 370 |
by (rule deflation_ssum_map) |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
371 |
have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
372 |
(\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union> |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
373 |
(\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}" |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
374 |
by (rule subsetI, case_tac x, simp_all) |
67312 | 375 |
then show "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
376 |
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
377 |
qed |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
378 |
|
67312 | 379 |
|
62175 | 380 |
subsection \<open>Map operator for strict function space\<close> |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
381 |
|
67312 | 382 |
definition sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)" |
383 |
where "sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)" |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
384 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
385 |
lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID" |
67312 | 386 |
by (simp add: sfun_map_def cfun_map_ID cfun_eq_iff) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
387 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
388 |
lemma sfun_map_map: |
67312 | 389 |
assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" |
390 |
shows "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) = |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
391 |
sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
67312 | 392 |
by (simp add: sfun_map_def cfun_eq_iff strictify_cancel assms cfun_map_map) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
393 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
394 |
lemma ep_pair_sfun_map: |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
395 |
assumes 1: "ep_pair e1 p1" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
396 |
assumes 2: "ep_pair e2 p2" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
397 |
shows "ep_pair (sfun_map\<cdot>p1\<cdot>e2) (sfun_map\<cdot>e1\<cdot>p2)" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
398 |
proof |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
399 |
interpret e1p1: pcpo_ep_pair e1 p1 |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
400 |
unfolding pcpo_ep_pair_def by fact |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
401 |
interpret e2p2: pcpo_ep_pair e2 p2 |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
402 |
unfolding pcpo_ep_pair_def by fact |
67312 | 403 |
show "sfun_map\<cdot>e1\<cdot>p2\<cdot>(sfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" for f |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
404 |
unfolding sfun_map_def |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
405 |
apply (simp add: sfun_eq_iff strictify_cancel) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
406 |
apply (rule ep_pair.e_inverse) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
407 |
apply (rule ep_pair_cfun_map [OF 1 2]) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
408 |
done |
67312 | 409 |
show "sfun_map\<cdot>p1\<cdot>e2\<cdot>(sfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" for g |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
410 |
unfolding sfun_map_def |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
411 |
apply (simp add: sfun_below_iff strictify_cancel) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
412 |
apply (rule ep_pair.e_p_below) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
413 |
apply (rule ep_pair_cfun_map [OF 1 2]) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
414 |
done |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
415 |
qed |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
416 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
417 |
lemma deflation_sfun_map: |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
418 |
assumes 1: "deflation d1" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
419 |
assumes 2: "deflation d2" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
420 |
shows "deflation (sfun_map\<cdot>d1\<cdot>d2)" |
67312 | 421 |
apply (simp add: sfun_map_def) |
422 |
apply (rule deflation.intro) |
|
423 |
apply simp |
|
424 |
apply (subst strictify_cancel) |
|
425 |
apply (simp add: cfun_map_def deflation_strict 1 2) |
|
426 |
apply (simp add: cfun_map_def deflation.idem 1 2) |
|
427 |
apply (simp add: sfun_below_iff) |
|
428 |
apply (subst strictify_cancel) |
|
429 |
apply (simp add: cfun_map_def deflation_strict 1 2) |
|
430 |
apply (rule deflation.below) |
|
431 |
apply (rule deflation_cfun_map [OF 1 2]) |
|
432 |
done |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
433 |
|
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
434 |
lemma finite_deflation_sfun_map: |
67312 | 435 |
assumes "finite_deflation d1" |
436 |
and "finite_deflation d2" |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
437 |
shows "finite_deflation (sfun_map\<cdot>d1\<cdot>d2)" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
438 |
proof (intro finite_deflation_intro) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
439 |
interpret d1: finite_deflation d1 by fact |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
440 |
interpret d2: finite_deflation d2 by fact |
67682
00c436488398
tuned proofs -- prefer explicit names for facts from 'interpret';
wenzelm
parents:
67312
diff
changeset
|
441 |
from d1.deflation_axioms d2.deflation_axioms show "deflation (sfun_map\<cdot>d1\<cdot>d2)" |
67312 | 442 |
by (rule deflation_sfun_map) |
443 |
from assms have "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
444 |
by (rule finite_deflation_cfun_map) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
445 |
then have "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
446 |
by (rule finite_deflation.finite_fixes) |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
447 |
moreover have "inj (\<lambda>f. sfun_rep\<cdot>f)" |
67312 | 448 |
by (rule inj_onI) (simp add: sfun_eq_iff) |
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
449 |
ultimately have "finite ((\<lambda>f. sfun_rep\<cdot>f) -` {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f})" |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
450 |
by (rule finite_vimageI) |
67312 | 451 |
with \<open>deflation d1\<close> \<open>deflation d2\<close> show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
452 |
by (simp add: sfun_map_def sfun_eq_iff strictify_cancel deflation_strict) |
|
40592
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
453 |
qed |
f432973ce0f6
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents:
40502
diff
changeset
|
454 |
|
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff
changeset
|
455 |
end |