184 unfolding rel_fun_def by simp |
184 unfolding rel_fun_def by simp |
185 |
185 |
186 lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R" |
186 lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R" |
187 by (rule ssubst) |
187 by (rule ssubst) |
188 |
188 |
189 lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g" |
|
190 by (erule arg_cong) |
|
191 |
|
192 lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g" |
|
193 by (rule ext) simp |
|
194 |
|
195 lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X" |
|
196 unfolding inj_on_def by simp |
|
197 |
|
198 lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x" |
|
199 by (case_tac x) simp |
|
200 |
|
201 lemma case_sum_o_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x" |
|
202 by (case_tac x) simp+ |
|
203 |
|
204 lemma case_prod_o_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x" |
|
205 by (case_tac x) simp+ |
|
206 |
|
207 lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)" |
|
208 by (simp add: inj_on_def) |
|
209 |
|
210 ML_file "Tools/BNF/bnf_lfp_util.ML" |
189 ML_file "Tools/BNF/bnf_lfp_util.ML" |
211 ML_file "Tools/BNF/bnf_lfp_tactics.ML" |
190 ML_file "Tools/BNF/bnf_lfp_tactics.ML" |
212 ML_file "Tools/BNF/bnf_lfp.ML" |
191 ML_file "Tools/BNF/bnf_lfp.ML" |
213 ML_file "Tools/BNF/bnf_lfp_compat.ML" |
192 ML_file "Tools/BNF/bnf_lfp_compat.ML" |
214 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" |
193 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" |
215 |
194 |
216 |
|
217 subsection {* Size of a datatype value *} |
|
218 |
|
219 ML_file "Tools/BNF/bnf_lfp_size.ML" |
|
220 ML_file "Tools/Function/size.ML" |
|
221 setup Size.setup |
|
222 |
|
223 lemma size_bool[code]: "size (b\<Colon>bool) = 0" |
|
224 by (cases b) auto |
|
225 |
|
226 lemma nat_size[simp, code]: "size (n\<Colon>nat) = n" |
|
227 by (induct n) simp_all |
|
228 |
|
229 declare prod.size[no_atp] |
|
230 |
|
231 lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)" |
|
232 by (rule ext) (case_tac x, auto) |
|
233 |
|
234 lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)" |
|
235 by (rule ext) auto |
|
236 |
|
237 setup {* |
|
238 BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size} |
|
239 @{thms sum_size_o_map} |
|
240 #> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size} |
|
241 @{thms prod_size_o_map} |
|
242 *} |
|
243 |
|
244 hide_fact (open) id_transfer |
195 hide_fact (open) id_transfer |
245 |
196 |
|
197 datatype_new 'a x = X 'a |
|
198 |
246 end |
199 end |