Email Gateway (Aug 19 2022 at 14:13): Email Gateway (Aug 19 2022 at 14:13):From: Edward Schwartz <edmcman@cmu.edu>
Hi all,
I'm trying to write a fairly simple proof in Isar, but I'm getting
stuck on a weird problem relating to polymorphism. Here's a minimized
example:
fun test_fun :: "'a \<Rightarrow> bool"
where
"test_fun a = True"
fun nat_fun :: "nat \<Rightarrow> bool"
where
"nat_fun a = True"
definition test_def :: "'a \<Rightarrow> bool"
where
"test_def \<equiv> \<lambda>a. True"
lemma one:
shows "\<exists>a. test_fun a"
(* fails *)
(* proof *)
(* show "test_fun a" *)
sorry
lemma two:
shows "\<exists>a. test_def a"
(* fails *)
(* proof *)
(* show "test_def a" *)
sorry
lemma three:
shows "\<exists>a. nat_fun a"
(* works *)
proof
show "nat_fun a" by simp
qed
On lemma one and two, I get errors like:
*** Failed to refine any pending goal
*** At command "show" (line 82 of "file.thy")
*** Local statement fails to refine any pending goal
*** Failed attempt to solve goal by exported rule:
*** test_fun a
*** At command "show" (line 82 of "file.thy")
Lemma three goes through fine.
Can someone help me understand what is going on? I would like to
prove lemma one or two. The problem is obviously related to
polymorphism, since lemma three goes through fine, but other than that
I am not sure what the problem is.
Thanks,
Edward
Email Gateway (Aug 19 2022 at 14:13):From: Peter Lammich <lammich@in.tum.de>
Hi.
Looks like Isabelle does not like the dangling free variable a that you
introduce. Using something else, e.g., undefined, does the job:
lemma one:
shows "\<exists>a. test_fun a"
proof
show "test_fun undefined"
by simp
qed
lemma two:
shows "\<exists>a. test_def a"
proof
show "test_def undefined"
by (simp add: test_def_def)
qed
Cheers,
Peter
Email Gateway (Aug 19 2022 at 14:13):From: Peter Lammich <lammich@in.tum.de>
A polymorphic type in a statement can be instantiated by any type. Thus,
you can think of them as being implicitely universally qualified.
What I want to state instead is:
There exists a type 'a such that there is an a :: 'a and P a.Is there any way to state such a property in Isabelle?
This is outside the expressiveness of HOL.
Another way of
thinking about this is that I want to state that there exists some
function of arity n, regardless of type, that has a certain property.
You can prove the statement
\<exists>f::'a1 => ... => 'an => 'b. P f
However, in the proof you cannot make any additional assumptions about
the type variables, in particular you cannot instantiate them.
The only way in Isabelle/HOL to express types with certain properties
are type-classes, which have several restrictions, e.g., they can only
depend on one type variable.
Email Gateway (Aug 19 2022 at 14:14):From: Makarius <makarius@sketis.net>
This sounds a bit too much like a magic addition of type classes to
Isabelle, but that is not the case. It is also not directly related to
Isabelle/HOL.
My TPHOLs paper from 1997 about type classes in Isabelle explains how that
slightly extended type system fits nicely into the existing logical
framework of Isabelle/Pure (which is a minimal version of H.O.L.).
As a spin-off you can also work with so-called "hidden polymorphism"
(which is related to "phantom types" elsewhere) using the type constructor
'a itself and the notation TYPE('a) in Pure. A predicate with more than
one TYPE('a) argument represents a general relation of types.
Doing that without the high-level interfaces of Isabelle type classes is
an arcance discipline, though. And the type-inference for type classes
does depend on the single-argument restriction, to keep things simple.
Makarius
Last updated: Apr 27 2024 at 01:05 UTC