[isabelle] Base case in termination proof..
I have the following function:
function (domintros) index:: "int â int" where
"index a = (if (a<0) then (index (a+5)) else (a mod 5))"
and have been trying to prove the result is always >=0 and <= 4. Ran
into a bit of trouble and after some investigation found that it was
because Isabelle couldn't automatically prove termination..
The intention is to prove that this condition is true for all ints, so I
need to prove "â a. index_dom a".
Print_theorems gives the following:
index.cases: (âa. ?x = a â ?P) â ?P
index.domintros: (?a < 0 â index_dom (?a + 5)) â index_dom ?a
index.pelims: index ?x = ?y â index_dom ?x â (âa. ?x = a â ?y = (if a
< 0 then index (a + 5) else a mod 5) â index_dom a â ?P) â ?P
index.pinduct: index_dom ?a0.0 â (âa. index_dom a â (a < 0 â ?P (a +
5)) â ?P a) â ?P ?a0.0
index.psimps: index_dom ?a â index ?a = (if ?a < 0 then index (?a +
5) else ?a mod 5)
with which I've managed to prove this inductive rule:
lemma ddda: "index_dom a â index_dom (a-5)"
apply(induction a rule:index.pinduct)
Which is well and good for negative numbers as long as I have an
appropriate base case. I'd been thinking of doing
1: index_dom (a) /\ a<5 /\ a>=0 as a base case. Can do for each
individual value of a, as it's a small enough range
2: index_dom a â index_dom (a-5) to extend over negative numbers
3: a >= 0 ==> index_dom a ==> index_dom a+5 to extend over positives
using cyclic nature of mod operation.
The problem is that I don't see any way in the theorems that mention
index_dom that I could establish index_dom 0, for example.
I can assume it and succeed in calculating the result - which would be
sufficient to prove to a human that it terminates for that value, but I
don't know how I'd mechanise that reasoning.
This archive was generated by a fusion of
Pipermail (Mailman edition) and