author | blanchet |
Tue, 10 Jun 2014 12:16:22 +0200 | |
changeset 57200 | aab87ffa60cc |
parent 57123 | b5324647e0f1 |
child 57206 | d9be905d6283 |
permissions | -rw-r--r-- |
55075 | 1 |
(* Title: HOL/BNF_Examples/ListF.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
Finite lists. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
header {* Finite Lists *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
theory ListF |
55076 | 12 |
imports Main |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
|
53355 | 15 |
datatype_new 'a listF (map: mapF rel: relF) = |
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57123
diff
changeset
|
16 |
NilF |
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57123
diff
changeset
|
17 |
| Conss (hdF: 'a) (tlF: "'a listF") |
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57123
diff
changeset
|
18 |
where |
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57123
diff
changeset
|
19 |
"tlF NilF = NilF" |
57123
b5324647e0f1
tuned whitespace, to make datatype definitions slightly less intimidating
blanchet
parents:
55531
diff
changeset
|
20 |
|
55531
601ca8efa000
renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents:
55530
diff
changeset
|
21 |
datatype_compat listF |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
definition Singll ("[[_]]") where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
[simp]: "Singll a \<equiv> Conss a NilF" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55076
diff
changeset
|
26 |
primrec appendd (infixr "@@" 65) where |
53353 | 27 |
"NilF @@ ys = ys" |
28 |
| "Conss x xs @@ ys = Conss x (xs @@ ys)" |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55076
diff
changeset
|
30 |
primrec lrev where |
53353 | 31 |
"lrev NilF = NilF" |
32 |
| "lrev (Conss y ys) = lrev ys @@ [[y]]" |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
lemma appendd_NilF[simp]: "xs @@ NilF = xs" |
53353 | 35 |
by (induct xs) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
lemma appendd_assoc[simp]: "(xs @@ ys) @@ zs = xs @@ ys @@ zs" |
53353 | 38 |
by (induct xs) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
lemma lrev_appendd[simp]: "lrev (xs @@ ys) = lrev ys @@ lrev xs" |
53353 | 41 |
by (induct xs) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
lemma listF_map_appendd[simp]: |
53353 | 44 |
"mapF f (xs @@ ys) = mapF f xs @@ mapF f ys" |
45 |
by (induct xs) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
|
53353 | 47 |
lemma lrev_listF_map[simp]: "lrev (mapF f xs) = mapF f (lrev xs)" |
48 |
by (induct xs) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
|
53353 | 50 |
lemma lrev_lrev[simp]: "lrev (lrev xs) = xs" |
51 |
by (induct xs) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55076
diff
changeset
|
53 |
primrec lengthh where |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
"lengthh NilF = 0" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
| "lengthh (Conss x xs) = Suc (lengthh xs)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
fun nthh where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
58 |
"nthh (Conss x xs) 0 = x" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
| "nthh (Conss x xs) (Suc n) = nthh xs n" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
| "nthh xs i = undefined" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
|
53353 | 62 |
lemma lengthh_listF_map[simp]: "lengthh (mapF f xs) = lengthh xs" |
63 |
by (induct xs) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
lemma nthh_listF_map[simp]: |
53353 | 66 |
"i < lengthh xs \<Longrightarrow> nthh (mapF f xs) i = f (nthh xs i)" |
67 |
by (induct rule: nthh.induct) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
|
54490
930409d43211
use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package
blanchet
parents:
53355
diff
changeset
|
69 |
lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> set_listF xs" |
53353 | 70 |
by (induct rule: nthh.induct) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
lemma NilF_iff[iff]: "(lengthh xs = 0) = (xs = NilF)" |
53353 | 73 |
by (induct xs) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
lemma Conss_iff[iff]: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
"(lengthh xs = Suc n) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)" |
53353 | 77 |
by (induct xs) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
lemma Conss_iff'[iff]: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
"(Suc n = lengthh xs) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)" |
53353 | 81 |
by (induct xs) (simp, simp, blast) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
|
53353 | 83 |
lemma listF_induct2[consumes 1, case_names NilF Conss]: "\<lbrakk>lengthh xs = lengthh ys; P NilF NilF; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
\<And>x xs y ys. P xs ys \<Longrightarrow> P (Conss x xs) (Conss y ys)\<rbrakk> \<Longrightarrow> P xs ys" |
53353 | 85 |
by (induct xs arbitrary: ys) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
fun zipp where |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
"zipp NilF NilF = NilF" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
| "zipp (Conss x xs) (Conss y ys) = Conss (x, y) (zipp xs ys)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
| "zipp xs ys = undefined" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
92 |
lemma listF_map_fst_zip[simp]: |
53353 | 93 |
"lengthh xs = lengthh ys \<Longrightarrow> mapF fst (zipp xs ys) = xs" |
94 |
by (induct rule: listF_induct2) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
lemma listF_map_snd_zip[simp]: |
53353 | 97 |
"lengthh xs = lengthh ys \<Longrightarrow> mapF snd (zipp xs ys) = ys" |
98 |
by (induct rule: listF_induct2) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
100 |
lemma lengthh_zip[simp]: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
101 |
"lengthh xs = lengthh ys \<Longrightarrow> lengthh (zipp xs ys) = lengthh xs" |
53353 | 102 |
by (induct rule: listF_induct2) auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
lemma nthh_zip[simp]: |
53353 | 105 |
assumes "lengthh xs = lengthh ys" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
shows "i < lengthh xs \<Longrightarrow> nthh (zipp xs ys) i = (nthh xs i, nthh ys i)" |
53353 | 107 |
using assms proof (induct arbitrary: i rule: listF_induct2) |
108 |
case (Conss x xs y ys) thus ?case by (induct i) auto |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
qed simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
lemma list_set_nthh[simp]: |
54490
930409d43211
use suffix '_list' etc. instead of prefix 'list_' for constants not present in the old package
blanchet
parents:
53355
diff
changeset
|
112 |
"(x \<in> set_listF xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)" |
53353 | 113 |
by (induct xs) (auto, induct rule: nthh.induct, auto) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
115 |
end |