author | blanchet |
Tue, 16 Sep 2014 19:23:37 +0200 | |
changeset 58353 | c9f374b64d99 |
parent 58282 | 48e16d74845b |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
58128 | 1 |
(* Title: HOL/BNF_Composition.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
57698 | 3 |
Author: Jasmin Blanchette, TU Muenchen |
4 |
Copyright 2012, 2013, 2014 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
Composition of bounded natural functors. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
header {* Composition of Bounded Natural Functors *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
|
58128 | 11 |
theory BNF_Composition |
55936 | 12 |
imports BNF_Def |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
|
49312 | 15 |
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})" |
58128 | 16 |
by (rule ext) simp |
49312 | 17 |
|
18 |
lemma Union_natural: "Union o image (image f) = image f o Union" |
|
58128 | 19 |
by (rule ext) (auto simp only: comp_apply) |
49312 | 20 |
|
21 |
lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A" |
|
58128 | 22 |
by (unfold comp_assoc) |
49312 | 23 |
|
24 |
lemma comp_single_set_bd: |
|
25 |
assumes fbd_Card_order: "Card_order fbd" and |
|
26 |
fset_bd: "\<And>x. |fset x| \<le>o fbd" and |
|
27 |
gset_bd: "\<And>x. |gset x| \<le>o gbd" |
|
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset
|
28 |
shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd" |
58128 | 29 |
apply simp |
30 |
apply (rule ordLeq_transitive) |
|
31 |
apply (rule card_of_UNION_Sigma) |
|
32 |
apply (subst SIGMA_CSUM) |
|
33 |
apply (rule ordLeq_transitive) |
|
34 |
apply (rule card_of_Csum_Times') |
|
35 |
apply (rule fbd_Card_order) |
|
36 |
apply (rule ballI) |
|
37 |
apply (rule fset_bd) |
|
38 |
apply (rule ordLeq_transitive) |
|
39 |
apply (rule cprod_mono1) |
|
40 |
apply (rule gset_bd) |
|
41 |
apply (rule ordIso_imp_ordLeq) |
|
42 |
apply (rule ordIso_refl) |
|
43 |
apply (rule Card_order_cprod) |
|
44 |
done |
|
49312 | 45 |
|
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
46 |
lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r" |
58128 | 47 |
apply (erule ordIso_transitive) |
48 |
apply (frule csum_absorb2') |
|
49 |
apply (erule ordLeq_refl) |
|
50 |
by simp |
|
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
51 |
|
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
52 |
lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r" |
58128 | 53 |
apply (erule ordIso_transitive) |
54 |
apply (rule cprod_infinite) |
|
55 |
by simp |
|
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
56 |
|
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset
|
57 |
lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)" |
58128 | 58 |
by simp |
49312 | 59 |
|
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset
|
60 |
lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A" |
58128 | 61 |
by simp |
49312 | 62 |
|
63 |
lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F" |
|
58128 | 64 |
by (rule ext) (auto simp add: collect_def) |
49312 | 65 |
|
66 |
lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" |
|
58128 | 67 |
by blast |
49312 | 68 |
|
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset
|
69 |
lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" |
58128 | 70 |
by blast |
49312 | 71 |
|
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51893
diff
changeset
|
72 |
lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd" |
58128 | 73 |
by (unfold comp_apply collect_def) simp |
49312 | 74 |
|
75 |
lemma wpull_cong: |
|
58128 | 76 |
"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2" |
77 |
by simp |
|
49312 | 78 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset
|
79 |
lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R" |
58128 | 80 |
unfolding Grp_def fun_eq_iff relcompp.simps by auto |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset
|
81 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset
|
82 |
lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g" |
58128 | 83 |
by (rule arg_cong) |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
49512
diff
changeset
|
84 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
85 |
lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow> |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
86 |
vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
87 |
unfolding vimage2p_def by auto |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
88 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
89 |
lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
90 |
by auto |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
91 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
92 |
lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
93 |
by auto |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
94 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
95 |
lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
96 |
by simp |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
97 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
98 |
context |
58128 | 99 |
fixes Rep Abs |
100 |
assumes type_copy: "type_definition Rep Abs UNIV" |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
101 |
begin |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
102 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
103 |
lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
104 |
using type_definition.Rep_inverse[OF type_copy] by auto |
55811 | 105 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
106 |
lemma type_copy_map_comp0: "M = M1 o M2 \<Longrightarrow> f o M o g = (f o M1 o Rep) o (Abs o M2 o g)" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
107 |
using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto |
55811 | 108 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
109 |
lemma type_copy_set_map0: "S o M = image f o S' \<Longrightarrow> (S o Rep) o (Abs o M o g) = image f o (S' o g)" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
110 |
using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff) |
55811 | 111 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
112 |
lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
113 |
using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto |
55811 | 114 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
115 |
lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
116 |
Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
117 |
unfolding vimage2p_def Grp_def fun_eq_iff |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
118 |
by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
119 |
type_definition.Rep_inverse[OF type_copy] dest: sym) |
55811 | 120 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
121 |
lemma type_copy_vimage2p_Grp_Abs: |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
122 |
"\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
123 |
unfolding vimage2p_def Grp_def fun_eq_iff |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
124 |
by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I] |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
125 |
type_definition.Rep_inverse[OF type_copy] dest: sym) |
55811 | 126 |
|
127 |
lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))" |
|
128 |
proof safe |
|
129 |
fix b assume "F b" |
|
130 |
show "\<exists>b'. F (Rep b')" |
|
131 |
proof (rule exI) |
|
132 |
from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto |
|
133 |
qed |
|
134 |
qed blast |
|
135 |
||
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
136 |
lemma vimage2p_relcompp_converse: |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
137 |
"vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S" |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
138 |
unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def |
55811 | 139 |
by (auto simp: type_copy_ex_RepI) |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
140 |
|
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
141 |
end |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55705
diff
changeset
|
142 |
|
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
143 |
bnf DEADID: 'a |
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
144 |
map: "id :: 'a \<Rightarrow> 'a" |
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
145 |
bd: natLeq |
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
146 |
rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" |
58128 | 147 |
by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) |
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
148 |
|
58353 | 149 |
definition id_bnf :: "'a \<Rightarrow> 'a" where |
150 |
"id_bnf \<equiv> (\<lambda>x. x)" |
|
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
151 |
|
58181 | 152 |
lemma id_bnf_apply: "id_bnf x = x" |
153 |
unfolding id_bnf_def by simp |
|
56016
8875cdcfc85b
unfold intermediate definitions after sealing the bnf
traytel
parents:
55936
diff
changeset
|
154 |
|
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
155 |
bnf ID: 'a |
58181 | 156 |
map: "id_bnf :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
55935
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
157 |
sets: "\<lambda>x. {x}" |
8f20d09d294e
move special BNFs used for composition only to BNF_Comp;
traytel
parents:
55930
diff
changeset
|
158 |
bd: natLeq |
58181 | 159 |
rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
160 |
unfolding id_bnf_def |
|
58128 | 161 |
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite) |
162 |
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
|
163 |
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] |
|
164 |
done |
|
55854
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55851
diff
changeset
|
165 |
|
58181 | 166 |
lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV" |
167 |
unfolding id_bnf_def by unfold_locales auto |
|
55854
ee270328a781
make 'typedef' optional, depending on size of original type
blanchet
parents:
55851
diff
changeset
|
168 |
|
55062 | 169 |
ML_file "Tools/BNF/bnf_comp_tactics.ML" |
170 |
ML_file "Tools/BNF/bnf_comp.ML" |
|
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
171 |
|
58282 | 172 |
hide_fact |
173 |
DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0 |
|
174 |
DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer |
|
175 |
DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq |
|
176 |
DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer |
|
177 |
ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id |
|
178 |
ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep |
|
179 |
ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer |
|
180 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
end |