[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.