src/HOL/ex/InductiveInvariant_examples.thy
 author paulson Wed Oct 22 10:52:36 2003 +0200 (2003-10-22) changeset 14244 f58598341d30 child 15636 57c437b70521 permissions -rw-r--r--
InductiveInvariant_examples illustrates advanced recursive function definitions
 paulson@14244 ` 1` ```theory InductiveInvariant_examples = InductiveInvariant : ``` paulson@14244 ` 2` paulson@14244 ` 3` ```(** Authors: Sava Krsti\'{c} and John Matthews **) ``` paulson@14244 ` 4` ```(** Date: Oct 17, 2003 **) ``` paulson@14244 ` 5` paulson@14244 ` 6` ```text "A simple example showing how to use an inductive invariant ``` paulson@14244 ` 7` ``` to solve termination conditions generated by recdef on ``` paulson@14244 ` 8` ``` nested recursive function definitions." ``` paulson@14244 ` 9` paulson@14244 ` 10` ```consts g :: "nat => nat" ``` paulson@14244 ` 11` paulson@14244 ` 12` ```recdef (permissive) g "less_than" ``` paulson@14244 ` 13` ``` "g 0 = 0" ``` paulson@14244 ` 14` ``` "g (Suc n) = g (g n)" ``` paulson@14244 ` 15` paulson@14244 ` 16` ```text "We can prove the unsolved termination condition for ``` paulson@14244 ` 17` ``` g by showing it is an inductive invariant." ``` paulson@14244 ` 18` paulson@14244 ` 19` ```recdef_tc g_tc[simp]: g ``` paulson@14244 ` 20` ```apply (rule allI) ``` paulson@14244 ` 21` ```apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def]) ``` paulson@14244 ` 22` ```apply (auto simp add: indinv_def split: nat.split) ``` paulson@14244 ` 23` ```apply (frule_tac x=nat in spec) ``` paulson@14244 ` 24` ```apply (drule_tac x="f nat" in spec) ``` paulson@14244 ` 25` ```by auto ``` paulson@14244 ` 26` paulson@14244 ` 27` paulson@14244 ` 28` ```text "This declaration invokes Isabelle's simplifier to ``` paulson@14244 ` 29` ``` remove any termination conditions before adding ``` paulson@14244 ` 30` ``` g's rules to the simpset." ``` paulson@14244 ` 31` ```declare g.simps [simplified, simp] ``` paulson@14244 ` 32` paulson@14244 ` 33` paulson@14244 ` 34` ```text "This is an example where the termination condition generated ``` paulson@14244 ` 35` ``` by recdef is not itself an inductive invariant." ``` paulson@14244 ` 36` paulson@14244 ` 37` ```consts g' :: "nat => nat" ``` paulson@14244 ` 38` ```recdef (permissive) g' "less_than" ``` paulson@14244 ` 39` ``` "g' 0 = 0" ``` paulson@14244 ` 40` ``` "g' (Suc n) = g' n + g' (g' n)" ``` paulson@14244 ` 41` paulson@14244 ` 42` ```thm g'.simps ``` paulson@14244 ` 43` paulson@14244 ` 44` paulson@14244 ` 45` ```text "The strengthened inductive invariant is as follows ``` paulson@14244 ` 46` ``` (this invariant also works for the first example above):" ``` paulson@14244 ` 47` paulson@14244 ` 48` ```lemma g'_inv: "g' n = 0" ``` paulson@14244 ` 49` ```thm tfl_indinv_wfrec [OF g'_def] ``` paulson@14244 ` 50` ```apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def]) ``` paulson@14244 ` 51` ```by (auto simp add: indinv_def split: nat.split) ``` paulson@14244 ` 52` paulson@14244 ` 53` ```recdef_tc g'_tc[simp]: g' ``` paulson@14244 ` 54` ```by (simp add: g'_inv) ``` paulson@14244 ` 55` paulson@14244 ` 56` ```text "Now we can remove the termination condition from ``` paulson@14244 ` 57` ``` the rules for g' ." ``` paulson@14244 ` 58` ```thm g'.simps [simplified] ``` paulson@14244 ` 59` paulson@14244 ` 60` paulson@14244 ` 61` ```text {* Sometimes a recursive definition is partial, that is, it ``` paulson@14244 ` 62` ``` is only meant to be invoked on "good" inputs. As a contrived ``` paulson@14244 ` 63` ``` example, we will define a new version of g that is only ``` paulson@14244 ` 64` ``` well defined for even inputs greater than zero. *} ``` paulson@14244 ` 65` paulson@14244 ` 66` ```consts g_even :: "nat => nat" ``` paulson@14244 ` 67` ```recdef (permissive) g_even "less_than" ``` paulson@14244 ` 68` ``` "g_even (Suc (Suc 0)) = 3" ``` paulson@14244 ` 69` ``` "g_even n = g_even (g_even (n - 2) - 1)" ``` paulson@14244 ` 70` paulson@14244 ` 71` paulson@14244 ` 72` ```text "We can prove a conditional version of the unsolved termination ``` paulson@14244 ` 73` ``` condition for @{term g_even} by proving a stronger inductive invariant." ``` paulson@14244 ` 74` paulson@14244 ` 75` ```lemma g_even_indinv: "\k. n = Suc (Suc (2*k)) ==> g_even n = 3" ``` paulson@14244 ` 76` ```apply (rule_tac D="{n. \k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def]) ``` paulson@14244 ` 77` ```apply (auto simp add: indinv_on_def split: nat.split) ``` paulson@14244 ` 78` ```by (case_tac ka, auto) ``` paulson@14244 ` 79` paulson@14244 ` 80` paulson@14244 ` 81` ```text "Now we can prove that the second recursion equation for @{term g_even} ``` paulson@14244 ` 82` ``` holds, provided that n is an even number greater than two." ``` paulson@14244 ` 83` paulson@14244 ` 84` ```theorem g_even_n: "\k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)" ``` paulson@14244 ` 85` ```apply (subgoal_tac "(\k. n - 2 = 2*k + 2) & (\k. n = 2*k + 2)") ``` paulson@14244 ` 86` ```by (auto simp add: g_even_indinv, arith) ``` paulson@14244 ` 87` paulson@14244 ` 88` paulson@14244 ` 89` ```text "McCarthy's ninety-one function. This function requires a ``` paulson@14244 ` 90` ``` non-standard measure to prove termination." ``` paulson@14244 ` 91` paulson@14244 ` 92` ```consts ninety_one :: "nat => nat" ``` paulson@14244 ` 93` ```recdef (permissive) ninety_one "measure (%n. 101 - n)" ``` paulson@14244 ` 94` ``` "ninety_one x = (if 100 < x ``` paulson@14244 ` 95` ``` then x - 10 ``` paulson@14244 ` 96` ``` else (ninety_one (ninety_one (x+11))))" ``` paulson@14244 ` 97` paulson@14244 ` 98` ```text "To discharge the termination condition, we will prove ``` paulson@14244 ` 99` ``` a strengthened inductive invariant: ``` paulson@14244 ` 100` ``` S x y == x < y + 11" ``` paulson@14244 ` 101` paulson@14244 ` 102` ```lemma ninety_one_inv: "n < ninety_one n + 11" ``` paulson@14244 ` 103` ```apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def]) ``` paulson@14244 ` 104` ```apply force ``` paulson@14244 ` 105` ```apply (auto simp add: indinv_def measure_def inv_image_def) ``` paulson@14244 ` 106` ```apply (frule_tac x="x+11" in spec) ``` paulson@14244 ` 107` ```apply (frule_tac x="f (x + 11)" in spec) ``` paulson@14244 ` 108` ```by arith ``` paulson@14244 ` 109` paulson@14244 ` 110` ```text "Proving the termination condition using the ``` paulson@14244 ` 111` ``` strengthened inductive invariant." ``` paulson@14244 ` 112` paulson@14244 ` 113` ```recdef_tc ninety_one_tc[rule_format]: ninety_one ``` paulson@14244 ` 114` ```apply clarify ``` paulson@14244 ` 115` ```by (cut_tac n="x+11" in ninety_one_inv, arith) ``` paulson@14244 ` 116` paulson@14244 ` 117` ```text "Now we can remove the termination condition from ``` paulson@14244 ` 118` ``` the simplification rule for @{term ninety_one}." ``` paulson@14244 ` 119` paulson@14244 ` 120` ```theorem def_ninety_one: ``` paulson@14244 ` 121` ```"ninety_one x = (if 100 < x ``` paulson@14244 ` 122` ``` then x - 10 ``` paulson@14244 ` 123` ``` else ninety_one (ninety_one (x+11)))" ``` paulson@14244 ` 124` ```by (subst ninety_one.simps, ``` paulson@14244 ` 125` ``` simp add: ninety_one_tc measure_def inv_image_def) ``` paulson@14244 ` 126` paulson@14244 ` 127` `end`