theory Simple_Inductive_Packageimports Main "../Base"keywords "simple_inductive" :: thy_declbeginML_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_defthm trcl.inductthm trcl.introssimple_inductive even and oddwhere even0: "even 0"| evenS: "odd n \<Longrightarrow> even (Suc n)"| oddS: "even n \<Longrightarrow> odd (Suc n)"thm even_def odd_defthm even.induct odd.inductthm even0thm evenSthm oddSthm even_odd.introssimple_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_defthm accpart.inductthm accpartIlocale 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 relbegin thm accpartI' thm accpart'.inductendthm rel.accpartI'thm rel.accpart'.induct*)end