theory Simple_Inductive_Package+ −
imports Main "../Base"+ −
keywords "simple_inductive" :: thy_decl+ −
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+ −
*)+ −
+ −
+ −
+ −
end+ −