1 theory Simple_Inductive_Package

     2 imports Main "../Base"

     3 uses "simple_inductive_package.ML"

     4 begin

     5 

     6 (*

     7 simple_inductive

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

     9 where

    10   base: "trcl R x x"

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

    12 

    13 thm trcl_def

    14 thm trcl.induct

    15 thm trcl.intros

    16 

    17 simple_inductive

    18   even and odd

    19 where

    20   even0: "even 0"

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

    22 | oddS: "even n \<Longrightarrow> odd (Suc n)"

    23 

    24 thm even_def odd_def

    25 thm even.induct odd.induct

    26 thm even0

    27 thm evenS

    28 thm oddS

    29 thm even_odd.intros

    30 

    31 simple_inductive

    32   accpart for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    33 where

    34   accpartI: "(\<And>y. r y x \<Longrightarrow> accpart r y) \<Longrightarrow> accpart r x"

    35 

    36 thm accpart_def

    37 thm accpart.induct

    38 thm accpartI

    39 

    40 locale rel =

    41   fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

    42 

    43 simple_inductive (in rel) accpart'

    44 where

    45   accpartI': "\<And>x. (\<And>y. r y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"

    46 

    47 

    48 context rel

    49 begin

    50   thm accpartI'

    51   thm accpart'.induct

    52 end

    53 

    54 thm rel.accpartI'

    55 thm rel.accpart'.induct

    56 *)

    57 

    58 use_chunks "simple_inductive_package.ML"

    59 

    60 

    61 end