Re: [isabelle] Simplifier not simplifying statement



Hi Joshua,

Implementing a new logic in Isabelle is very much more difficult than using Isabelle/HOL or Isabelle/ZF out of the box. The simplifier and classical reasoner both have to be set up for a new logic, and this is only possible if the logic conforms to the basic requirements. For the simplifier, you need an equality relation taking just two arguments (so x=y, not x=y:A) and satisfying the usual properties. For the classical reasoner, you need normal-looking natural deduction rules, and I'm not sure how well it will work if your rules mention proof objects explicitly.

Anyway, by default, simp will do little or nothing for you. You will need to use the primitive proof methods such as rule and assumption. In the example you give, your three subgoals can all be solved by assumption.

You'll need to follow CTT (and possibly CCL) very closely to see how things are done there. CTT implements its own very basic simplifier that works by resolution alone. (This relies on having extensional equality.)

Larry Paulson



> On 23 May 2018, at 20:25, Joshua Chen <joshua.chen at uni-bonn.de> wrote:
> 
> 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
>> 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.