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