Email Gateway (Aug 22 2022 at 14:05): Email Gateway (Aug 22 2022 at 14:05):From: Li Yongjian <lyj238@gmail.com>
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
test.thy
Email Gateway (Aug 22 2022 at 14:05):From: Simon Wimmer <wimmersimon@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
Last updated: Apr 26 2024 at 20:16 UTC