src/Doc/Tutorial/Trie/Trie.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
child 58305 57752a91eec4
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     1
(*<*)
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15905
diff changeset
     2
theory Trie imports Main begin;
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     3
(*>*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     4
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     5
To minimize running time, each node of a trie should contain an array that maps
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10171
diff changeset
     6
letters to subtries. We have chosen a
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     7
representation where the subtries are held in an association list, i.e.\ a
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
     8
list of (letter,trie) pairs.  Abstracting over the alphabet @{typ"'a"} and the
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
     9
values @{typ"'v"} we define a trie as follows:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    10
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    11
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    12
datatype ('a,'v)trie = Trie  "'v option"  "('a * ('a,'v)trie)list";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    13
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    14
text{*\noindent
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
    15
\index{datatypes!and nested recursion}%
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    16
The first component is the optional value, the second component the
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    17
association list of subtries.  This is an example of nested recursion involving products,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    18
which is fine because products are datatypes as well.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    19
We define two selector functions:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    20
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    21
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    22
primrec "value" :: "('a,'v)trie \<Rightarrow> 'v option" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    23
"value(Trie ov al) = ov"
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    24
primrec alist :: "('a,'v)trie \<Rightarrow> ('a * ('a,'v)trie)list" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    25
"alist(Trie ov al) = al"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    26
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    27
text{*\noindent
11309
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11303
diff changeset
    28
Association lists come with a generic lookup function.  Its result
d666f11ca2d4 minor suggestions by Tanja Vos
paulson
parents: 11303
diff changeset
    29
involves type @{text option} because a lookup can fail:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    30
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    31
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    32
primrec assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    33
"assoc [] x = None" |
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    34
"assoc (p#ps) x =
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    35
   (let (a,b) = p in if a=x then Some b else assoc ps x)"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    37
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    38
Now we can define the lookup function for tries. It descends into the trie
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    39
examining the letters of the search string one by one. As
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    40
recursion on lists is simpler than on tries, let us express this as primitive
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    41
recursion on the search string argument:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    42
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    43
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    44
primrec lookup :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v option" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    45
"lookup t [] = value t" |
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    46
"lookup t (a#as) = (case assoc (alist t) a of
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    47
                      None \<Rightarrow> None
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    48
                    | Some at \<Rightarrow> lookup at as)"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    49
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    51
As a first simple property we prove that looking up a string in the empty
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
    52
trie @{term"Trie None []"} always returns @{const None}. The proof merely
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    53
distinguishes the two cases whether the search string is empty or not:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    54
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    55
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    56
lemma [simp]: "lookup (Trie None []) as = None";
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    57
apply(case_tac as, simp_all);
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    58
done
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    59
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    60
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    61
Things begin to get interesting with the definition of an update function
12328
7c4ec77a8715 *** empty log message ***
nipkow
parents: 11458
diff changeset
    62
that adds a new (string, value) pair to a trie, overwriting the old value
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    63
associated with that string:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    64
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    65
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    66
primrec update:: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)trie" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    67
"update t []     v = Trie (Some v) (alist t)" |
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    68
"update t (a#as) v =
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    69
   (let tt = (case assoc (alist t) a of
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    70
                None \<Rightarrow> Trie None [] | Some at \<Rightarrow> at)
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
    71
    in Trie (value t) ((a,update tt as v) # alist t))"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    72
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    73
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    74
The base case is obvious. In the recursive case the subtrie
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    75
@{term tt} associated with the first letter @{term a} is extracted,
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    76
recursively updated, and then placed in front of the association list.
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    77
The old subtrie associated with @{term a} is still in the association list
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
    78
but no longer accessible via @{const assoc}. Clearly, there is room here for
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    79
optimizations!
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    80
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
    81
Before we start on any proofs about @{const update} we tell the simplifier to
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    82
expand all @{text let}s and to split all @{text case}-constructs over
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    83
options:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    84
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    85
9933
9feb1e0c4cb3 *** empty log message ***
nipkow
parents: 9792
diff changeset
    86
declare Let_def[simp] option.split[split]
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    87
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    88
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    89
The reason becomes clear when looking (probably after a failed proof
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
    90
attempt) at the body of @{const update}: it contains both
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    91
@{text let} and a case distinction over type @{text option}.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    92
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
    93
Our main goal is to prove the correct interaction of @{const update} and
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
    94
@{const lookup}:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    95
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    96
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    97
theorem "\<forall>t v bs. lookup (update t as v) bs =
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    98
                    (if as=bs then Some v else lookup t bs)";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    99
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   100
txt{*\noindent
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
   101
Our plan is to induct on @{term as}; hence the remaining variables are
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   102
quantified. From the definitions it is clear that induction on either
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
   103
@{term as} or @{term bs} is required. The choice of @{term as} is 
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
   104
guided by the intuition that simplification of @{const lookup} might be easier
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
   105
if @{const update} has already been simplified, which can only happen if
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
   106
@{term as} is instantiated.
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
   107
The start of the proof is conventional:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   108
*};
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8745
diff changeset
   109
apply(induct_tac as, auto);
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   110
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   111
txt{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   112
Unfortunately, this time we are left with three intimidating looking subgoals:
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9689
diff changeset
   113
\begin{isabelle}
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   114
~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   115
~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   116
~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9689
diff changeset
   117
\end{isabelle}
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
   118
Clearly, if we want to make headway we have to instantiate @{term bs} as
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   119
well now. It turns out that instead of induction, case distinction
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   120
suffices:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   121
*};
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
   122
apply(case_tac[!] bs, auto);
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
   123
done
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   124
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   125
text{*\noindent
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
   126
\index{subgoal numbering}%
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
   127
All methods ending in @{text tac} take an optional first argument that
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   128
specifies the range of subgoals they are applied to, where @{text"[!]"} means
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   129
all subgoals, i.e.\ @{text"[1-3]"} in our case. Individual subgoal numbers,
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   130
e.g. @{text"[2]"} are also allowed.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   131
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   132
This proof may look surprisingly straightforward. However, note that this
9792
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   133
comes at a cost: the proof script is unreadable because the intermediate
bbefb6ce5cb2 *** empty log message ***
nipkow
parents: 9723
diff changeset
   134
proof states are invisible, and we rely on the (possibly brittle) magic of
10971
6852682eaf16 *** empty log message ***
nipkow
parents: 10795
diff changeset
   135
@{text auto} (@{text simp_all} will not do --- try it) to split the subgoals
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
   136
of the induction up in such a way that case distinction on @{term bs} makes
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
   137
sense and solves the proof. 
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   138
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   139
\begin{exercise}
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
   140
  Modify @{const update} (and its type) such that it allows both insertion and
11303
f0661da2f6ae typo, etc.
paulson
parents: 11294
diff changeset
   141
  deletion of entries with a single function.  Prove the corresponding version 
f0661da2f6ae typo, etc.
paulson
parents: 11294
diff changeset
   142
  of the main theorem above.
f0661da2f6ae typo, etc.
paulson
parents: 11294
diff changeset
   143
  Optimize your function such that it shrinks tries after
f0661da2f6ae typo, etc.
paulson
parents: 11294
diff changeset
   144
  deletion if possible.
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   145
\end{exercise}
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   146
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   147
\begin{exercise}
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
   148
  Write an improved version of @{const update} that does not suffer from the
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   149
  space leak (pointed out above) caused by not deleting overwritten entries
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   150
  from the association list. Prove the main theorem for your improved
15905
0a4cc9b113c7 introduced @{const ...} antiquotation
haftmann
parents: 12328
diff changeset
   151
  @{const update}.
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   152
\end{exercise}
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   153
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   154
\begin{exercise}
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   155
  Conceptually, each node contains a mapping from letters to optional
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   156
  subtries. Above we have implemented this by means of an association
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   157
  list. Replay the development replacing @{typ "('a * ('a,'v)trie)list"}
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   158
  with @{typ"'a \<Rightarrow> ('a,'v)trie option"}.
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   159
\end{exercise}
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   160
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   161
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   162
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   163
(*<*)
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   164
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   165
(* Exercise 1. Solution by Getrud Bauer *)
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   166
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   167
primrec update1 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   168
where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   169
  "update1 t []     vo = Trie vo (alist t)" |
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   170
  "update1 t (a#as) vo =
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   171
     (let tt = (case assoc (alist t) a of
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   172
                  None \<Rightarrow> Trie None [] 
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   173
                | Some at \<Rightarrow> at)
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   174
      in Trie (value t) ((a, update1 tt as vo) # alist t))"
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   175
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   176
theorem [simp]: "\<forall>t v bs. lookup (update1 t as v) bs =
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   177
                    (if as = bs then v else lookup t bs)";
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   178
apply (induct_tac as, auto);
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   179
apply (case_tac[!] bs, auto);
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   180
done
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   181
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   182
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   183
(* Exercise 2. Solution by Getrud Bauer *)
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   184
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   185
primrec overwrite :: "'a \<Rightarrow> 'b \<Rightarrow> ('a * 'b) list \<Rightarrow> ('a * 'b) list" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   186
"overwrite a v [] = [(a,v)]" |
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   187
"overwrite a v (p#ps) = (if a = fst p then (a,v)#ps else p # overwrite a v ps)"
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   188
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   189
lemma [simp]: "\<forall> a v b. assoc (overwrite a v ps) b = assoc ((a,v)#ps) b"
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   190
apply (induct_tac ps, auto)
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   191
apply (case_tac[!] a)
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   192
done
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   193
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   194
primrec update2 :: "('a, 'v) trie \<Rightarrow> 'a list \<Rightarrow> 'v option \<Rightarrow> ('a, 'v) trie"
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   195
where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   196
  "update2 t []     vo = Trie vo (alist t)" |
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   197
  "update2 t (a#as) vo =
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   198
     (let tt = (case assoc (alist t) a of 
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   199
                  None \<Rightarrow> Trie None []  
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   200
                | Some at \<Rightarrow> at) 
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   201
      in Trie (value t) (overwrite a (update2 tt as vo) (alist t)))"; 
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   202
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   203
theorem "\<forall>t v bs. lookup (update2 t as vo) bs =
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   204
                    (if as = bs then vo else lookup t bs)";
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   205
apply (induct_tac as, auto);
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   206
apply (case_tac[!] bs, auto);
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   207
done
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   208
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   209
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   210
(* Exercise 3. Solution by Getrud Bauer *)
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   211
datatype ('a,'v) triem = Triem  "'v option" "'a \<Rightarrow> ('a,'v) triem option";
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   212
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   213
primrec valuem :: "('a, 'v) triem \<Rightarrow> 'v option" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   214
"valuem (Triem ov m) = ov"
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   215
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   216
primrec mapping :: "('a,'v) triem \<Rightarrow> 'a \<Rightarrow> ('a, 'v) triem option" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   217
"mapping (Triem ov m) = m"
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   218
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   219
primrec lookupm :: "('a,'v) triem \<Rightarrow> 'a list \<Rightarrow> 'v option" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   220
  "lookupm t [] = valuem t" |
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   221
  "lookupm t (a#as) = (case mapping t a of
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   222
                        None \<Rightarrow> None
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   223
                      | Some at \<Rightarrow> lookupm at as)";
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   224
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   225
lemma [simp]: "lookupm (Triem None  (\<lambda>c. None)) as = None";
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   226
apply (case_tac as, simp_all);
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   227
done
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   228
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   229
primrec updatem :: "('a,'v)triem \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)triem" where
f8537d69f514 *** empty log message ***
nipkow
parents: 17555
diff changeset
   230
  "updatem t []     v = Triem (Some v) (mapping t)" |
11294
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   231
  "updatem t (a#as) v =
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   232
     (let tt = (case mapping t a of
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   233
                  None \<Rightarrow> Triem None (\<lambda>c. None) 
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   234
                | Some at \<Rightarrow> at)
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   235
      in Triem (valuem t) 
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   236
              (\<lambda>c. if c = a then Some (updatem tt as v) else mapping t c))";
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   237
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   238
theorem "\<forall>t v bs. lookupm (updatem t as v) bs = 
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   239
                    (if as = bs then Some v else lookupm t bs)";
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   240
apply (induct_tac as, auto);
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   241
apply (case_tac[!] bs, auto);
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   242
done
16481a4cc9f3 *** empty log message ***
nipkow
parents: 10978
diff changeset
   243
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   244
end;
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   245
(*>*)