# [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)
apply(simp add:index.domintros)
done

`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.
`
Any clues?
--
DH

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