doc-src/Exercises/2002/a5/l2.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 13739 f5d0a66c8124
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13739
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     1
theory l2 = Main:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     2
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     3
text {*
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     4
  \section*{Sortieren auf Listen}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     5
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     6
  Der erste Teil des Blattes beschäftigt sich mit einem
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     7
  einfachen Sortieralgorithmus auf Listen von natürlichen Zahlen.
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     8
  Ihre Aufgabe ist es, den Sortieralgorithmus in Isabelle zu
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
     9
  programmieren und zu zeigen, dass Ihre Implementierung korrekt ist.
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    10
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    11
  Der Algorithmus lässt sich in folgende Funktionen zerlegen:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    12
*}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    13
consts 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    14
  insort :: "nat \<Rightarrow> nat list \<Rightarrow> nat list"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    15
  sort   :: "nat list \<Rightarrow> nat list"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    16
  le     :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    17
  sorted :: "nat list \<Rightarrow> bool"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    18
text {*
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    19
  Hierbei soll @{term "insort x xs"} eine Zahl @{term x} in eine
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    20
  sortierte Liste @{text xs} einfügen, und die Funktion @{term "sort ys"}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    21
  (aufbauend auf @{text insort}) die sortierte Version von @{text ys}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    22
  liefern.
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    23
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    24
  Um zu zeigen, dass die resultierende Liste tatsächlich sortiert
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    25
  ist, benötigen sie das Prädikat @{term "sorted xs"}, das überprüft
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    26
  ob jedes Element der Liste kleiner ist als alle folgenden Elemente
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    27
  der Liste. Die Funktion @{term "le n xs"} soll genau dann wahr sein,
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    28
  wenn @{term n} kleiner oder gleich allen Elementen von @{text xs}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    29
  ist. 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    30
*}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    31
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    32
  "le a [] = True"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    33
  "le a (x#xs) = (a <= x & le a xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    34
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    35
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    36
  "sorted [] = True"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    37
  "sorted (x#xs) = (le x xs & sorted xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    38
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    39
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    40
  "insort a [] = [a]"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    41
  "insort a (x#xs) = (if a <= x then a#x#xs else x # insort a xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    42
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    43
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    44
  "sort [] = []"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    45
  "sort (x#xs) = insort x (sort xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    46
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    47
lemma "le 3 [7,10,3]" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    48
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    49
lemma "\<not> le 3 [7,10,2]" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    50
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    51
lemma "sorted [1,2,3,4]" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    52
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    53
lemma "\<not> sorted [3,1,4,2]" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    54
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    55
lemma "sort [3,1,4,2] = [1,2,3,4]" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    56
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    57
text {*
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    58
  Zeigen Sie zu Beginn folgendes Monotonie-Lemma über @{term le}. Die
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    59
  Formulierung des Lemmas ist aus technischen Gründen (über die sie
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    60
  später mehr erfahren werden) etwas ungewohnt:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    61
*} 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    62
lemma [simp]: "x \<le> y \<Longrightarrow> le y xs \<longrightarrow> le x xs"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    63
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    64
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    65
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    66
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    67
lemma [simp]: 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    68
  "le x (insort a xs) = (x <= a & le x xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    69
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    70
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    71
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    72
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    73
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    74
  "sorted (insort a xs) = sorted xs"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    75
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    76
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    77
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    78
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    79
theorem "sorted (sort xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    80
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    81
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    82
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    83
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    84
text  {*
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    85
  Das Theorem sagt zwar aus, dass Ihr Algorithmus eine sortierte
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    86
  Liste zurückgibt, es gibt Ihnen aber nicht die Sicherheit, dass die sortierte
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    87
  Liste auch die gleichen Elemente wie das Original enthält. Formulieren Sie deswegen
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    88
  eine Funktion @{term "count xs x"}, die zählt, wie oft die Zahl
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    89
  @{term x} in @{term xs} vorkommt.  
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    90
*}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    91
consts
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    92
  count :: "nat list => nat => nat"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    93
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    94
  "count [] y = 0"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    95
  "count (x#xs) y = (if x=y then Suc(count xs y) else count xs y)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    96
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    97
lemma "count [2,3,1,3] 3 = 2" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    98
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
    99
lemma "count [2,3,1,3] 7 = 0" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   100
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   101
lemma "count [2,3,1,3] 2 = 1" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   102
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   103
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   104
  "count (insort x xs) y =
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   105
  (if x=y then Suc (count xs y) else count xs y)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   106
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   107
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   108
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   109
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   110
theorem "count (sort xs) x = count xs x"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   111
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   112
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   113
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   114
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   115
text {*
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   116
  \section*{Sortieren mit Bäumen}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   117
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   118
  Der zweite Teil des Blattes beschäftigt sich mit einem
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   119
  Sortieralgorithmus, der Bäume verwendet.
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   120
  Definieren Sie dazu zuerst den Datentyp @{text bintree} der
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   121
  Binärbäume. Für diese Aufgabe sind Binärbäume entweder leer, oder
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   122
  bestehen aus einem
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   123
  Knoten mit einer natürlichen Zahl und zwei Unterbäumen.  
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   124
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   125
  Schreiben Sie dann eine Funktion @{text tsorted}, die feststellt, ob
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   126
  ein Binärbaum geordnet ist. Sie werden dazu zwei Hilfsfunktionen
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   127
  @{text tge} und @{text tle} benötigen, die überprüfen ob eine Zahl
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   128
  grössergleich/kleinergleich als alle Elemente eines Baumes sind.
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   129
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   130
  Formulieren Sie schliesslich eine Funktion @{text tree_of}, die zu einer
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   131
  (unsortierten) Liste den geordneten Binärbaum zurückgibt. Stützen Sie
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   132
  sich dabei auf eine Funktion @{term "ins n b"}, die eine Zahl @{term
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   133
  n} in einen geordneten Binärbaum @{term b} einfügt.  
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   134
*}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   135
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   136
datatype bintree = Empty | Node nat bintree bintree
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   137
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   138
consts
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   139
  tsorted :: "bintree \<Rightarrow> bool"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   140
  tge :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   141
  tle :: "nat \<Rightarrow> bintree \<Rightarrow> bool"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   142
  ins :: "nat \<Rightarrow> bintree \<Rightarrow> bintree"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   143
  tree_of :: "nat list \<Rightarrow> bintree"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   144
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   145
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   146
  "tsorted Empty = True"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   147
  "tsorted (Node n t1 t2) = (tsorted t1 \<and> tsorted t2 \<and> tge n t1 \<and> tle n t2)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   148
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   149
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   150
  "tge x Empty = True"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   151
  "tge x (Node n t1 t2) = (n \<le> x \<and> tge x t1 \<and> tge x t2)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   152
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   153
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   154
  "tle x Empty = True"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   155
  "tle x (Node n t1 t2) = (x \<le> n \<and> tle x t1 \<and> tle x t2)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   156
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   157
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   158
  "ins x Empty = Node x Empty Empty"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   159
  "ins x (Node n t1 t2) = (if x \<le> n then Node n (ins x t1) t2 else Node n t1 (ins x t2))"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   160
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   161
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   162
  "tree_of [] = Empty"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   163
  "tree_of (x#xs) = ins x (tree_of xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   164
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   165
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   166
lemma "tge 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   167
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   168
lemma "\<not> tge 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   169
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   170
lemma "\<not> tle 5 (Node 3 (Node 2 Empty Empty) Empty)" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   171
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   172
lemma "\<not> tle 5 (Node 3 Empty (Node 7 Empty Empty))" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   173
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   174
lemma "tle 3 (Node 3 Empty (Node 7 Empty Empty))" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   175
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   176
lemma "tsorted (Node 3 Empty (Node 7 Empty Empty))" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   177
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   178
lemma "tree_of [3,2] = Node 2 Empty (Node 3 Empty Empty)" by auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   179
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   180
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   181
  "tge a (ins x t) = (x \<le> a \<and> tge a t)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   182
  apply (induct_tac t)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   183
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   184
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   185
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   186
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   187
  "tle a (ins x t) = (a \<le> x \<and> tle a t)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   188
  apply (induct_tac t)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   189
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   190
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   191
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   192
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   193
  "tsorted (ins x t) = tsorted t"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   194
  apply (induct_tac t)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   195
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   196
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   197
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   198
theorem [simp]: "tsorted (tree_of xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   199
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   200
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   201
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   202
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   203
text {* 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   204
  Auch bei diesem Algorithmus müssen wir noch zeigen, dass keine
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   205
  Elemente beim Sortieren verloren gehen (oder erfunden werden). Formulieren
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   206
  Sie analog zu den Listen eine Funktion @{term "tcount x b"}, die zählt, wie
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   207
  oft die Zahl @{term x} im Baum @{term b} vorkommt.
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   208
*} 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   209
consts
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   210
  tcount :: "bintree => nat => nat"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   211
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   212
  "tcount Empty y = 0"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   213
  "tcount (Node x t1 t2) y = 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   214
  (if x=y 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   215
   then Suc (tcount t1 y + tcount t2 y) 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   216
   else tcount t1 y + tcount t2 y)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   217
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   218
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   219
  "tcount (ins x t) y =
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   220
  (if x=y then Suc (tcount t y) else tcount t y)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   221
  apply(induct_tac t)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   222
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   223
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   224
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   225
theorem "tcount (tree_of xs) x = count xs x"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   226
  apply (induct_tac xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   227
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   228
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   229
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   230
text {*
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   231
  Die eigentliche Aufgabe war es, Listen zu sortieren. Bis jetzt haben
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   232
  wir lediglich einen Algorithmus, der Listen in geordnete Bäume
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   233
  transformiert. Definieren Sie deswegen eine Funktion @{text
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   234
  list_of}, die zu einen (geordneten) Baum eine (geordnete) Liste liefert. 
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   235
*}
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   236
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   237
consts
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   238
  ge      :: "nat \<Rightarrow> nat list \<Rightarrow> bool"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   239
  list_of :: "bintree \<Rightarrow> nat list"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   240
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   241
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   242
  "ge a [] = True"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   243
  "ge a (x#xs) = (x \<le> a \<and> ge a xs)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   244
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   245
primrec
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   246
  "list_of Empty = []"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   247
  "list_of (Node n t1 t2) = list_of t1 @ [n] @ list_of t2"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   248
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   249
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   250
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   251
  "le x (a@b) = (le x a \<and> le x b)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   252
  apply (induct_tac a)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   253
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   254
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   255
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   256
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   257
  "ge x (a@b) = (ge x a \<and> ge x b)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   258
  apply (induct_tac a)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   259
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   260
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   261
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   262
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   263
  "sorted (a@x#b) = (sorted a \<and> sorted b \<and> ge x a \<and> le x b)"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   264
  apply (induct_tac a)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   265
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   266
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   267
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   268
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   269
  "ge n (list_of t) = tge n t"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   270
  apply (induct_tac t)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   271
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   272
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   273
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   274
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   275
  "le n (list_of t) = tle n t"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   276
  apply (induct_tac t)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   277
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   278
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   279
  
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   280
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   281
  "sorted (list_of t) = tsorted t"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   282
  apply (induct_tac t)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   283
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   284
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   285
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   286
theorem "sorted (list_of (tree_of xs))"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   287
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   288
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   289
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   290
lemma count_append [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   291
  "count (a@b) n = count a n + count b n"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   292
  apply (induct a)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   293
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   294
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   295
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   296
lemma [simp]:
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   297
  "count (list_of b) n = tcount b n"
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   298
  apply (induct b)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   299
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   300
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   301
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   302
theorem "count (list_of (tree_of xs)) n = count xs n"    
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   303
  apply (induct xs)
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   304
  apply auto
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   305
  done
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   306
f5d0a66c8124 exercise collection
kleing
parents:
diff changeset
   307
end