|
1 (* Title: HOL/BNF_Fixpoint_Base.thy |
|
2 Author: Lorenz Panny, TU Muenchen |
|
3 Author: Dmitriy Traytel, TU Muenchen |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Author: Martin Desharnais, TU Muenchen |
|
6 Copyright 2012, 2013, 2014 |
|
7 |
|
8 Shared fixed point operations on bounded natural functors. |
|
9 *) |
|
10 |
|
11 header {* Shared Fixed Point Operations on Bounded Natural Functors *} |
|
12 |
|
13 theory BNF_Fixpoint_Base |
|
14 imports BNF_Composition Basic_BNFs |
|
15 begin |
|
16 |
|
17 lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True" |
|
18 by default simp_all |
|
19 |
|
20 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" |
|
21 by default simp_all |
|
22 |
|
23 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
|
24 by auto |
|
25 |
|
26 lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y" |
|
27 by auto |
|
28 |
|
29 lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
|
30 by blast |
|
31 |
|
32 lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f" |
|
33 by (cases u) (hypsubst, rule unit.case) |
|
34 |
|
35 lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p" |
|
36 by simp |
|
37 |
|
38 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
|
39 by simp |
|
40 |
|
41 lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x" |
|
42 unfolding comp_def fun_eq_iff by simp |
|
43 |
|
44 lemma o_bij: |
|
45 assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id" |
|
46 shows "bij f" |
|
47 unfolding bij_def inj_on_def surj_def proof safe |
|
48 fix a1 a2 assume "f a1 = f a2" |
|
49 hence "g ( f a1) = g (f a2)" by simp |
|
50 thus "a1 = a2" using gf unfolding fun_eq_iff by simp |
|
51 next |
|
52 fix b |
|
53 have "b = f (g b)" |
|
54 using fg unfolding fun_eq_iff by simp |
|
55 thus "EX a. b = f a" by blast |
|
56 qed |
|
57 |
|
58 lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp |
|
59 |
|
60 lemma case_sum_step: |
|
61 "case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p" |
|
62 "case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p" |
|
63 by auto |
|
64 |
|
65 lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P" |
|
66 by blast |
|
67 |
|
68 lemma type_copy_obj_one_point_absE: |
|
69 assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P |
|
70 using type_definition.Rep_inverse[OF assms(1)] |
|
71 by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp |
|
72 |
|
73 lemma obj_sumE_f: |
|
74 assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P" |
|
75 shows "\<forall>x. s = f x \<longrightarrow> P" |
|
76 proof |
|
77 fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto |
|
78 qed |
|
79 |
|
80 lemma case_sum_if: |
|
81 "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)" |
|
82 by simp |
|
83 |
|
84 lemma prod_set_simps: |
|
85 "fsts (x, y) = {x}" |
|
86 "snds (x, y) = {y}" |
|
87 unfolding fsts_def snds_def by simp+ |
|
88 |
|
89 lemma sum_set_simps: |
|
90 "setl (Inl x) = {x}" |
|
91 "setl (Inr x) = {}" |
|
92 "setr (Inl x) = {}" |
|
93 "setr (Inr x) = {x}" |
|
94 unfolding sum_set_defs by simp+ |
|
95 |
|
96 lemma Inl_Inr_False: "(Inl x = Inr y) = False" |
|
97 by simp |
|
98 |
|
99 lemma Inr_Inl_False: "(Inr x = Inl y) = False" |
|
100 by simp |
|
101 |
|
102 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" |
|
103 by blast |
|
104 |
|
105 lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r" |
|
106 unfolding comp_def fun_eq_iff by auto |
|
107 |
|
108 lemma rewriteR_comp_comp2: "\<lbrakk>g \<circ> h = r1 \<circ> r2; f \<circ> r1 = l\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = l \<circ> r2" |
|
109 unfolding comp_def fun_eq_iff by auto |
|
110 |
|
111 lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h" |
|
112 unfolding comp_def fun_eq_iff by auto |
|
113 |
|
114 lemma rewriteL_comp_comp2: "\<lbrakk>f \<circ> g = l1 \<circ> l2; l2 \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l1 \<circ> r" |
|
115 unfolding comp_def fun_eq_iff by auto |
|
116 |
|
117 lemma convol_o: "\<langle>f, g\<rangle> \<circ> h = \<langle>f \<circ> h, g \<circ> h\<rangle>" |
|
118 unfolding convol_def by auto |
|
119 |
|
120 lemma map_prod_o_convol: "map_prod h1 h2 \<circ> \<langle>f, g\<rangle> = \<langle>h1 \<circ> f, h2 \<circ> g\<rangle>" |
|
121 unfolding convol_def by auto |
|
122 |
|
123 lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x" |
|
124 unfolding map_prod_o_convol id_comp comp_id .. |
|
125 |
|
126 lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)" |
|
127 unfolding comp_def by (auto split: sum.splits) |
|
128 |
|
129 lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)" |
|
130 unfolding comp_def by (auto split: sum.splits) |
|
131 |
|
132 lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x" |
|
133 unfolding case_sum_o_map_sum id_comp comp_id .. |
|
134 |
|
135 lemma rel_fun_def_butlast: |
|
136 "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))" |
|
137 unfolding rel_fun_def .. |
|
138 |
|
139 lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)" |
|
140 by auto |
|
141 |
|
142 lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)" |
|
143 by auto |
|
144 |
|
145 lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)" |
|
146 unfolding Grp_def id_apply by blast |
|
147 |
|
148 lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv> |
|
149 (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)" |
|
150 unfolding Grp_def by rule auto |
|
151 |
|
152 lemma vimage2p_mono: "vimage2p f g R x y \<Longrightarrow> R \<le> S \<Longrightarrow> vimage2p f g S x y" |
|
153 unfolding vimage2p_def by blast |
|
154 |
|
155 lemma vimage2p_refl: "(\<And>x. R x x) \<Longrightarrow> vimage2p f f R x x" |
|
156 unfolding vimage2p_def by auto |
|
157 |
|
158 lemma |
|
159 assumes "type_definition Rep Abs UNIV" |
|
160 shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id" |
|
161 unfolding fun_eq_iff comp_apply id_apply |
|
162 type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all |
|
163 |
|
164 lemma type_copy_map_comp0_undo: |
|
165 assumes "type_definition Rep Abs UNIV" |
|
166 "type_definition Rep' Abs' UNIV" |
|
167 "type_definition Rep'' Abs'' UNIV" |
|
168 shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M" |
|
169 by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I] |
|
170 type_definition.Abs_inverse[OF assms(1) UNIV_I] |
|
171 type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x]) |
|
172 |
|
173 lemma vimage2p_id: "vimage2p id id R = R" |
|
174 unfolding vimage2p_def by auto |
|
175 |
|
176 lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1" |
|
177 unfolding fun_eq_iff vimage2p_def o_apply by simp |
|
178 |
|
179 lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g" |
|
180 by (erule arg_cong) |
|
181 |
|
182 lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X" |
|
183 unfolding inj_on_def by simp |
|
184 |
|
185 lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x" |
|
186 by (case_tac x) simp |
|
187 |
|
188 lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x" |
|
189 by (case_tac x) simp+ |
|
190 |
|
191 lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x" |
|
192 by (case_tac x) simp+ |
|
193 |
|
194 lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)" |
|
195 by (simp add: inj_on_def) |
|
196 |
|
197 lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)" |
|
198 by simp |
|
199 |
|
200 ML_file "Tools/BNF/bnf_fp_util.ML" |
|
201 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" |
|
202 ML_file "Tools/BNF/bnf_lfp_size.ML" |
|
203 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
|
204 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
|
205 ML_file "Tools/BNF/bnf_fp_n2m.ML" |
|
206 ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML" |
|
207 |
|
208 ML_file "Tools/Function/old_size.ML" |
|
209 setup Old_Size.setup |
|
210 |
|
211 lemma size_bool[code]: "size (b\<Colon>bool) = 0" |
|
212 by (cases b) auto |
|
213 |
|
214 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" |
|
215 by (induct n) simp_all |
|
216 |
|
217 declare prod.size[no_atp] |
|
218 |
|
219 lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)" |
|
220 by (rule ext) (case_tac x, auto) |
|
221 |
|
222 lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)" |
|
223 by (rule ext) auto |
|
224 |
|
225 setup {* |
|
226 BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} |
|
227 @{thms size_sum_o_map} |
|
228 #> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} |
|
229 @{thms size_prod_o_map} |
|
230 *} |
|
231 |
|
232 end |