doc-src/Tutorial/Datatype/assoc

various theorems about image and inverse image

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)"