src/HOL/BNF_Examples/ListF.thy
 author blanchet Mon Jan 20 18:24:56 2014 +0100 (2014-01-20) changeset 55076 1e73e090a514 parent 55075 b3d0a02a756d child 55530 3dfb724db099 permissions -rw-r--r--
compile
```     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 Main
```
```    13 begin
```
```    14
```
```    15 datatype_new 'a listF (map: mapF rel: relF) =
```
```    16   NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
```
```    17 datatype_new_compat listF
```
```    18
```
```    19 definition Singll ("[[_]]") where
```
```    20   [simp]: "Singll a \<equiv> Conss a NilF"
```
```    21
```
```    22 primrec_new appendd (infixr "@@" 65) where
```
```    23   "NilF @@ ys = ys"
```
```    24 | "Conss x xs @@ ys = Conss x (xs @@ ys)"
```
```    25
```
```    26 primrec_new lrev where
```
```    27   "lrev NilF = NilF"
```
```    28 | "lrev (Conss y ys) = lrev ys @@ [[y]]"
```
```    29
```
```    30 lemma appendd_NilF[simp]: "xs @@ NilF = xs"
```
```    31   by (induct xs) auto
```
```    32
```
```    33 lemma appendd_assoc[simp]: "(xs @@ ys) @@ zs = xs @@ ys @@ zs"
```
```    34   by (induct xs) auto
```
```    35
```
```    36 lemma lrev_appendd[simp]: "lrev (xs @@ ys) = lrev ys @@ lrev xs"
```
```    37   by (induct xs) auto
```
```    38
```
```    39 lemma listF_map_appendd[simp]:
```
```    40   "mapF f (xs @@ ys) = mapF f xs @@ mapF f ys"
```
```    41   by (induct xs) auto
```
```    42
```
```    43 lemma lrev_listF_map[simp]: "lrev (mapF f xs) = mapF f (lrev xs)"
```
```    44   by (induct xs) auto
```
```    45
```
```    46 lemma lrev_lrev[simp]: "lrev (lrev xs) = xs"
```
```    47   by (induct xs) auto
```
```    48
```
```    49 primrec_new lengthh where
```
```    50   "lengthh NilF = 0"
```
```    51 | "lengthh (Conss x xs) = Suc (lengthh xs)"
```
```    52
```
```    53 fun nthh where
```
```    54   "nthh (Conss x xs) 0 = x"
```
```    55 | "nthh (Conss x xs) (Suc n) = nthh xs n"
```
```    56 | "nthh xs i = undefined"
```
```    57
```
```    58 lemma lengthh_listF_map[simp]: "lengthh (mapF f xs) = lengthh xs"
```
```    59   by (induct xs) auto
```
```    60
```
```    61 lemma nthh_listF_map[simp]:
```
```    62   "i < lengthh xs \<Longrightarrow> nthh (mapF f xs) i = f (nthh xs i)"
```
```    63   by (induct rule: nthh.induct) auto
```
```    64
```
```    65 lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> set_listF xs"
```
```    66   by (induct rule: nthh.induct) auto
```
```    67
```
```    68 lemma NilF_iff[iff]: "(lengthh xs = 0) = (xs = NilF)"
```
```    69   by (induct xs) auto
```
```    70
```
```    71 lemma Conss_iff[iff]:
```
```    72   "(lengthh xs = Suc n) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)"
```
```    73   by (induct xs) auto
```
```    74
```
```    75 lemma Conss_iff'[iff]:
```
```    76   "(Suc n = lengthh xs) = (\<exists>y ys. xs = Conss y ys \<and> lengthh ys = n)"
```
```    77   by (induct xs) (simp, simp, blast)
```
```    78
```
```    79 lemma listF_induct2[consumes 1, case_names NilF Conss]: "\<lbrakk>lengthh xs = lengthh ys; P NilF NilF;
```
```    80     \<And>x xs y ys. P xs ys \<Longrightarrow> P (Conss x xs) (Conss y ys)\<rbrakk> \<Longrightarrow> P xs ys"
```
```    81     by (induct xs arbitrary: ys) auto
```
```    82
```
```    83 fun zipp where
```
```    84   "zipp NilF NilF = NilF"
```
```    85 | "zipp (Conss x xs) (Conss y ys) = Conss (x, y) (zipp xs ys)"
```
```    86 | "zipp xs ys = undefined"
```
```    87
```
```    88 lemma listF_map_fst_zip[simp]:
```
```    89   "lengthh xs = lengthh ys \<Longrightarrow> mapF fst (zipp xs ys) = xs"
```
```    90   by (induct rule: listF_induct2) auto
```
```    91
```
```    92 lemma listF_map_snd_zip[simp]:
```
```    93   "lengthh xs = lengthh ys \<Longrightarrow> mapF snd (zipp xs ys) = ys"
```
```    94   by (induct rule: listF_induct2) auto
```
```    95
```
```    96 lemma lengthh_zip[simp]:
```
```    97   "lengthh xs = lengthh ys \<Longrightarrow> lengthh (zipp xs ys) = lengthh xs"
```
```    98   by (induct rule: listF_induct2) auto
```
```    99
```
```   100 lemma nthh_zip[simp]:
```
```   101   assumes "lengthh xs = lengthh ys"
```
```   102   shows "i < lengthh xs \<Longrightarrow> nthh (zipp xs ys) i = (nthh xs i, nthh ys i)"
```
```   103 using assms proof (induct arbitrary: i rule: listF_induct2)
```
```   104   case (Conss x xs y ys) thus ?case by (induct i) auto
```
```   105 qed simp
```
```   106
```
```   107 lemma list_set_nthh[simp]:
```
```   108   "(x \<in> set_listF xs) \<Longrightarrow> (\<exists>i < lengthh xs. nthh xs i = x)"
```
```   109   by (induct xs) (auto, induct rule: nthh.induct, auto)
```
```   110
```
```   111 end
```