author | blanchet |
Tue, 16 Sep 2014 19:23:37 +0200 | |
changeset 58352 | 37745650a3f4 |
child 58353 | c9f374b64d99 |
permissions | -rw-r--r-- |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Basic_BNF_Least_Fixpoints.thy |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
3 |
Copyright 2014 |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
4 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
5 |
Registration of basic types as BNF least fixpoints (datatypes). |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
6 |
*) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
7 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
8 |
theory Basic_BNF_Least_Fixpoints |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
9 |
imports BNF_Least_Fixpoint |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
10 |
begin |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
11 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
12 |
subsection {* Size setup (TODO: Merge with rest of file) *} |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
13 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
14 |
lemma size_bool[code]: "size (b\<Colon>bool) = 0" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
15 |
by (cases b) auto |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
16 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
17 |
lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
18 |
by (induct n) simp_all |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
19 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
20 |
declare prod.size[no_atp] |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
21 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
22 |
lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
23 |
by (rule ext) (case_tac x, auto) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
24 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
25 |
lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
26 |
by (rule ext) auto |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
27 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
28 |
setup {* |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
29 |
BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
30 |
@{thms size_sum_o_map} |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
31 |
#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
32 |
@{thms size_prod_o_map} |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
33 |
*} |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
34 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
35 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
36 |
subsection {* FP sugar setup *} |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
37 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
38 |
definition xtor :: "'a \<Rightarrow> 'a" where |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
39 |
"xtor x = x" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
40 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
41 |
lemma xtor_map: "f (xtor x) = xtor (f x)" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
42 |
unfolding xtor_def by (rule refl) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
43 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
44 |
lemma xtor_set: "f (xtor x) = f x" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
45 |
unfolding xtor_def by (rule refl) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
46 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
47 |
lemma xtor_rel: "R (xtor x) (xtor y) = R x y" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
48 |
unfolding xtor_def by (rule refl) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
49 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
50 |
lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
51 |
unfolding xtor_def by assumption |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
52 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
53 |
lemma xtor_xtor: "xtor (xtor x) = x" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
54 |
unfolding xtor_def by (rule refl) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
55 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
56 |
lemmas xtor_inject = xtor_rel[of "op ="] |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
57 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
58 |
definition ctor_rec :: "'a \<Rightarrow> 'a" where |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
59 |
"ctor_rec x = x" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
60 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
61 |
lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf) x)" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
62 |
unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
63 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
64 |
lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf))" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
65 |
unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
66 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
67 |
lemma xtor_rel_induct: "(\<And>x y. vimage2p BNF_Composition.id_bnf BNF_Composition.id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
68 |
unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
69 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
70 |
lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inl a)))" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
71 |
unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
72 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
73 |
lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inr a)))" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
74 |
unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
75 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
76 |
lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (BNF_Composition.id_bnf (a, b)))" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
77 |
unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
78 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
79 |
ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
80 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
81 |
end |