diff -r dfff821d2949 -r 59d6633835fa doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Mon Oct 09 09:33:45 2000 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Mon Oct 09 10:18:21 2000 +0200 @@ -18,8 +18,8 @@ We define two selector functions: *}; -consts value :: "('a,'v)trie \\ 'v option" - alist :: "('a,'v)trie \\ ('a * ('a,'v)trie)list"; +consts value :: "('a,'v)trie \ 'v option" + alist :: "('a,'v)trie \ ('a * ('a,'v)trie)list"; primrec "value(Trie ov al) = ov"; primrec "alist(Trie ov al) = al"; @@ -27,7 +27,7 @@ Association lists come with a generic lookup function: *}; -consts assoc :: "('key * 'val)list \\ 'key \\ 'val option"; +consts assoc :: "('key * 'val)list \ 'key \ 'val option"; primrec "assoc [] x = None" "assoc (p#ps) x = (let (a,b) = p in if a=x then Some b else assoc ps x)"; @@ -39,20 +39,21 @@ recursion on the search string argument: *}; -consts lookup :: "('a,'v)trie \\ 'a list \\ 'v option"; +consts lookup :: "('a,'v)trie \ 'a list \ 'v option"; primrec "lookup t [] = value t" "lookup t (a#as) = (case assoc (alist t) a of - None \\ None - | Some at \\ lookup at as)"; + None \ None + | Some at \ lookup at as)"; text{* As a first simple property we prove that looking up a string in the empty -trie @{term"Trie None []"} always returns @{term"None"}. The proof merely +trie @{term"Trie None []"} always returns @{term None}. The proof merely distinguishes the two cases whether the search string is empty or not: *}; lemma [simp]: "lookup (Trie None []) as = None"; -by(case_tac as, simp_all); +apply(case_tac as, simp_all); +done text{* Things begin to get interesting with the definition of an update function @@ -60,24 +61,24 @@ associated with that string: *}; -consts update :: "('a,'v)trie \\ 'a list \\ 'v \\ ('a,'v)trie"; +consts update :: "('a,'v)trie \ 'a list \ 'v \ ('a,'v)trie"; primrec "update t [] v = Trie (Some v) (alist t)" "update t (a#as) v = (let tt = (case assoc (alist t) a of - None \\ Trie None [] | Some at \\ at) + None \ Trie None [] | Some at \ at) in Trie (value t) ((a,update tt as v)#alist t))"; text{*\noindent The base case is obvious. In the recursive case the subtrie -@{term"tt"} associated with the first letter @{term"a"} is extracted, +@{term tt} associated with the first letter @{term a} is extracted, recursively updated, and then placed in front of the association list. -The old subtrie associated with @{term"a"} is still in the association list -but no longer accessible via @{term"assoc"}. Clearly, there is room here for +The old subtrie associated with @{term a} is still in the association list +but no longer accessible via @{term assoc}. Clearly, there is room here for optimizations! -Before we start on any proofs about @{term"update"} we tell the simplifier to -expand all @{text"let"}s and to split all @{text"case"}-constructs over +Before we start on any proofs about @{term update} we tell the simplifier to +expand all @{text let}s and to split all @{text case}-constructs over options: *}; @@ -85,23 +86,23 @@ text{*\noindent The reason becomes clear when looking (probably after a failed proof -attempt) at the body of @{term"update"}: it contains both -@{text"let"} and a case distinction over type @{text"option"}. +attempt) at the body of @{term update}: it contains both +@{text let} and a case distinction over type @{text option}. -Our main goal is to prove the correct interaction of @{term"update"} and -@{term"lookup"}: +Our main goal is to prove the correct interaction of @{term update} and +@{term lookup}: *}; -theorem "\\t v bs. lookup (update t as v) bs = +theorem "\t v bs. lookup (update t as v) bs = (if as=bs then Some v else lookup t bs)"; txt{*\noindent -Our plan is to induct on @{term"as"}; hence the remaining variables are +Our plan is to induct on @{term as}; hence the remaining variables are quantified. From the definitions it is clear that induction on either -@{term"as"} or @{term"bs"} is required. The choice of @{term"as"} is merely -guided by the intuition that simplification of @{term"lookup"} might be easier -if @{term"update"} has already been simplified, which can only happen if -@{term"as"} is instantiated. +@{term as} or @{term bs} is required. The choice of @{term as} is merely +guided by the intuition that simplification of @{term lookup} might be easier +if @{term update} has already been simplified, which can only happen if +@{term as} is instantiated. The start of the proof is completely conventional: *}; apply(induct_tac as, auto); @@ -113,14 +114,15 @@ ~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline ~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs \end{isabelle} -Clearly, if we want to make headway we have to instantiate @{term"bs"} as +Clearly, if we want to make headway we have to instantiate @{term bs} as well now. It turns out that instead of induction, case distinction suffices: *}; -by(case_tac[!] bs, auto); +apply(case_tac[!] bs, auto); +done text{*\noindent -All methods ending in @{text"tac"} take an optional first argument that +All methods ending in @{text tac} take an optional first argument that specifies the range of subgoals they are applied to, where @{text"[!]"} means all subgoals, i.e.\ @{text"[1-3]"} in our case. Individual subgoal numbers, e.g. @{text"[2]"} are also allowed. @@ -128,8 +130,8 @@ This proof may look surprisingly straightforward. However, note that this comes at a cost: the proof script is unreadable because the intermediate proof states are invisible, and we rely on the (possibly brittle) magic of -@{text"auto"} (@{text"simp_all"} will not do---try it) to split the subgoals -of the induction up in such a way that case distinction on @{term"bs"} makes +@{text auto} (@{text simp_all} will not do---try it) to split the subgoals +of the induction up in such a way that case distinction on @{term bs} makes sense and solves the proof. Part~\ref{Isar} shows you how to write readable and stable proofs. *};