converted from DOS to UNIX format
authorpaulson
Wed Mar 30 08:33:41 2005 +0200 (2005-03-30 ago)
changeset 1563657c437b70521
parent 15635 8408a06590a6
child 15637 d2a06007ebfa
converted from DOS to UNIX format
src/HOL/ex/InductiveInvariant.thy
src/HOL/ex/InductiveInvariant_examples.thy
     1.1 --- a/src/HOL/ex/InductiveInvariant.thy	Tue Mar 29 12:30:48 2005 +0200
     1.2 +++ b/src/HOL/ex/InductiveInvariant.thy	Wed Mar 30 08:33:41 2005 +0200
     1.3 @@ -1,89 +1,89 @@
     1.4 -theory InductiveInvariant = Main:
     1.5 -
     1.6 -(** Authors: Sava Krsti\'{c} and John Matthews **)
     1.7 -(**    Date: Sep 12, 2003                      **)
     1.8 -
     1.9 -text {* A formalization of some of the results in
    1.10 -        \emph{Inductive Invariants for Nested Recursion},
    1.11 -        by Sava Krsti\'{c} and John Matthews.
    1.12 -        Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *}
    1.13 -
    1.14 -
    1.15 -text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
    1.16 -
    1.17 -constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
    1.18 -         "indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)"
    1.19 -
    1.20 -
    1.21 -text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
    1.22 -
    1.23 -constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
    1.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)"
    1.25 -
    1.26 -
    1.27 -text "The key theorem, corresponding to theorem 1 of the paper. All other results
    1.28 -      in this theory are proved using instances of this theorem, and theorems
    1.29 -      derived from this theorem."
    1.30 -
    1.31 -theorem indinv_wfrec:
    1.32 -  assumes WF:  "wf r" and
    1.33 -          INV: "indinv r S F"
    1.34 -  shows        "S x (wfrec r F x)"
    1.35 -proof (induct_tac x rule: wf_induct [OF WF])
    1.36 -  fix x
    1.37 -  assume  IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
    1.38 -  then have     "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
    1.39 -  with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
    1.40 -  thus "S x (wfrec r F x)" using WF by (simp add: wfrec)
    1.41 -qed
    1.42 -
    1.43 -theorem indinv_on_wfrec:
    1.44 -  assumes WF:  "wf r" and
    1.45 -          INV: "indinv_on r D S F" and
    1.46 -          D:   "x\<in>D"
    1.47 -  shows        "S x (wfrec r F x)"
    1.48 -apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])
    1.49 -by (simp add: indinv_on_def indinv_def)
    1.50 -
    1.51 -theorem ind_fixpoint_on_lemma:
    1.52 -  assumes WF:  "wf r" and
    1.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)
    1.54 -                               --> S x (wfrec r F x) & F f x = wfrec r F x" and
    1.55 -           D: "x\<in>D"
    1.56 -  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
    1.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])
    1.58 -  show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"
    1.59 -  proof (unfold indinv_on_def, clarify)
    1.60 -    fix f x
    1.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)"
    1.62 -    assume D': "x\<in>D"
    1.63 -    from A1 INV [THEN spec, of f, THEN bspec, OF D']
    1.64 -      have "S x (wfrec r F x)" and
    1.65 -           "F f x = wfrec r F x" by auto
    1.66 -    moreover
    1.67 -    from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto
    1.68 -    with D' INV [THEN spec, of "wfrec r F", simplified]
    1.69 -      have "F (wfrec r F) x = wfrec r F x" by blast
    1.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
    1.71 -  qed
    1.72 -qed
    1.73 -
    1.74 -theorem ind_fixpoint_lemma:
    1.75 -  assumes WF:  "wf r" and
    1.76 -         INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
    1.77 -                         --> S x (wfrec r F x) & F f x = wfrec r F x"
    1.78 -  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
    1.79 -apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])
    1.80 -by (rule INV)
    1.81 -
    1.82 -theorem tfl_indinv_wfrec:
    1.83 -"[| f == wfrec r F; wf r; indinv r S F |]
    1.84 - ==> S x (f x)"
    1.85 -by (simp add: indinv_wfrec)
    1.86 -
    1.87 -theorem tfl_indinv_on_wfrec:
    1.88 -"[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |]
    1.89 - ==> S x (f x)"
    1.90 -by (simp add: indinv_on_wfrec)
    1.91 -
    1.92 +theory InductiveInvariant = Main:
    1.93 +
    1.94 +(** Authors: Sava Krsti\'{c} and John Matthews **)
    1.95 +(**    Date: Sep 12, 2003                      **)
    1.96 +
    1.97 +text {* A formalization of some of the results in
    1.98 +        \emph{Inductive Invariants for Nested Recursion},
    1.99 +        by Sava Krsti\'{c} and John Matthews.
   1.100 +        Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *}
   1.101 +
   1.102 +
   1.103 +text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
   1.104 +
   1.105 +constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
   1.106 +         "indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)"
   1.107 +
   1.108 +
   1.109 +text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
   1.110 +
   1.111 +constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
   1.112 +         "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)"
   1.113 +
   1.114 +
   1.115 +text "The key theorem, corresponding to theorem 1 of the paper. All other results
   1.116 +      in this theory are proved using instances of this theorem, and theorems
   1.117 +      derived from this theorem."
   1.118 +
   1.119 +theorem indinv_wfrec:
   1.120 +  assumes WF:  "wf r" and
   1.121 +          INV: "indinv r S F"
   1.122 +  shows        "S x (wfrec r F x)"
   1.123 +proof (induct_tac x rule: wf_induct [OF WF])
   1.124 +  fix x
   1.125 +  assume  IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"
   1.126 +  then have     "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
   1.127 +  with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
   1.128 +  thus "S x (wfrec r F x)" using WF by (simp add: wfrec)
   1.129 +qed
   1.130 +
   1.131 +theorem indinv_on_wfrec:
   1.132 +  assumes WF:  "wf r" and
   1.133 +          INV: "indinv_on r D S F" and
   1.134 +          D:   "x\<in>D"
   1.135 +  shows        "S x (wfrec r F x)"
   1.136 +apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])
   1.137 +by (simp add: indinv_on_def indinv_def)
   1.138 +
   1.139 +theorem ind_fixpoint_on_lemma:
   1.140 +  assumes WF:  "wf r" and
   1.141 +         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)
   1.142 +                               --> S x (wfrec r F x) & F f x = wfrec r F x" and
   1.143 +           D: "x\<in>D"
   1.144 +  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
   1.145 +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])
   1.146 +  show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"
   1.147 +  proof (unfold indinv_on_def, clarify)
   1.148 +    fix f x
   1.149 +    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)"
   1.150 +    assume D': "x\<in>D"
   1.151 +    from A1 INV [THEN spec, of f, THEN bspec, OF D']
   1.152 +      have "S x (wfrec r F x)" and
   1.153 +           "F f x = wfrec r F x" by auto
   1.154 +    moreover
   1.155 +    from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto
   1.156 +    with D' INV [THEN spec, of "wfrec r F", simplified]
   1.157 +      have "F (wfrec r F) x = wfrec r F x" by blast
   1.158 +    ultimately show "F (wfrec r F) x = F f x & wfrec r F x = F f x & S x (F f x)" by auto
   1.159 +  qed
   1.160 +qed
   1.161 +
   1.162 +theorem ind_fixpoint_lemma:
   1.163 +  assumes WF:  "wf r" and
   1.164 +         INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
   1.165 +                         --> S x (wfrec r F x) & F f x = wfrec r F x"
   1.166 +  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
   1.167 +apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])
   1.168 +by (rule INV)
   1.169 +
   1.170 +theorem tfl_indinv_wfrec:
   1.171 +"[| f == wfrec r F; wf r; indinv r S F |]
   1.172 + ==> S x (f x)"
   1.173 +by (simp add: indinv_wfrec)
   1.174 +
   1.175 +theorem tfl_indinv_on_wfrec:
   1.176 +"[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |]
   1.177 + ==> S x (f x)"
   1.178 +by (simp add: indinv_on_wfrec)
   1.179 +
   1.180  end
   1.181 \ No newline at end of file
     2.1 --- a/src/HOL/ex/InductiveInvariant_examples.thy	Tue Mar 29 12:30:48 2005 +0200
     2.2 +++ b/src/HOL/ex/InductiveInvariant_examples.thy	Wed Mar 30 08:33:41 2005 +0200
     2.3 @@ -1,127 +1,127 @@
     2.4 -theory InductiveInvariant_examples = InductiveInvariant :
     2.5 -
     2.6 -(** Authors: Sava Krsti\'{c} and John Matthews **)
     2.7 -(**    Date: Oct 17, 2003                      **)
     2.8 -
     2.9 -text "A simple example showing how to use an inductive invariant
    2.10 -      to solve termination conditions generated by recdef on
    2.11 -      nested recursive function definitions."
    2.12 -
    2.13 -consts g :: "nat => nat"
    2.14 -
    2.15 -recdef (permissive) g "less_than"
    2.16 -  "g 0 = 0"
    2.17 -  "g (Suc n) = g (g n)"
    2.18 -
    2.19 -text "We can prove the unsolved termination condition for
    2.20 -      g by showing it is an inductive invariant."
    2.21 -
    2.22 -recdef_tc g_tc[simp]: g
    2.23 -apply (rule allI)
    2.24 -apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
    2.25 -apply (auto simp add: indinv_def split: nat.split)
    2.26 -apply (frule_tac x=nat in spec)
    2.27 -apply (drule_tac x="f nat" in spec)
    2.28 -by auto
    2.29 -
    2.30 -
    2.31 -text "This declaration invokes Isabelle's simplifier to
    2.32 -      remove any termination conditions before adding
    2.33 -      g's rules to the simpset."
    2.34 -declare g.simps [simplified, simp]
    2.35 -
    2.36 -
    2.37 -text "This is an example where the termination condition generated
    2.38 -      by recdef is not itself an inductive invariant."
    2.39 -
    2.40 -consts g' :: "nat => nat"
    2.41 -recdef (permissive) g' "less_than"
    2.42 -  "g' 0 = 0"
    2.43 -  "g' (Suc n) = g' n + g' (g' n)"
    2.44 -
    2.45 -thm g'.simps
    2.46 -
    2.47 -
    2.48 -text "The strengthened inductive invariant is as follows
    2.49 -      (this invariant also works for the first example above):"
    2.50 -
    2.51 -lemma g'_inv: "g' n = 0"
    2.52 -thm tfl_indinv_wfrec [OF g'_def]
    2.53 -apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
    2.54 -by (auto simp add: indinv_def split: nat.split)
    2.55 -
    2.56 -recdef_tc g'_tc[simp]: g'
    2.57 -by (simp add: g'_inv)
    2.58 -
    2.59 -text "Now we can remove the termination condition from
    2.60 -      the rules for g' ."
    2.61 -thm g'.simps [simplified]
    2.62 -
    2.63 -
    2.64 -text {* Sometimes a recursive definition is partial, that is, it
    2.65 -        is only meant to be invoked on "good" inputs. As a contrived
    2.66 -        example, we will define a new version of g that is only
    2.67 -        well defined for even inputs greater than zero. *}
    2.68 -
    2.69 -consts g_even :: "nat => nat"
    2.70 -recdef (permissive) g_even "less_than"
    2.71 -  "g_even (Suc (Suc 0)) = 3"
    2.72 -  "g_even n = g_even (g_even (n - 2) - 1)"
    2.73 -
    2.74 -
    2.75 -text "We can prove a conditional version of the unsolved termination
    2.76 -      condition for @{term g_even} by proving a stronger inductive invariant."
    2.77 -
    2.78 -lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
    2.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])
    2.80 -apply (auto simp add: indinv_on_def split: nat.split)
    2.81 -by (case_tac ka, auto)
    2.82 -
    2.83 -
    2.84 -text "Now we can prove that the second recursion equation for @{term g_even}
    2.85 -      holds, provided that n is an even number greater than two."
    2.86 -
    2.87 -theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
    2.88 -apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
    2.89 -by (auto simp add: g_even_indinv, arith)
    2.90 -
    2.91 -
    2.92 -text "McCarthy's ninety-one function. This function requires a
    2.93 -      non-standard measure to prove termination."
    2.94 -
    2.95 -consts ninety_one :: "nat => nat"
    2.96 -recdef (permissive) ninety_one "measure (%n. 101 - n)"
    2.97 -  "ninety_one x = (if 100 < x
    2.98 -                     then x - 10
    2.99 -                     else (ninety_one (ninety_one (x+11))))"
   2.100 -
   2.101 -text "To discharge the termination condition, we will prove
   2.102 -      a strengthened inductive invariant:
   2.103 -         S x y == x < y + 11"
   2.104 -
   2.105 -lemma ninety_one_inv: "n < ninety_one n + 11"
   2.106 -apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
   2.107 -apply force
   2.108 -apply (auto simp add: indinv_def measure_def inv_image_def)
   2.109 -apply (frule_tac x="x+11" in spec)
   2.110 -apply (frule_tac x="f (x + 11)" in spec)
   2.111 -by arith
   2.112 -
   2.113 -text "Proving the termination condition using the
   2.114 -      strengthened inductive invariant."
   2.115 -
   2.116 -recdef_tc ninety_one_tc[rule_format]: ninety_one
   2.117 -apply clarify
   2.118 -by (cut_tac n="x+11" in ninety_one_inv, arith)
   2.119 -
   2.120 -text "Now we can remove the termination condition from
   2.121 -      the simplification rule for @{term ninety_one}."
   2.122 -
   2.123 -theorem def_ninety_one:
   2.124 -"ninety_one x = (if 100 < x
   2.125 -                   then x - 10
   2.126 -                   else ninety_one (ninety_one (x+11)))"
   2.127 -by (subst ninety_one.simps,
   2.128 -    simp add: ninety_one_tc measure_def inv_image_def)
   2.129 -
   2.130 +theory InductiveInvariant_examples = InductiveInvariant :
   2.131 +
   2.132 +(** Authors: Sava Krsti\'{c} and John Matthews **)
   2.133 +(**    Date: Oct 17, 2003                      **)
   2.134 +
   2.135 +text "A simple example showing how to use an inductive invariant
   2.136 +      to solve termination conditions generated by recdef on
   2.137 +      nested recursive function definitions."
   2.138 +
   2.139 +consts g :: "nat => nat"
   2.140 +
   2.141 +recdef (permissive) g "less_than"
   2.142 +  "g 0 = 0"
   2.143 +  "g (Suc n) = g (g n)"
   2.144 +
   2.145 +text "We can prove the unsolved termination condition for
   2.146 +      g by showing it is an inductive invariant."
   2.147 +
   2.148 +recdef_tc g_tc[simp]: g
   2.149 +apply (rule allI)
   2.150 +apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def])
   2.151 +apply (auto simp add: indinv_def split: nat.split)
   2.152 +apply (frule_tac x=nat in spec)
   2.153 +apply (drule_tac x="f nat" in spec)
   2.154 +by auto
   2.155 +
   2.156 +
   2.157 +text "This declaration invokes Isabelle's simplifier to
   2.158 +      remove any termination conditions before adding
   2.159 +      g's rules to the simpset."
   2.160 +declare g.simps [simplified, simp]
   2.161 +
   2.162 +
   2.163 +text "This is an example where the termination condition generated
   2.164 +      by recdef is not itself an inductive invariant."
   2.165 +
   2.166 +consts g' :: "nat => nat"
   2.167 +recdef (permissive) g' "less_than"
   2.168 +  "g' 0 = 0"
   2.169 +  "g' (Suc n) = g' n + g' (g' n)"
   2.170 +
   2.171 +thm g'.simps
   2.172 +
   2.173 +
   2.174 +text "The strengthened inductive invariant is as follows
   2.175 +      (this invariant also works for the first example above):"
   2.176 +
   2.177 +lemma g'_inv: "g' n = 0"
   2.178 +thm tfl_indinv_wfrec [OF g'_def]
   2.179 +apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def])
   2.180 +by (auto simp add: indinv_def split: nat.split)
   2.181 +
   2.182 +recdef_tc g'_tc[simp]: g'
   2.183 +by (simp add: g'_inv)
   2.184 +
   2.185 +text "Now we can remove the termination condition from
   2.186 +      the rules for g' ."
   2.187 +thm g'.simps [simplified]
   2.188 +
   2.189 +
   2.190 +text {* Sometimes a recursive definition is partial, that is, it
   2.191 +        is only meant to be invoked on "good" inputs. As a contrived
   2.192 +        example, we will define a new version of g that is only
   2.193 +        well defined for even inputs greater than zero. *}
   2.194 +
   2.195 +consts g_even :: "nat => nat"
   2.196 +recdef (permissive) g_even "less_than"
   2.197 +  "g_even (Suc (Suc 0)) = 3"
   2.198 +  "g_even n = g_even (g_even (n - 2) - 1)"
   2.199 +
   2.200 +
   2.201 +text "We can prove a conditional version of the unsolved termination
   2.202 +      condition for @{term g_even} by proving a stronger inductive invariant."
   2.203 +
   2.204 +lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3"
   2.205 +apply (rule_tac D="{n. \<exists>k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def])
   2.206 +apply (auto simp add: indinv_on_def split: nat.split)
   2.207 +by (case_tac ka, auto)
   2.208 +
   2.209 +
   2.210 +text "Now we can prove that the second recursion equation for @{term g_even}
   2.211 +      holds, provided that n is an even number greater than two."
   2.212 +
   2.213 +theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)"
   2.214 +apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)")
   2.215 +by (auto simp add: g_even_indinv, arith)
   2.216 +
   2.217 +
   2.218 +text "McCarthy's ninety-one function. This function requires a
   2.219 +      non-standard measure to prove termination."
   2.220 +
   2.221 +consts ninety_one :: "nat => nat"
   2.222 +recdef (permissive) ninety_one "measure (%n. 101 - n)"
   2.223 +  "ninety_one x = (if 100 < x
   2.224 +                     then x - 10
   2.225 +                     else (ninety_one (ninety_one (x+11))))"
   2.226 +
   2.227 +text "To discharge the termination condition, we will prove
   2.228 +      a strengthened inductive invariant:
   2.229 +         S x y == x < y + 11"
   2.230 +
   2.231 +lemma ninety_one_inv: "n < ninety_one n + 11"
   2.232 +apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
   2.233 +apply force
   2.234 +apply (auto simp add: indinv_def measure_def inv_image_def)
   2.235 +apply (frule_tac x="x+11" in spec)
   2.236 +apply (frule_tac x="f (x + 11)" in spec)
   2.237 +by arith
   2.238 +
   2.239 +text "Proving the termination condition using the
   2.240 +      strengthened inductive invariant."
   2.241 +
   2.242 +recdef_tc ninety_one_tc[rule_format]: ninety_one
   2.243 +apply clarify
   2.244 +by (cut_tac n="x+11" in ninety_one_inv, arith)
   2.245 +
   2.246 +text "Now we can remove the termination condition from
   2.247 +      the simplification rule for @{term ninety_one}."
   2.248 +
   2.249 +theorem def_ninety_one:
   2.250 +"ninety_one x = (if 100 < x
   2.251 +                   then x - 10
   2.252 +                   else ninety_one (ninety_one (x+11)))"
   2.253 +by (subst ninety_one.simps,
   2.254 +    simp add: ninety_one_tc measure_def inv_image_def)
   2.255 +
   2.256  end
   2.257 \ No newline at end of file