Re: [isabelle] Non-atomic premise



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




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