*To*: Li Yongjian <lyj238 at gmail.com>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Problems on auto solving in some basic arithmetic simplication*From*: Simon Wimmer <wimmersimon at gmail.com>*Date*: Mon, 12 Sep 2016 08:11:50 +0000*Cc*: lyj238 <lyj238 at ios.ac.cn>*In-reply-to*: <CABCjkDrwiHyU_xh1J+K2wpUhQ7PDbHvhG6jjUVY710ozxE5XZw@mail.gmail.com>*References*: <CABCjkDrwiHyU_xh1J+K2wpUhQ7PDbHvhG6jjUVY710ozxE5XZw@mail.gmail.com>

Hi Li, your observations are all related to simplification. Try typing 'apply simp' after the statement of lemma test2. You will get a goal which looks like I LAST ''-'' [index (m - Suc 0), index (Suc 0)] = index (m - 2) Now, the reason why auto and simp can't go from there is that your axiom axiomOnISub doesn't match this format for rewriting because it contains the 'index 1' bit instead of 'index (Suc 0)'. You have (at least) two options: Either you could rewrite your axiom to match this format: I LAST ''-'' [index m, index (Suc 0)] = index (m - 1) Then the lemma can be solved 'by simp'. Or you pass the axiom as a chained fact to the simplifier, which will have the effect that is processed by simplification first as well. This will rewrite '1' to 'Suc 0' and then the rule can be applied. This works by writing 'using axiomOnISub by simp'. Simon On Mon, Sep 12, 2016 at 6:58 AM Li Yongjian <lyj238 at gmail.com> wrote: > Dear all: > I meet some problem as follows: > > datatype scalrValueType=enum string string |index nat | boolV bool | topVal > | bottomVal > > axiomatization where axiomOnISub [simp,intro ]: " I LAST ''-'' [index m, > index 1] = index (m - 1)" > > > > (*lemma aux2:"I LAST ''-'' [index( m - 1 ), index 1] = index ((m - 1 ) - 1) > " > by blast*) > > lemma test2:"I LAST ''-'' [index( m - 1 ), index 1] = index (m - 2 ) " > (*by (simp only:aux2,auto)*) > using nat_1_add_1 by auto > > Q1: have thought: the lemma test2 can be solved by auto. > > Isablle's sledgehammer also hint me to use the command "using nat_1_add_1 > by auto". > > But all the above fail. I' confused about why Isabelle cann't solve the > lemma automatically. > > I can prove lemma aux2, then use simp only:aux2,auto to solve it. > > > Q2: If I add another axiom: axiomatization where axiomOnISub1 [simp,intro > ]: " I LAST ''-'' [index m, index n] = index (m - n)" > Isabelle can prove lemma test2 automatically by being given the " by auto" > command. > > why? > > Here I use ISabelle 2015, and the proof script is attached. > > regars > lyj >

**References**:

- Previous by Date: [isabelle] Problems on auto solving in some basic arithmetic simplication
- Next by Date: Re: [isabelle] Behavior of configuration options in local theories
- Previous by Thread: [isabelle] Problems on auto solving in some basic arithmetic simplication
- Next by Thread: [isabelle] Proof failed for datatype
- Cl-isabelle-users September 2016 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