*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] Non-atomic premise*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Sun, 1 Dec 2013 17:55:29 -0800*Cc*: Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1385933525.29066.1.camel@kirk>*References*: <1385933525.29066.1.camel@kirk>

Hi Joachim, The problem with your second example, using "(⋀ x. P (m x) (m' x)) ⟹ fun_rel' P m m'", is that some of the inferred type variables have the empty sort "{}" instead of the usual default sort "type". (The object-level forall quantifier requires sort "type", which is why the atomization fails.) Adding the "id" functions constrains these type variables to the appropriate sort. To fix the problem you can add some type annotations for P and x: inductive fun_rel' for P :: "'a ⇒ 'b ⇒ bool" where fun_relI'[intro]: "(⋀ x::'c. P (m x) ( m' x)) ⟹ fun_rel' P m m'" Or if you'd rather have Isabelle infer the types as much as possible, you can try something like this: inductive fun_rel' for P :: "_::type" where fun_relI'[intro]: "(⋀ x::_::type. P (m x) ( m' x)) ⟹ fun_rel' P m m'" The meta-universal quantifier is defined in Pure (outside of HOL) so it makes sense for it to allow more general sorts than HOL's "type". However, I don't see any possible use for HOL-specific commands like "inductive" to allow free variables or parameters with non-"type" types. Perhaps we should make a feature request: Free variables in specifications of HOL-specific commands (e.g. the P, m, and m' in the "inductive" command above) should be constrained to have a sort no more general than "type". - Brian On Sun, Dec 1, 2013 at 1:32 PM, Joachim Breitner <breitner at kit.edu> wrote: > Hi, > > when I use > > inductive fun_rel' for P where > fun_relI'[intro]: "(⋀ x. P (id m x) (id m' x)) ⟹ fun_rel' P m > m'" > > inductive works without problem. But when I do > > inductive fun_rel' for P where > fun_relI'[intro]: "(⋀ x. P (m x) (m' x)) ⟹ fun_rel' P m m'" > > I get: > > Proofs for inductive predicate(s) "fun_rel" > Ill-formed premise > ⋀x. P (m x) (m' x) > in introduction rule "fun_relI" > ⋀m m'. (⋀x. P (m x) (m' x)) ⟹ fun_rel P m m' > Non-atomic premise > > I don’t understand the error message, nor why it should not work. Can > anyone enlighten me? > > Thanks, > Joachim > > -- > Dipl.-Math. Dipl.-Inform. Joachim Breitner > Wissenschaftlicher Mitarbeiter > http://pp.ipd.kit.edu/~breitner

**References**:**[isabelle] Non-atomic premise***From:*Joachim Breitner

- Previous by Date: [isabelle] Non-atomic premise
- Next by Date: [isabelle] comm_monoid_big not in Isabelle 2013-1
- Previous by Thread: [isabelle] Non-atomic premise
- Next by Thread: [isabelle] comm_monoid_big not in Isabelle 2013-1
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list