src/HOL/ex/InductiveInvariant.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 17388 495c799df31d child 19736 d8d0f8f51d69 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  ID:         $Id$

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

     3 *)

     4

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

     6

     7 theory InductiveInvariant imports Main begin

     8

     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. *}

    13

    14

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

    16

    17 constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"

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

    19

    20

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

    22

    23 constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"

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

    25

    26

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

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

    29       derived from this theorem."

    30

    31 theorem indinv_wfrec:

    32   assumes WF:  "wf r" and

    33           INV: "indinv r S F"

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

    35 proof (induct_tac x rule: wf_induct [OF WF])

    36   fix x

    37   assume  IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)"

    38   then have     "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)

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

    40   thus "S x (wfrec r F x)" using WF by (simp add: wfrec)

    41 qed

    42

    43 theorem indinv_on_wfrec:

    44   assumes WF:  "wf r" and

    45           INV: "indinv_on r D S F" and

    46           D:   "x\<in>D"

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

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

    49 by (simp add: indinv_on_def indinv_def)

    50

    51 theorem ind_fixpoint_on_lemma:

    52   assumes WF:  "wf r" and

    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)

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

    55            D: "x\<in>D"

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

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

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

    59   proof (unfold indinv_on_def, clarify)

    60     fix f x

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

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

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

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

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

    66     moreover

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

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

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

    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

    71   qed

    72 qed

    73

    74 theorem ind_fixpoint_lemma:

    75   assumes WF:  "wf r" and

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

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

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

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

    80 by (rule INV)

    81

    82 theorem tfl_indinv_wfrec:

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

    84  ==> S x (f x)"

    85 by (simp add: indinv_wfrec)

    86

    87 theorem tfl_indinv_on_wfrec:

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

    89  ==> S x (f x)"

    90 by (simp add: indinv_on_wfrec)

    91

    92 end