theory Simple_Inductive_Package
imports Main "../Base"
uses "simple_inductive_package.ML"
begin

(*
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
*)

use_chunks "simple_inductive_package.ML"


end