5 inductive

     5 

     6   even :: "nat \<Rightarrow> bool" and

     6 (* inductive_cases do not simplify with simple equations *)

     7   odd  :: "nat \<Rightarrow> bool"

     7 atom_decl var

     8 where

     8 nominal_datatype expr =

     9   "even 0"

     9   eCnst nat

    10 | "odd n \<Longrightarrow> even (Suc n)"

    10 | eVar nat

    11 | "even n \<Longrightarrow> odd (Suc n)"

    11 

    12 

    12 inductive 

    13 thm even_odd_def

    13   eval :: "expr \<Rightarrow> nat \<Rightarrow> bool"

    14 

    14 where

    15 lemma

    15   evCnst: "eval (eCnst c) 0"

    16   shows "p \<bullet> (even n) = even (p \<bullet> n)"

    16 | evVar: "eval (eVar n) 2"

    17 unfolding even_def

    17 

    18 unfolding even_odd_def

    18 inductive_cases 

    19 apply(perm_simp)

    19   evInv_Cnst: "eval (eCnst c) m"

    20 apply(rule refl)

    20 

    21 done

    21 thm evInv_Cnst[simplified expr.distinct expr.eq_iff]

    22