theory Simple_Inductive_Package

imports Main "../Base"

keywords "simple_inductive" :: thy_decl

begin

ML_file "simple_inductive_package.ML"

simple_inductive

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

where

  base: "trcl R x x"

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

thm trcl_def

thm trcl.induct

thm trcl.intros

(*

simple_inductive

  even and odd

where

  even0: "even 0"

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

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

thm even_def odd_def

thm even.induct odd.induct

thm even0

thm evenS

thm oddS

thm even_odd.intros

simple_inductive

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

where

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

thm accpart_def

thm accpart.induct

thm accpartI

locale rel =

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

simple_inductive (in rel) accpart'

where

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

context rel

begin

  thm accpartI'

  thm accpart'.induct

end

thm rel.accpartI'

thm rel.accpart'.induct

*)

end