Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] failing inductive definition

Email Gateway (Aug 17 2022 at 14:46):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
The following inductive definition

inductive "hpo sig S crel r"
intros (* note order *)
ctxtI : "(t, s) : ctxt (hpo sig S crel r) ==> (t, s) : hpo sig S
crel r"
subtI : "si : set ss ==> (si, Node f ss) : hpo sig S crel r"
monos red_mono

fails as follows:

Exception- ERROR raised
*** Bad final proof state:
*** A <= B --> hpo sig S crel A <= hpo sig S crel B
*** 1. !!a b s t.
*** [| A <= B;
*** (t, s)
*** : ctxt
*** (hpo sig S crel A Int
*** {x. (%(v, u). (v, u) : hpo sig S crel B) x}) |]
*** ==> (t, s) : ctxt (hpo sig S crel B)
*** 1 unsolved goals!
*** Proof failed!
*** The error(s) above occurred for "A <= B --> hpo sig S crel A <= hpo
sig S crel B"
*** At command "use".

The theorem red_mono is
val it = "?r <= ?s ==> ctxt ?r <= ctxt ?s" : Thm.thm

When I remove either of the two introduction clauses in the definition,
the definition succeeds, which I find odd.

Can anyone help on this?

Thanks

Jeremy

Email Gateway (Aug 17 2022 at 14:46):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Jeremy Dawson wrote:
Please ignore the previous message, the problem was elsewhere

Jeremy

Last updated: May 03 2024 at 08:18 UTC