# [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


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.