doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs

added an intro lemma for freshness of products; set up
the simplifier so that it can deal with the compact and
long notation for freshness constraints (FIXME: it should
also be able to deal with the special case of freshness
of atoms)

module Codegen where
import qualified Nat

class Null a where
  null :: a

head :: (Codegen.Null a_1) => [a_1] -> a_1
head (y : xs) = y
head [] = Codegen.null

null_option :: Maybe b
null_option = Nothing

instance Codegen.Null (Maybe b) where
  null = Codegen.null_option

dummy :: Maybe Nat.Nat
dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]