*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplifier not simplifying statement*From*: "Joshua Chen" <joshua.chen at uni-bonn.de>*Date*: Wed, 23 May 2018 21:25:31 +0200*In-reply-to*: <web-9511474@be4.uni-bonn.de>*References*: <web-9511474@be4.uni-bonn.de>

Is there any proof method that does this instead?

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

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 myfunction type definition (which I can provide ifnecessary, it's mostly the same as that insrc/CTT/CTT.thy).Code:1 lemma lemma1: "!!x. A : U ==> B : U ==> x : A ==>\<^bold>\lambda y. x : B -> A" ..23 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 usesimp_all with lemma1.The output after line 4 is: proof (prove) goal (2 subgoals): 1. A : U ==> B : U ==> A : U2. !!x. A : U ==> B : U ==> x : A ==> \<^bold>\lambday. x : B -> Aand after line 5: proof (prove) goal (1 subgoal):1. !!x. A : U ==> B : U ==> x : A ==> \<^bold>\lambday. 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 -> AWould anyone know why the simplifier did not use lemma1to solve subgoal 2?Thanks very much for any advice! Best, Josh

**Follow-Ups**:**Re: [isabelle] Simplifier not simplifying statement***From:*Lawrence Paulson

**References**:**[isabelle] Simplifier not simplifying statement***From:*Joshua Chen

- Previous by Date: Re: [isabelle] Running opentheory in Isabelle
- Next by Date: [isabelle] isabelle doc - where to start?
- Previous by Thread: [isabelle] Simplifier not simplifying statement
- Next by Thread: Re: [isabelle] Simplifier not simplifying statement
- Cl-isabelle-users May 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list