|
1 (* Title: HOL/Basic_BNF_LFPs.thy |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2014 |
|
4 |
|
5 Registration of basic types as BNF least fixpoints (datatypes). |
|
6 *) |
|
7 |
|
8 theory Basic_BNF_LFPs |
|
9 imports BNF_Least_Fixpoint |
|
10 begin |
|
11 |
|
12 definition xtor :: "'a \<Rightarrow> 'a" where |
|
13 "xtor x = x" |
|
14 |
|
15 lemma xtor_map: "f (xtor x) = xtor (f x)" |
|
16 unfolding xtor_def by (rule refl) |
|
17 |
|
18 lemma xtor_set: "f (xtor x) = f x" |
|
19 unfolding xtor_def by (rule refl) |
|
20 |
|
21 lemma xtor_rel: "R (xtor x) (xtor y) = R x y" |
|
22 unfolding xtor_def by (rule refl) |
|
23 |
|
24 lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z" |
|
25 unfolding xtor_def by assumption |
|
26 |
|
27 lemma xtor_xtor: "xtor (xtor x) = x" |
|
28 unfolding xtor_def by (rule refl) |
|
29 |
|
30 lemmas xtor_inject = xtor_rel[of "op ="] |
|
31 |
|
32 lemma xtor_rel_induct: "(\<And>x y. vimage2p id_bnf id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR" |
|
33 unfolding xtor_def vimage2p_def id_bnf_def by default |
|
34 |
|
35 lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))" |
|
36 unfolding xtor_def id_bnf_def by (rule reflexive) |
|
37 |
|
38 lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))" |
|
39 unfolding xtor_def id_bnf_def by (rule reflexive) |
|
40 |
|
41 lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))" |
|
42 unfolding xtor_def id_bnf_def by (rule reflexive) |
|
43 |
|
44 definition ctor_rec :: "'a \<Rightarrow> 'a" where |
|
45 "ctor_rec x = x" |
|
46 |
|
47 lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)" |
|
48 unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl) |
|
49 |
|
50 lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)" |
|
51 unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) |
|
52 |
|
53 lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))" |
|
54 unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) |
|
55 |
|
56 lemma eq_fst_iff: "a = fst p \<longleftrightarrow> (\<exists>b. p = (a, b))" |
|
57 by (cases p) auto |
|
58 |
|
59 lemma eq_snd_iff: "b = snd p \<longleftrightarrow> (\<exists>a. p = (a, b))" |
|
60 by (cases p) auto |
|
61 |
|
62 lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)" |
|
63 by default blast+ |
|
64 |
|
65 lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)" |
|
66 by default blast+ |
|
67 |
|
68 lemma isl_map_sum: |
|
69 "isl (map_sum f g s) = isl s" |
|
70 by (cases s) simp_all |
|
71 |
|
72 lemma map_sum_sel: |
|
73 "isl s \<Longrightarrow> projl (map_sum f g s) = f (projl s)" |
|
74 "\<not> isl s \<Longrightarrow> projr (map_sum f g s) = g (projr s)" |
|
75 by (case_tac [!] s) simp_all |
|
76 |
|
77 lemma set_sum_sel: |
|
78 "isl s \<Longrightarrow> projl s \<in> setl s" |
|
79 "\<not> isl s \<Longrightarrow> projr s \<in> setr s" |
|
80 by (case_tac [!] s) (auto intro: setl.intros setr.intros) |
|
81 |
|
82 lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b \<and> |
|
83 (isl a \<longrightarrow> isl b \<longrightarrow> R1 (projl a) (projl b)) \<and> |
|
84 (\<not> isl a \<longrightarrow> \<not> isl b \<longrightarrow> R2 (projr a) (projr b)))" |
|
85 by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all |
|
86 |
|
87 lemma isl_transfer: "rel_fun (rel_sum A B) (op =) isl isl" |
|
88 unfolding rel_fun_def rel_sum_sel by simp |
|
89 |
|
90 lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) \<and> R2 (snd p) (snd q))" |
|
91 by (force simp: rel_prod.simps elim: rel_prod.cases) |
|
92 |
|
93 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML" |
|
94 |
|
95 ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" |
|
96 |
|
97 lemma size_bool[code]: "size (b\<Colon>bool) = 0" |
|
98 by (cases b) auto |
|
99 |
|
100 declare prod.size[no_atp] |
|
101 |
|
102 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" |
|
103 by (induct n) simp_all |
|
104 |
|
105 hide_const (open) xtor ctor_rec |
|
106 |
|
107 hide_fact (open) |
|
108 xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec |
|
109 ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt |
|
110 |
|
111 end |