src/HOL/ex/InductiveInvariant.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 21404 eb85850d3eb7
child 32960 69916a850301
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
wenzelm@17388
     1
(*  ID:         $Id$
wenzelm@17388
     2
    Author:	Sava Krsti\'{c} and John Matthews
wenzelm@17388
     3
*)
wenzelm@17388
     4
wenzelm@17388
     5
header {* Some of the results in Inductive Invariants for Nested Recursion *}
wenzelm@17388
     6
haftmann@16417
     7
theory InductiveInvariant imports Main begin
paulson@15636
     8
wenzelm@17388
     9
text {* A formalization of some of the results in \emph{Inductive
wenzelm@17388
    10
  Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
wenzelm@17388
    11
  Matthews.  Appears in the proceedings of TPHOLs 2003, LNCS
wenzelm@17388
    12
  vol. 2758, pp. 253-269. *}
paulson@15636
    13
paulson@15636
    14
paulson@15636
    15
text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
paulson@15636
    16
wenzelm@19736
    17
definition
wenzelm@21404
    18
  indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
wenzelm@19736
    19
  "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"
paulson@15636
    20
paulson@15636
    21
paulson@15636
    22
text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
paulson@15636
    23
wenzelm@19736
    24
definition
wenzelm@21404
    25
  indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
wenzelm@19736
    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))"
paulson@15636
    27
paulson@15636
    28
paulson@15636
    29
text "The key theorem, corresponding to theorem 1 of the paper. All other results
paulson@15636
    30
      in this theory are proved using instances of this theorem, and theorems
paulson@15636
    31
      derived from this theorem."
paulson@15636
    32
paulson@15636
    33
theorem indinv_wfrec:
wenzelm@19736
    34
  assumes wf:  "wf r" and
wenzelm@19736
    35
          inv: "indinv r S F"
paulson@15636
    36
  shows        "S x (wfrec r F x)"
wenzelm@19736
    37
  using wf
wenzelm@19736
    38
proof (induct x)
paulson@15636
    39
  fix x
wenzelm@19736
    40
  assume  IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"
wenzelm@19736
    41
  then have     "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
wenzelm@19736
    42
  with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
wenzelm@19736
    43
  thus "S x (wfrec r F x)" using wf by (simp add: wfrec)
paulson@15636
    44
qed
paulson@15636
    45
paulson@15636
    46
theorem indinv_on_wfrec:
paulson@15636
    47
  assumes WF:  "wf r" and
paulson@15636
    48
          INV: "indinv_on r D S F" and
paulson@15636
    49
          D:   "x\<in>D"
paulson@15636
    50
  shows        "S x (wfrec r F x)"
paulson@15636
    51
apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])
paulson@15636
    52
by (simp add: indinv_on_def indinv_def)
paulson@15636
    53
paulson@15636
    54
theorem ind_fixpoint_on_lemma:
paulson@15636
    55
  assumes WF:  "wf r" and
paulson@15636
    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)
paulson@15636
    57
                               --> S x (wfrec r F x) & F f x = wfrec r F x" and
paulson@15636
    58
           D: "x\<in>D"
paulson@15636
    59
  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
paulson@15636
    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])
paulson@15636
    61
  show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"
paulson@15636
    62
  proof (unfold indinv_on_def, clarify)
paulson@15636
    63
    fix f x
paulson@15636
    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)"
paulson@15636
    65
    assume D': "x\<in>D"
paulson@15636
    66
    from A1 INV [THEN spec, of f, THEN bspec, OF D']
paulson@15636
    67
      have "S x (wfrec r F x)" and
paulson@15636
    68
           "F f x = wfrec r F x" by auto
paulson@15636
    69
    moreover
paulson@15636
    70
    from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto
paulson@15636
    71
    with D' INV [THEN spec, of "wfrec r F", simplified]
paulson@15636
    72
      have "F (wfrec r F) x = wfrec r F x" by blast
paulson@15636
    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
paulson@15636
    74
  qed
paulson@15636
    75
qed
paulson@15636
    76
paulson@15636
    77
theorem ind_fixpoint_lemma:
paulson@15636
    78
  assumes WF:  "wf r" and
paulson@15636
    79
         INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
paulson@15636
    80
                         --> S x (wfrec r F x) & F f x = wfrec r F x"
paulson@15636
    81
  shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
paulson@15636
    82
apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])
paulson@15636
    83
by (rule INV)
paulson@15636
    84
paulson@15636
    85
theorem tfl_indinv_wfrec:
paulson@15636
    86
"[| f == wfrec r F; wf r; indinv r S F |]
paulson@15636
    87
 ==> S x (f x)"
paulson@15636
    88
by (simp add: indinv_wfrec)
paulson@15636
    89
paulson@15636
    90
theorem tfl_indinv_on_wfrec:
paulson@15636
    91
"[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |]
paulson@15636
    92
 ==> S x (f x)"
paulson@15636
    93
by (simp add: indinv_on_wfrec)
paulson@15636
    94
wenzelm@17388
    95
end