Email Gateway (Aug 18 2022 at 13:00): Email Gateway (Aug 18 2022 at 13:00):From: "\"Juan Rodriguez Hortalá\"" <juanrh@fdi.ucm.es>
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".
Any help will be appreciated, regards,
Juan
Email Gateway (Aug 18 2022 at 13:00):From: Stefan Berghofer <berghofe@in.tum.de>
Juan Rodriguez Hortalá wrote:
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
Last updated: May 03 2024 at 01:09 UTC