Email Gateway (Aug 22 2022 at 16:05): Email Gateway (Aug 22 2022 at 16:05):From: Cristina Matache <cristina@aestheticintegration.com>
Dear Isabelle users,
I need to prove some arithmetic rewritings and I'm trying to write an
Eisbach "method" to do this.
A simple example of something I need to prove is:
notepad
begin
fix rr :: real
assume assm: "¬ rr < 0 ∧ ¬ rr * (3 + rr * (5 / 2)) / (3 + rr * (4 + rr))
< rr * 2 / (2 + rr) ∧ ¬ rr ≤ - 1"
then have "¬ rr < 0 ∧ ¬ (- 1 / 2 + (1 + rr) * (- 2 + (1 + rr) * (5 / 2)))
/ ((1 + rr) * (2 + (1 + rr))) < rr * 2 / (2 + rr) ∧ ¬ 1 + rr ≤ 0"
apply (simp add: divide_simps split: if_splits)
apply sos+
done
end
The strategy is to eliminate division from the polynomials using "simp",
and then solve the resulting subgoals by "sos" (Sum_of_Squares).
I tried combining the two proof steps above in the Eisbach method:
method mt_arith = ((simp add: divide_simps split: if_splits); sos)
but this method fails. I'm not sure why this doesn't behave the same as the
two proof steps above; I think I'm misunderstanding how ";" works.
The Isabelle reference manual says:
"Structural composition “m 1 ; m 2 ” means that method m 1 is applied with
restriction to the first subgoal, then m 2 is applied consecutively with
restriction to each subgoal that has newly emerged due to m 1 ."
So is it not the case that "sos" will be applied in turn to all three
subgoals resulting from "simp"?
What is the correct way to translate this proof to an Eisbach "method"?
Thanks,
Cristina Matache
Email Gateway (Aug 22 2022 at 16:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Cristina,
The combinator ";" does not change the facts that are chained in (via then/using), and in
your example, the sos method chokes on the "assm" that is fed into the goal, probably
because it still contains divisions. You can change the chaining locally with the method
transformer "use", as in
method mt_arith = (simp add: divide_simps split: if_splits; use nothing in sos)
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 16:06):From: Cristina Matache <cristina@aestheticintegration.com>
Dear Andreas,
Thank you for the suggestion. This works perfectly.
Best wishes,
Cristina
Last updated: Apr 25 2024 at 12:23 UTC