Email Gateway (Aug 19 2022 at 12:57): Email Gateway (Aug 19 2022 at 12:57):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Email Gateway (Aug 19 2022 at 12:59):From: Brian Huffman <huffman.brian.c@gmail.com>
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".
Last updated: Apr 16 2024 at 12:28 UTC