summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/InductiveInvariant.thy

author | nipkow |

Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) | |

changeset 30313 | b2441b0c8d38 |

parent 21404 | eb85850d3eb7 |

child 32960 | 69916a850301 |

permissions | -rw-r--r-- |

added lemmas

1 (* ID: $Id$

2 Author: Sava Krsti\'{c} and John Matthews

3 *)

5 header {* Some of the results in Inductive Invariants for Nested Recursion *}

7 theory InductiveInvariant imports Main begin

9 text {* A formalization of some of the results in \emph{Inductive

10 Invariants for Nested Recursion}, by Sava Krsti\'{c} and John

11 Matthews. Appears in the proceedings of TPHOLs 2003, LNCS

12 vol. 2758, pp. 253-269. *}

15 text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."

17 definition

18 indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where

19 "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"

22 text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."

24 definition

25 indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where

26 "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))"

29 text "The key theorem, corresponding to theorem 1 of the paper. All other results

30 in this theory are proved using instances of this theorem, and theorems

31 derived from this theorem."

33 theorem indinv_wfrec:

34 assumes wf: "wf r" and

35 inv: "indinv r S F"

36 shows "S x (wfrec r F x)"

37 using wf

38 proof (induct x)

39 fix x

40 assume IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"

41 then have "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)

42 with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)

43 thus "S x (wfrec r F x)" using wf by (simp add: wfrec)

44 qed

46 theorem indinv_on_wfrec:

47 assumes WF: "wf r" and

48 INV: "indinv_on r D S F" and

49 D: "x\<in>D"

50 shows "S x (wfrec r F x)"

51 apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])

52 by (simp add: indinv_on_def indinv_def)

54 theorem ind_fixpoint_on_lemma:

55 assumes WF: "wf r" and

56 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)

57 --> S x (wfrec r F x) & F f x = wfrec r F x" and

58 D: "x\<in>D"

59 shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"

60 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])

61 show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"

62 proof (unfold indinv_on_def, clarify)

63 fix f x

64 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)"

65 assume D': "x\<in>D"

66 from A1 INV [THEN spec, of f, THEN bspec, OF D']

67 have "S x (wfrec r F x)" and

68 "F f x = wfrec r F x" by auto

69 moreover

70 from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto

71 with D' INV [THEN spec, of "wfrec r F", simplified]

72 have "F (wfrec r F) x = wfrec r F x" by blast

73 ultimately show "F (wfrec r F) x = F f x & wfrec r F x = F f x & S x (F f x)" by auto

74 qed

75 qed

77 theorem ind_fixpoint_lemma:

78 assumes WF: "wf r" and

79 INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)

80 --> S x (wfrec r F x) & F f x = wfrec r F x"

81 shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"

82 apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])

83 by (rule INV)

85 theorem tfl_indinv_wfrec:

86 "[| f == wfrec r F; wf r; indinv r S F |]

87 ==> S x (f x)"

88 by (simp add: indinv_wfrec)

90 theorem tfl_indinv_on_wfrec:

91 "[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |]

92 ==> S x (f x)"

93 by (simp add: indinv_on_wfrec)

95 end