summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

6 Finite lists.

7 *)

9 header {* Finite Lists *}

11 theory ListF

12 imports Main

13 begin

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

19 definition Singll ("[[_]]") where

20 [simp]: "Singll a \<equiv> Conss a NilF"

22 primrec_new appendd (infixr "@@" 65) where

23 "NilF @@ ys = ys"

24 | "Conss x xs @@ ys = Conss x (xs @@ ys)"

26 primrec_new lrev where

27 "lrev NilF = NilF"

28 | "lrev (Conss y ys) = lrev ys @@ [[y]]"

30 lemma appendd_NilF[simp]: "xs @@ NilF = xs"

31 by (induct xs) auto

33 lemma appendd_assoc[simp]: "(xs @@ ys) @@ zs = xs @@ ys @@ zs"

34 by (induct xs) auto

36 lemma lrev_appendd[simp]: "lrev (xs @@ ys) = lrev ys @@ lrev xs"

37 by (induct xs) auto

39 lemma listF_map_appendd[simp]:

40 "mapF f (xs @@ ys) = mapF f xs @@ mapF f ys"

41 by (induct xs) auto

43 lemma lrev_listF_map[simp]: "lrev (mapF f xs) = mapF f (lrev xs)"

44 by (induct xs) auto

46 lemma lrev_lrev[simp]: "lrev (lrev xs) = xs"

47 by (induct xs) auto

49 primrec_new lengthh where

50 "lengthh NilF = 0"

51 | "lengthh (Conss x xs) = Suc (lengthh xs)"

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"

58 lemma lengthh_listF_map[simp]: "lengthh (mapF f xs) = lengthh xs"

59 by (induct xs) auto

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

65 lemma nthh_listF_set[simp]: "i < lengthh xs \<Longrightarrow> nthh xs i \<in> set_listF xs"

66 by (induct rule: nthh.induct) auto

68 lemma NilF_iff[iff]: "(lengthh xs = 0) = (xs = NilF)"

69 by (induct xs) auto

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

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)

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

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"

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

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

96 lemma lengthh_zip[simp]:

97 "lengthh xs = lengthh ys \<Longrightarrow> lengthh (zipp xs ys) = lengthh xs"

98 by (induct rule: listF_induct2) auto

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

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)

111 end