InductiveInvariant_examples illustrates advanced recursive function definitions
authorpaulson
Wed Oct 22 10:52:36 2003 +0200 (2003-10-22)
changeset 14244f58598341d30
parent 14243 0e2ec694784d
child 14245 c0272df4775b
InductiveInvariant_examples illustrates advanced recursive function definitions
src/HOL/IsaMakefile
src/HOL/ex/InductiveInvariant.thy
src/HOL/ex/InductiveInvariant_examples.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Recdefs.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Oct 22 10:51:30 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Oct 22 10:52:36 2003 +0200
     1.3 @@ -586,6 +586,7 @@
     1.4  $(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.ML ex/AVL.thy ex/Antiquote.thy \
     1.5    ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
     1.6    ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
     1.7 +  ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
     1.8    ex/IntRing.thy ex/Intuitionistic.thy \
     1.9    ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
    1.10    ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/InductiveInvariant.thy	Wed Oct 22 10:52:36 2003 +0200
     2.3 @@ -0,0 +1,89 @@
     2.4 +theory InductiveInvariant = Main:
     2.5 +
     2.6 +(** Authors: Sava Krsti\'{c} and John Matthews **)
     2.7 +(**    Date: Sep 12, 2003                      **)
     2.8 +
     2.9 +text {* A formalization of some of the results in
    2.10 +        \emph{Inductive Invariants for Nested Recursion},
    2.11 +        by Sava Krsti\'{c} and John Matthews.
    2.12 +        Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *}
    2.13 +
    2.14 +
    2.15 +text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
    2.16 +
    2.17 +constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
    2.18 +         "indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)"
    2.19 +
    2.20 +
    2.21 +text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
    2.22 +
    2.23 +constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
    2.24 +         "indinv_on r D S F == \<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (f y)) --> S x (F f x)"
    2.25 +
    2.26 +
    2.27 +text "The key theorem, corresponding to theorem 1 of the paper. All other results
    2.28 +      in this theory are proved using instances of this theorem, and theorems
    2.29 +      derived from this theorem."
    2.30 +
    2.31 +theorem indinv_wfrec:
    2.32 +  assumes WF:  "wf r" and
    2.33 +          INV: "indinv r S F"
    2.34 +  shows        "S x (wfrec r F x)"
    2.35 +proof (induct_tac x rule: wf_induct [OF WF])
    2.36 +  fix x
    2.37 +  assume  IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
    2.38 +  then have     "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
    2.39 +  with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
    2.40 +  thus "S x (wfrec r F x)" using WF by (simp add: wfrec)
    2.41 +qed
    2.42 +
    2.43 +theorem indinv_on_wfrec:
    2.44 +  assumes WF:  "wf r" and
    2.45 +          INV: "indinv_on r D S F" and
    2.46 +          D:   "x\<in>D"
    2.47 +  shows        "S x (wfrec r F x)"
    2.48 +apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])
    2.49 +by (simp add: indinv_on_def indinv_def)
    2.50 +
    2.51 +theorem ind_fixpoint_on_lemma:
    2.52 +  assumes WF:  "wf r" and
    2.53 +         INV: "\<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
    2.54 +                               --> S x (wfrec r F x) & F f x = wfrec r F x" and
    2.55 +           D: "x\<in>D"
    2.56 +  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
    2.57 +proof (rule indinv_on_wfrec [OF WF _ D, of "% a b. F (wfrec r F) a = b & wfrec r F a = b & S a b" F, simplified])
    2.58 +  show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"
    2.59 +  proof (unfold indinv_on_def, clarify)
    2.60 +    fix f x
    2.61 +    assume A1: "\<forall>y\<in>D. (y, x) \<in> r --> F (wfrec r F) y = f y & wfrec r F y = f y & S y (f y)"
    2.62 +    assume D': "x\<in>D"
    2.63 +    from A1 INV [THEN spec, of f, THEN bspec, OF D']
    2.64 +      have "S x (wfrec r F x)" and
    2.65 +           "F f x = wfrec r F x" by auto
    2.66 +    moreover
    2.67 +    from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto
    2.68 +    with D' INV [THEN spec, of "wfrec r F", simplified]
    2.69 +      have "F (wfrec r F) x = wfrec r F x" by blast
    2.70 +    ultimately show "F (wfrec r F) x = F f x & wfrec r F x = F f x & S x (F f x)" by auto
    2.71 +  qed
    2.72 +qed
    2.73 +
    2.74 +theorem ind_fixpoint_lemma:
    2.75 +  assumes WF:  "wf r" and
    2.76 +         INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
    2.77 +                         --> S x (wfrec r F x) & F f x = wfrec r F x"
    2.78 +  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
    2.79 +apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])
    2.80 +by (rule INV)
    2.81 +
    2.82 +theorem tfl_indinv_wfrec:
    2.83 +"[| f == wfrec r F; wf r; indinv r S F |]
    2.84 + ==> S x (f x)"
    2.85 +by (simp add: indinv_wfrec)
    2.86 +
    2.87 +theorem tfl_indinv_on_wfrec:
    2.88 +"[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |]
    2.89 + ==> S x (f x)"
    2.90 +by (simp add: indinv_on_wfrec)
    2.91 +
    2.92 +end
    2.93 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/InductiveInvariant_examples.thy	Wed Oct 22 10:52:36 2003 +0200
     3.3 @@ -0,0 +1,127 @@
     3.4 +theory InductiveInvariant_examples = InductiveInvariant :
     3.5 +
     3.6 +(** Authors: Sava Krsti\'{c} and John Matthews **)
     3.7 +(**    Date: Oct 17, 2003                      **)
     3.8 +
     3.9 +text "A simple example showing how to use an inductive invariant
    3.10 +      to solve termination conditions generated by recdef on
    3.11 +      nested recursive function definitions."
    3.12 +
    3.13 +consts g :: "nat => nat"
    3.14 +
    3.15 +recdef (permissive) g "less_than"
    3.16 +  "g 0 = 0"
    3.17 +  "g (Suc n) = g (g n)"
    3.18 +
    3.19 +text "We can prove the unsolved termination condition for
    3.20 +      g by showing it is an inductive invariant."
    3.21 +
    3.22 +recdef_tc g_tc[simp]: g
    3.23 +apply (rule allI)
    3.24 +apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
    3.25 +apply (auto simp add: indinv_def split: nat.split)
    3.26 +apply (frule_tac x=nat in spec)
    3.27 +apply (drule_tac x="f nat" in spec)
    3.28 +by auto
    3.29 +
    3.30 +
    3.31 +text "This declaration invokes Isabelle's simplifier to
    3.32 +      remove any termination conditions before adding
    3.33 +      g's rules to the simpset."
    3.34 +declare g.simps [simplified, simp]
    3.35 +
    3.36 +
    3.37 +text "This is an example where the termination condition generated
    3.38 +      by recdef is not itself an inductive invariant."
    3.39 +
    3.40 +consts g' :: "nat => nat"
    3.41 +recdef (permissive) g' "less_than"
    3.42 +  "g' 0 = 0"
    3.43 +  "g' (Suc n) = g' n + g' (g' n)"
    3.44 +
    3.45 +thm g'.simps
    3.46 +
    3.47 +
    3.48 +text "The strengthened inductive invariant is as follows
    3.49 +      (this invariant also works for the first example above):"
    3.50 +
    3.51 +lemma g'_inv: "g' n = 0"
    3.52 +thm tfl_indinv_wfrec [OF g'_def]
    3.53 +apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
    3.54 +by (auto simp add: indinv_def split: nat.split)
    3.55 +
    3.56 +recdef_tc g'_tc[simp]: g'
    3.57 +by (simp add: g'_inv)
    3.58 +
    3.59 +text "Now we can remove the termination condition from
    3.60 +      the rules for g' ."
    3.61 +thm g'.simps [simplified]
    3.62 +
    3.63 +
    3.64 +text {* Sometimes a recursive definition is partial, that is, it
    3.65 +        is only meant to be invoked on "good" inputs. As a contrived
    3.66 +        example, we will define a new version of g that is only
    3.67 +        well defined for even inputs greater than zero. *}
    3.68 +
    3.69 +consts g_even :: "nat => nat"
    3.70 +recdef (permissive) g_even "less_than"
    3.71 +  "g_even (Suc (Suc 0)) = 3"
    3.72 +  "g_even n = g_even (g_even (n - 2) - 1)"
    3.73 +
    3.74 +
    3.75 +text "We can prove a conditional version of the unsolved termination
    3.76 +      condition for @{term g_even} by proving a stronger inductive invariant."
    3.77 +
    3.78 +lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
    3.79 +apply (rule_tac D="{n. \<exists>k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def])
    3.80 +apply (auto simp add: indinv_on_def split: nat.split)
    3.81 +by (case_tac ka, auto)
    3.82 +
    3.83 +
    3.84 +text "Now we can prove that the second recursion equation for @{term g_even}
    3.85 +      holds, provided that n is an even number greater than two."
    3.86 +
    3.87 +theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
    3.88 +apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
    3.89 +by (auto simp add: g_even_indinv, arith)
    3.90 +
    3.91 +
    3.92 +text "McCarthy's ninety-one function. This function requires a
    3.93 +      non-standard measure to prove termination."
    3.94 +
    3.95 +consts ninety_one :: "nat => nat"
    3.96 +recdef (permissive) ninety_one "measure (%n. 101 - n)"
    3.97 +  "ninety_one x = (if 100 < x
    3.98 +                     then x - 10
    3.99 +                     else (ninety_one (ninety_one (x+11))))"
   3.100 +
   3.101 +text "To discharge the termination condition, we will prove
   3.102 +      a strengthened inductive invariant:
   3.103 +         S x y == x < y + 11"
   3.104 +
   3.105 +lemma ninety_one_inv: "n < ninety_one n + 11"
   3.106 +apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
   3.107 +apply force
   3.108 +apply (auto simp add: indinv_def measure_def inv_image_def)
   3.109 +apply (frule_tac x="x+11" in spec)
   3.110 +apply (frule_tac x="f (x + 11)" in spec)
   3.111 +by arith
   3.112 +
   3.113 +text "Proving the termination condition using the
   3.114 +      strengthened inductive invariant."
   3.115 +
   3.116 +recdef_tc ninety_one_tc[rule_format]: ninety_one
   3.117 +apply clarify
   3.118 +by (cut_tac n="x+11" in ninety_one_inv, arith)
   3.119 +
   3.120 +text "Now we can remove the termination condition from
   3.121 +      the simplification rule for @{term ninety_one}."
   3.122 +
   3.123 +theorem def_ninety_one:
   3.124 +"ninety_one x = (if 100 < x
   3.125 +                   then x - 10
   3.126 +                   else ninety_one (ninety_one (x+11)))"
   3.127 +by (subst ninety_one.simps,
   3.128 +    simp add: ninety_one_tc measure_def inv_image_def)
   3.129 +
   3.130 +end
   3.131 \ No newline at end of file
     4.1 --- a/src/HOL/ex/ROOT.ML	Wed Oct 22 10:51:30 2003 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Wed Oct 22 10:52:36 2003 +0200
     4.3 @@ -7,6 +7,7 @@
     4.4  time_use_thy "Higher_Order_Logic";
     4.5  
     4.6  time_use_thy "Recdefs";
     4.7 +time_use_thy "InductiveInvariant_examples";
     4.8  time_use_thy "Primrec";
     4.9  time_use_thy "Locales";
    4.10  time_use_thy "Records";
     5.1 --- a/src/HOL/ex/Recdefs.thy	Wed Oct 22 10:51:30 2003 +0200
     5.2 +++ b/src/HOL/ex/Recdefs.thy	Wed Oct 22 10:52:36 2003 +0200
     5.3 @@ -33,7 +33,7 @@
     5.4  
     5.5  text {* Not handled automatically: too complicated. *}
     5.6  consts variant :: "nat * nat list => nat"
     5.7 -recdef (permissive) variant  "measure (\<lambda>(n::nat, ns). size (filter (\<lambda>y. n \<le> y) ns))"
     5.8 +recdef (permissive) variant "measure (\<lambda>(n,ns). size (filter (\<lambda>y. n \<le> y) ns))"
     5.9    "variant (x, L) = (if x mem L then variant (Suc x, L) else x)"
    5.10  
    5.11  consts gcd :: "nat * nat => nat"