Up to index of Isabelle/HOL/ex
theory InductiveInvariant_examples(* ID: $Id: InductiveInvariant_examples.thy,v 1.4 2005/09/14 20:08:08 wenzelm Exp $ Author: Sava Krsti\'{c} and John Matthews *) header {* Example use if an inductive invariant to solve termination conditions *} theory InductiveInvariant_examples imports InductiveInvariant begin text "A simple example showing how to use an inductive invariant to solve termination conditions generated by recdef on nested recursive function definitions." consts g :: "nat => nat" recdef (permissive) g "less_than" "g 0 = 0" "g (Suc n) = g (g n)" text "We can prove the unsolved termination condition for g by showing it is an inductive invariant." recdef_tc g_tc[simp]: g apply (rule allI) apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def]) apply (auto simp add: indinv_def split: nat.split) apply (frule_tac x=nat in spec) apply (drule_tac x="f nat" in spec) by auto text "This declaration invokes Isabelle's simplifier to remove any termination conditions before adding g's rules to the simpset." declare g.simps [simplified, simp] text "This is an example where the termination condition generated by recdef is not itself an inductive invariant." consts g' :: "nat => nat" recdef (permissive) g' "less_than" "g' 0 = 0" "g' (Suc n) = g' n + g' (g' n)" thm g'.simps text "The strengthened inductive invariant is as follows (this invariant also works for the first example above):" lemma g'_inv: "g' n = 0" thm tfl_indinv_wfrec [OF g'_def] apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def]) by (auto simp add: indinv_def split: nat.split) recdef_tc g'_tc[simp]: g' by (simp add: g'_inv) text "Now we can remove the termination condition from the rules for g' ." thm g'.simps [simplified] text {* Sometimes a recursive definition is partial, that is, it is only meant to be invoked on "good" inputs. As a contrived example, we will define a new version of g that is only well defined for even inputs greater than zero. *} consts g_even :: "nat => nat" recdef (permissive) g_even "less_than" "g_even (Suc (Suc 0)) = 3" "g_even n = g_even (g_even (n - 2) - 1)" text "We can prove a conditional version of the unsolved termination condition for @{term g_even} by proving a stronger inductive invariant." lemma g_even_indinv: "∃k. n = Suc (Suc (2*k)) ==> g_even n = 3" apply (rule_tac D="{n. ∃k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def]) apply (auto simp add: indinv_on_def split: nat.split) by (case_tac ka, auto) text "Now we can prove that the second recursion equation for @{term g_even} holds, provided that n is an even number greater than two." theorem g_even_n: "∃k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)" apply (subgoal_tac "(∃k. n - 2 = 2*k + 2) & (∃k. n = 2*k + 2)") by (auto simp add: g_even_indinv, arith) text "McCarthy's ninety-one function. This function requires a non-standard measure to prove termination." consts ninety_one :: "nat => nat" recdef (permissive) ninety_one "measure (%n. 101 - n)" "ninety_one x = (if 100 < x then x - 10 else (ninety_one (ninety_one (x+11))))" text "To discharge the termination condition, we will prove a strengthened inductive invariant: S x y == x < y + 11" lemma ninety_one_inv: "n < ninety_one n + 11" apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def]) apply force apply (auto simp add: indinv_def measure_def inv_image_def) apply (frule_tac x="x+11" in spec) apply (frule_tac x="f (x + 11)" in spec) by arith text "Proving the termination condition using the strengthened inductive invariant." recdef_tc ninety_one_tc[rule_format]: ninety_one apply clarify by (cut_tac n="x+11" in ninety_one_inv, arith) text "Now we can remove the termination condition from the simplification rule for @{term ninety_one}." theorem def_ninety_one: "ninety_one x = (if 100 < x then x - 10 else ninety_one (ninety_one (x+11)))" by (subst ninety_one.simps, simp add: ninety_one_tc measure_def inv_image_def) end
lemma g'_inv:
g' n = 0
lemma g_even_indinv:
∃k. n = Suc (Suc (2 * k)) ==> g_even n = 3
theorem g_even_n:
∃k. n = 2 * k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)
lemma ninety_one_inv:
n < ninety_one n + 11
theorem def_ninety_one:
ninety_one x = (if 100 < x then x - 10 else ninety_one (ninety_one (x + 11)))