# Re: [isabelle] Simplifier not simplifying statement

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

On Wed, 23 May 2018 17:30:39 +0200
"Joshua Chen" <joshua.chen at uni-bonn.de> wrote:

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


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





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