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



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
>



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