Re: [isabelle] Inductive set and tutorial



Juan Rodriguez Hortalá wrote:
> Dear list, I'm afraid I'm still having troubles with the updated tutorial of http://isabelle.in.tum.de/devel/Isabelle_04-Feb-2009_pdf.tar.gz. Everithing was fine until this example of page 19 of isar-overview.pdf
> 
> inductive_set
>   rtc :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a)set"   ("_*" [1000] 999)
>   for r :: "('a \<times> 'a)set"
> where
>   refl: "(x,x) \<in> r\<^sup>*"
> | step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r\<^sup>* \<rbrakk> \<Longrightarrow> (x,z) \<in> r\<^sup>*"
> 
> *** Ill-formed introduction rule "refl"
> *** r^** x x
> *** Conclusion of introduction rule must be an inductive predicate
> *** At command "inductive_set".

Hi,

you confused r\<^sup>* (which is already defined in HOL/Transitive_Closure.thy) with
r* (which is only used in the tutorial). If you replace r\<^sup>* by r* in the rules
refl and step, the definition should work as expected.

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.