[isabelle] failing inductive definition




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





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