src/HOL/IMP/Util.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 44177 b4b5cbca2519
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@43158
     3
theory Util imports Main
kleing@43158
     4
begin
kleing@43158
     5
kleing@43158
     6
subsection "Show sets of variables as lists"
kleing@43158
     7
kleing@44177
     8
text {* Sets may be infinite and are not always displayed by element 
kleing@44177
     9
  if computed as values. Lists do not have this problem. 
kleing@43158
    10
kleing@44177
    11
  We define a function @{text show} that converts a set of
kleing@43158
    12
  variable names into a list. To keep things simple, we rely on
kleing@43158
    13
  the convention that we only use single letter names.
kleing@43158
    14
*}
kleing@43158
    15
definition 
kleing@43158
    16
  letters :: "string list" where
kleing@43158
    17
  "letters = map (\<lambda>c. [c]) chars"
kleing@43158
    18
kleing@43158
    19
definition 
kleing@43158
    20
  "show" :: "string set \<Rightarrow> string list" where
huffman@44174
    21
  "show S = filter (\<lambda>x. x \<in> S) letters" 
kleing@43158
    22
kleing@43158
    23
value "show {''x'', ''z''}"
kleing@43158
    24
kleing@43158
    25
end