*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Problems on auto solving in some basic arithmetic simplication*From*: Li Yongjian <lyj238 at gmail.com>*Date*: Mon, 12 Sep 2016 12:57:33 +0800*Cc*: lyj238 <lyj238 at ios.ac.cn>

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

**Attachment:
test.thy**

**Follow-Ups**:

- Previous by Date: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Next by Date: Re: [isabelle] Problems on auto solving in some basic arithmetic simplication
- Previous by Thread: Re: [isabelle] a question of formalization of parameterized-word (bit-vector)
- Next by Thread: Re: [isabelle] Problems on auto solving in some basic arithmetic simplication
- 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