theory Inductive_Examples imports Simple_Inductive_Package begin section {* Transitive closure *} simple_inductive trcl for r :: "'a \ 'a \ bool" where base: "trcl r x x" | step: "trcl r x y \ r y z \ trcl r x z" thm trcl_def thm trcl.induct thm base thm step thm trcl.intros lemma trcl_strong_induct: assumes trcl: "trcl r x y" and I1: "\x. P x x" and I2: "\x y z. P x y \ trcl r x y \ r y z \ P x z" shows "P x y" proof - from trcl have "P x y \ trcl r x y" proof induct case (base x) from I1 and trcl.base show ?case .. next case (step x y z) then have "P x y" and "trcl r x y" by simp_all from `P x y` `trcl r x y` `r y z` have "P x z" by (rule I2) moreover from `trcl r x y` `r y z` have "trcl r x z" by (rule trcl.step) ultimately show ?case .. qed then show ?thesis .. qed section {* Even and odd numbers *} simple_inductive even and odd where even0: "even 0" | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" thm even_def odd_def thm even.induct odd.induct thm even0 thm evenS thm oddS thm even_odd.intros section {* Accessible part *} simple_inductive accpart for r :: "'a \ 'a \ bool" where accpartI: "(\y. r y x \ accpart r y) \ accpart r x" thm accpart_def thm accpart.induct thm accpartI section {* Accessible part in locale *} locale rel = fixes r :: "'a \ 'a \ bool" simple_inductive (in rel) accpart' where accpartI': "\x. (\y. r y x \ accpart' y) \ accpart' x" context rel begin thm accpartI' thm accpart'.induct end thm rel.accpartI' thm rel.accpart'.induct end