doc-src/TutorialI/Trie/Trie.thy
author nipkow
Tue, 29 Aug 2000 16:05:13 +0200
changeset 9723 a977245dfc8a
parent 9689 751fde5307e4
child 9792 bbefb6ce5cb2
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     1
(*<*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     2
theory Trie = Main:;
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
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     6
letters to subtries. We have chosen a (sometimes) more space efficient
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
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     8
list of (letter,trie) pairs.  Abstracting over the alphabet \isa{'a} and the
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     9
values \isa{'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
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    15
The first component is the optional value, the second component the
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    16
association list of subtries.  This is an example of nested recursion involving products,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    17
which is fine because products are datatypes as well.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    18
We define two selector functions:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    19
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    20
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    21
consts value :: "('a,'v)trie \\<Rightarrow> 'v option"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    22
       alist :: "('a,'v)trie \\<Rightarrow> ('a * ('a,'v)trie)list";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    23
primrec "value(Trie ov al) = ov";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    24
primrec "alist(Trie ov al) = al";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    25
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    26
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    27
Association lists come with a generic lookup function:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    28
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    29
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    30
consts   assoc :: "('key * 'val)list \\<Rightarrow> 'key \\<Rightarrow> 'val option";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    31
primrec "assoc [] x = None"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    32
        "assoc (p#ps) x =
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    33
           (let (a,b) = p in if a=x then Some b else assoc ps x)";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    34
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    35
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
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
    37
examining the letters of the search string one by one. As
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    38
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
    39
recursion on the search string argument:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    40
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    41
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    42
consts   lookup :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v option";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    43
primrec "lookup t [] = value t"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    44
        "lookup t (a#as) = (case assoc (alist t) a of
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    45
                              None \\<Rightarrow> None
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    46
                            | Some at \\<Rightarrow> lookup at as)";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    47
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    48
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    49
As a first simple property we prove that looking up a string in the empty
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    51
distinguishes the two cases whether the search string is empty or not:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    52
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    53
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    54
lemma [simp]: "lookup (Trie None []) as = None";
9689
751fde5307e4 *** empty log message ***
nipkow
parents: 9541
diff changeset
    55
by(case_tac as, simp_all);
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    56
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    57
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    58
Things begin to get interesting with the definition of an update function
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    59
that adds a new (string,value) pair to a trie, overwriting the old value
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    60
associated with that string:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    61
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    62
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    63
consts update :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v \\<Rightarrow> ('a,'v)trie";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    64
primrec
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    65
  "update t []     v = Trie (Some v) (alist t)"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    66
  "update t (a#as) v =
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    67
     (let tt = (case assoc (alist t) a of
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    68
                  None \\<Rightarrow> Trie None [] | Some at \\<Rightarrow> at)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    69
      in Trie (value t) ((a,update tt as v)#alist t))";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    70
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    71
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    72
The base case is obvious. In the recursive case the subtrie
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    73
\isa{tt} associated with the first letter \isa{a} is extracted,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    74
recursively updated, and then placed in front of the association list.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    75
The old subtrie associated with \isa{a} is still in the association list
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    76
but no longer accessible via \isa{assoc}. Clearly, there is room here for
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    77
optimizations!
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    78
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    79
Before we start on any proofs about \isa{update} we tell the simplifier to
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    80
expand all \isa{let}s and to split all \isa{case}-constructs over
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    81
options:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    82
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    83
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
    84
lemmas [simp] = Let_def;
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
    85
lemmas [split] = option.split;
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    86
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    87
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    88
The reason becomes clear when looking (probably after a failed proof
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    89
attempt) at the body of \isa{update}: it contains both
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    90
\isa{let} and a case distinction over type \isa{option}.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    91
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    92
Our main goal is to prove the correct interaction of \isa{update} and
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    93
\isa{lookup}:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
    94
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    95
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    96
theorem "\\<forall>t v bs. lookup (update t as v) bs =
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    97
                    (if as=bs then Some v else lookup t bs)";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    98
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    99
txt{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   100
Our plan is to induct on \isa{as}; hence the remaining variables are
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   101
quantified. From the definitions it is clear that induction on either
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   102
\isa{as} or \isa{bs} is required. The choice of \isa{as} is merely
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   103
guided by the intuition that simplification of \isa{lookup} might be easier
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   104
if \isa{update} has already been simplified, which can only happen if
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   105
\isa{as} is instantiated.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   106
The start of the proof is completely conventional:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   107
*};
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8745
diff changeset
   108
apply(induct_tac as, auto);
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   109
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   110
txt{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   111
Unfortunately, this time we are left with three intimidating looking subgoals:
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9689
diff changeset
   112
\begin{isabelle}
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   113
~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   114
~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   115
~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
9723
a977245dfc8a *** empty log message ***
nipkow
parents: 9689
diff changeset
   116
\end{isabelle}
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   117
Clearly, if we want to make headway we have to instantiate \isa{bs} as
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   118
well now. It turns out that instead of induction, case distinction
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   119
suffices:
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   120
*};
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
   121
by(case_tac[!] bs, auto);
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   122
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   123
text{*\noindent
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
   124
All methods ending in \isa{tac} take an optional first argument that
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
   125
specifies the range of subgoals they are applied to, where \isa{[!]} means all
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
   126
subgoals, i.e.\ \isa{[1-3]} in our case. Individual subgoal numbers,
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
   127
e.g. \isa{[2]} are also allowed.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   128
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   129
This proof may look surprisingly straightforward. However, note that this
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   130
comes at a cost: the proof script is unreadable because the
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   131
intermediate proof states are invisible, and we rely on the (possibly
9689
751fde5307e4 *** empty log message ***
nipkow
parents: 9541
diff changeset
   132
brittle) magic of \isa{auto} (\isa{simp\_all} will not do---try it) to split the subgoals
751fde5307e4 *** empty log message ***
nipkow
parents: 9541
diff changeset
   133
of the induction up in such a way that case distinction on \isa{bs} makes sense and
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   134
solves the proof. Part~\ref{Isar} shows you how to write readable and stable
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   135
proofs.
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   136
*};
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   137
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   138
(*<*)
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8771
diff changeset
   139
end;
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   140
(*>*)