3 keywords "simple_inductive" :: thy_decl

     3 keywords "simple_inductive" :: thy_decl

     4 begin

     4 begin

     5 

     5 

     6 ML_file "simple_inductive_package.ML"

     6 ML_file "simple_inductive_package.ML"

     7 

     7 

     9 simple_inductive

     9 simple_inductive

    10   trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

    10   trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

    11 where

    11 where

    12   base: "trcl R x x"

    12   base: "trcl R x x"

    13 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"

    13 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"

    14 

    14 

    15 thm trcl_def

    15 thm trcl_def

    16 thm trcl.induct

    16 thm trcl.induct

    17 thm trcl.intros

    17 thm trcl.intros

    18 

    18 

    19 simple_inductive

    20 simple_inductive

    20   even and odd

    21   even and odd

    21 where

    22 where

    22   even0: "even 0"

    23   even0: "even 0"

    23 | evenS: "odd n \<Longrightarrow> even (Suc n)"

    24 | evenS: "odd n \<Longrightarrow> even (Suc n)"