[isabelle] Problems on auto solving in some basic arithmetic simplication



 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
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.