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 *)
     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 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))"
    20 
    21 
    22 text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
    23 
    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))"
    27 
    28 
    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."
    32 
    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
    45 
    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)
    53 
    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
    76 
    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)
    84 
    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)
    89 
    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)
    94 
    95 end