# [isabelle] Simplifier not simplifying statement

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

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