Email Gateway (Aug 22 2022 at 17:19): Email Gateway (Aug 22 2022 at 17:19):From: Joshua Chen <joshua.chen@uni-bonn.de>
Dear Isabelle users,
I am working on implementing a new object type theory, and
have run into the following problem when testing my
function type definition (which I can provide if
necessary, it's mostly the same as that in
src/CTT/CTT.thy).
Code:
1 lemma lemma1: "!!x. A : U ==> B : U ==> x : A ==>
\<^bold>\lambda y. x : B -> A" ..
2
3 lemma "[| A : U; B : U |] ==> \<^bold>\lambda x.
\<^bold>\lambda y. x : A -> B -> A"
4 apply standard
5 apply (simp_all add: lemma1)
Everything is fine up to line 5, where I try to use
simp_all with lemma1.
The output after line 4 is:
proof (prove)
goal (2 subgoals):
1. A : U ==> B : U ==> A : U
2. !!x. A : U ==> B : U ==> x : A ==> \<^bold>\lambda y.
x : B -> A
and after line 5:
proof (prove)
goal (1 subgoal):
1. !!x. A : U ==> B : U ==> x : A ==> \<^bold>\lambda y.
x : B -> A
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
A : U ==> B : U ==> A : U
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
!!x. A : U ==> B : U ==> x : A ==> \<^bold>\lambda y. x :
B -> A
Would anyone know why the simplifier did not use lemma1 to
solve subgoal 2?
Thanks very much for any advice!
Best,
Josh
Email Gateway (Aug 22 2022 at 17:19):From: Joshua Chen <joshua.chen@uni-bonn.de>
Ah, my apologies. I believe I misunderstood how the
simplifier works, and was expecting it to immediately
recognize when a given rule corresponds exactly to a
subgoal.
Is there any proof method that does this instead?
I was able to use "apply (rule lemma1)" to obtain three
new subgoals
1. !!x. A : U ==> B : U ==> x : A ==> A : U
2. !!x. A : U ==> B : U ==> x : A ==> B : U
3. !!x. A : U ==> B : U ==> x : A ==> x : A
which I then apply simp to prove, but it would be nice if
I could write something like "apply (lemma lemma1)" when I
have a proof state with \phi as a subgoal, and have
already previously proved \phi. I've looked in the docs
but haven't quite found something like this.
Best,
Josh
Email Gateway (Aug 22 2022 at 17:20):From: Lawrence Paulson <lp15@cam.ac.uk>
Hi Joshua,
Implementing a new logic in Isabelle is very much more difficult than using Isabelle/HOL or Isabelle/ZF out of the box. The simplifier and classical reasoner both have to be set up for a new logic, and this is only possible if the logic conforms to the basic requirements. For the simplifier, you need an equality relation taking just two arguments (so x=y, not x=y:A) and satisfying the usual properties. For the classical reasoner, you need normal-looking natural deduction rules, and I'm not sure how well it will work if your rules mention proof objects explicitly.
Anyway, by default, simp will do little or nothing for you. You will need to use the primitive proof methods such as rule and assumption. In the example you give, your three subgoals can all be solved by assumption.
You'll need to follow CTT (and possibly CCL) very closely to see how things are done there. CTT implements its own very basic simplifier that works by resolution alone. (This relies on having extensional equality.)
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC