1 (* Title: HOL/BNF/Examples/ListF.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Finite lists. |
|
7 *) |
|
8 |
|
9 header {* Finite Lists *} |
|
10 |
|
11 theory ListF |
|
12 imports "../BNF" |
|
13 begin |
|
14 |
|
15 data_raw listF: 'list = "unit + 'a \<times> 'list" |
|
16 |
|
17 definition "NilF = listF_ctor (Inl ())" |
|
18 definition "Conss a as \<equiv> listF_ctor (Inr (a, as))" |
|
19 |
|
20 lemma listF_map_NilF[simp]: "listF_map f NilF = NilF" |
|
21 unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_folds by simp |
|
22 |
|
23 lemma listF_map_Conss[simp]: |
|
24 "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)" |
|
25 unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_folds by simp |
|
26 |
|
27 lemma listF_set_NilF[simp]: "listF_set NilF = {}" |
|
28 unfolding listF_set_def NilF_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def |
|
29 sum_set_defs pre_listF_map_def collect_def[abs_def] by simp |
|
30 |
|
31 lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \<union> listF_set xs" |
|
32 unfolding listF_set_def Conss_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def |
|
33 sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_def] by simp |
|
34 |
|
35 lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" |
|
36 unfolding NilF_def listF.ctor_folds pre_listF_map_def by simp |
|
37 |
|
38 |
|
39 lemma fold_sum_case_Conss: |
|
40 "listF_ctor_fold (sum_case f g) (Conss y ys) = g (y, listF_ctor_fold (sum_case f g) ys)" |
|
41 unfolding Conss_def listF.ctor_folds pre_listF_map_def by simp |
|
42 |
|
43 (* familiar induction principle *) |
|
44 lemma listF_induct: |
|
45 fixes xs :: "'a listF" |
|
46 assumes IB: "P NilF" and IH: "\<And>x xs. P xs \<Longrightarrow> P (Conss x xs)" |
|
47 shows "P xs" |
|
48 proof (rule listF.ctor_induct) |
|
49 fix xs :: "unit + 'a \<times> 'a listF" |
|
50 assume raw_IH: "\<And>a. a \<in> pre_listF_set2 xs \<Longrightarrow> P a" |
|
51 show "P (listF_ctor xs)" |
|
52 proof (cases xs) |
|
53 case (Inl a) with IB show ?thesis unfolding NilF_def by simp |
|
54 next |
|
55 case (Inr b) |
|
56 then obtain y ys where yys: "listF_ctor xs = Conss y ys" |
|
57 unfolding Conss_def listF.ctor_inject by (blast intro: prod.exhaust) |
|
58 hence "ys \<in> pre_listF_set2 xs" |
|
59 unfolding pre_listF_set2_def Conss_def listF.ctor_inject sum_set_defs prod_set_defs |
|
60 collect_def[abs_def] by simp |
|
61 with raw_IH have "P ys" by blast |
|
62 with IH have "P (Conss y ys)" by blast |
|
63 with yys show ?thesis by simp |
|
64 qed |
|
65 qed |
|
66 |
|
67 rep_datatype NilF Conss |
|
68 by (blast intro: listF_induct) (auto simp add: NilF_def Conss_def listF.ctor_inject) |
|
69 |
|
70 definition Singll ("[[_]]") where |
|
71 [simp]: "Singll a \<equiv> Conss a NilF" |
|
72 |
|
73 definition appendd (infixr "@@" 65) where |
|
74 "appendd \<equiv> listF_ctor_fold (sum_case (\<lambda> _. id) (\<lambda> (a,f) bs. Conss a (f bs)))" |
|
75 |
|
76 definition "lrev \<equiv> listF_ctor_fold (sum_case (\<lambda> _. NilF) (\<lambda> (b,bs). bs @@ [[b]]))" |
|
77 |
|
78 lemma lrev_NilF[simp]: "lrev NilF = NilF" |
|
79 unfolding lrev_def by (simp add: fold_sum_case_NilF) |
|
80 |
|
81 lemma lrev_Conss[simp]: "lrev (Conss y ys) = lrev ys @@ [[y]]" |
|
82 unfolding lrev_def by (simp add: fold_sum_case_Conss) |
|
83 |
|
84 lemma NilF_appendd[simp]: "NilF @@ ys = ys" |
|
85 unfolding appendd_def by (simp add: fold_sum_case_NilF) |
|
86 |
|
87 lemma Conss_append[simp]: "Conss x xs @@ ys = Conss x (xs @@ ys)" |
|
88 unfolding appendd_def by (simp add: fold_sum_case_Conss) |
|
89 |
|
90 lemma appendd_NilF[simp]: "xs @@ NilF = xs" |
|
91 by (rule listF_induct) auto |
|
92 |
|
93 lemma appendd_assoc[simp]: "(xs @@ ys) @@ zs = xs @@ ys @@ zs" |
|
94 by (rule listF_induct) auto |
|
95 |
|
96 lemma lrev_appendd[simp]: "lrev (xs @@ ys) = lrev ys @@ lrev xs" |
|
97 by (rule listF_induct[of _ xs]) auto |
|
98 |
|
99 lemma listF_map_appendd[simp]: |
|
100 "listF_map f (xs @@ ys) = listF_map f xs @@ listF_map f ys" |
|
101 by (rule listF_induct[of _ xs]) auto |
|
102 |
|
103 lemma lrev_listF_map[simp]: "lrev (listF_map f xs) = listF_map f (lrev xs)" |
|
104 by (rule listF_induct[of _ xs]) auto |
|
105 |
|
106 lemma lrev_lrev[simp]: "lrev (lrev as) = as" |
|
107 by (rule listF_induct) auto |
|
108 |
|
109 fun lengthh where |
|
110 "lengthh NilF = 0" |
|
111 | "lengthh (Conss x xs) = Suc (lengthh xs)" |
|
112 |
|
113 fun nthh where |
|
114 "nthh (Conss x xs) 0 = x" |
|
115 | "nthh (Conss x xs) (Suc n) = nthh xs n" |
|
116 | "nthh xs i = undefined" |
|
117 |
|
118 lemma lengthh_listF_map[simp]: "lengthh (listF_map f xs) = lengthh xs" |
|
119 by (rule listF_induct[of _ xs]) auto |
|
120 |
|
121 lemma nthh_listF_map[simp]: |
|
122 "i < lengthh xs \<Longrightarrow> nthh (listF_map f xs) i = f (nthh xs i)" |
|
123 by (induct rule: nthh.induct) auto |
|
124 |
|
125 lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> listF_set xs" |
|
126 by (induct rule: nthh.induct) auto |
|
127 |
|
128 lemma NilF_iff[iff]: "(lengthh xs = 0) = (xs = NilF)" |
|
129 by (induct xs) auto |
|
130 |
|
131 lemma Conss_iff[iff]: |
|
132 "(lengthh xs = Suc n) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)" |
|
133 by (induct xs) auto |
|
134 |
|
135 lemma Conss_iff'[iff]: |
|
136 "(Suc n = lengthh xs) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)" |
|
137 by (induct xs) (simp, simp, blast) |
|
138 |
|
139 lemma listF_induct2: "\<lbrakk>lengthh xs = lengthh ys; P NilF NilF; |
|
140 \<And>x xs y ys. P xs ys \<Longrightarrow> P (Conss x xs) (Conss y ys)\<rbrakk> \<Longrightarrow> P xs ys" |
|
141 by (induct xs arbitrary: ys rule: listF_induct) auto |
|
142 |
|
143 fun zipp where |
|
144 "zipp NilF NilF = NilF" |
|
145 | "zipp (Conss x xs) (Conss y ys) = Conss (x, y) (zipp xs ys)" |
|
146 | "zipp xs ys = undefined" |
|
147 |
|
148 lemma listF_map_fst_zip[simp]: |
|
149 "lengthh xs = lengthh ys \<Longrightarrow> listF_map fst (zipp xs ys) = xs" |
|
150 by (erule listF_induct2) auto |
|
151 |
|
152 lemma listF_map_snd_zip[simp]: |
|
153 "lengthh xs = lengthh ys \<Longrightarrow> listF_map snd (zipp xs ys) = ys" |
|
154 by (erule listF_induct2) auto |
|
155 |
|
156 lemma lengthh_zip[simp]: |
|
157 "lengthh xs = lengthh ys \<Longrightarrow> lengthh (zipp xs ys) = lengthh xs" |
|
158 by (erule listF_induct2) auto |
|
159 |
|
160 lemma nthh_zip[simp]: |
|
161 assumes *: "lengthh xs = lengthh ys" |
|
162 shows "i < lengthh xs \<Longrightarrow> nthh (zipp xs ys) i = (nthh xs i, nthh ys i)" |
|
163 proof (induct arbitrary: i rule: listF_induct2[OF *]) |
|
164 case (2 x xs y ys) thus ?case by (induct i) auto |
|
165 qed simp |
|
166 |
|
167 lemma list_set_nthh[simp]: |
|
168 "(x \<in> listF_set xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)" |
|
169 by (induct xs) (auto, induct rule: nthh.induct, auto) |
|
170 |
|
171 end |
|