src/HOL/Gfp.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14169 0590de71a016
permissions -rw-r--r--
import -> imports
     1 (*  Title:      HOL/Gfp.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 The Knaster-Tarski Theorem for greatest fixed points.
     7 *)
     8 
     9 (*** Proof of Knaster-Tarski Theorem using gfp ***)
    10 
    11 val gfp_def = thm "gfp_def";
    12 
    13 (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
    14 
    15 Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
    16 by (etac (CollectI RS Union_upper) 1);
    17 qed "gfp_upperbound";
    18 
    19 val prems = Goalw [gfp_def]
    20     "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X";
    21 by (REPEAT (ares_tac ([Union_least]@prems) 1));
    22 by (etac CollectD 1);
    23 qed "gfp_least";
    24 
    25 Goal "mono(f) ==> gfp(f) <= f(gfp(f))";
    26 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
    27             etac monoD, rtac gfp_upperbound, atac]);
    28 qed "gfp_lemma2";
    29 
    30 Goal "mono(f) ==> f(gfp(f)) <= gfp(f)";
    31 by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac,
    32             etac gfp_lemma2]);
    33 qed "gfp_lemma3";
    34 
    35 Goal "mono(f) ==> gfp(f) = f(gfp(f))";
    36 by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
    37 qed "gfp_unfold";
    38 
    39 (*** Coinduction rules for greatest fixed points ***)
    40 
    41 (*weak version*)
    42 Goal "[| a: X;  X <= f(X) |] ==> a : gfp(f)";
    43 by (rtac (gfp_upperbound RS subsetD) 1);
    44 by Auto_tac;
    45 qed "weak_coinduct";
    46 
    47 Goal "!!X. [| a : X; g`X <= f (g`X) |] ==> g a : gfp f";
    48 by (etac (gfp_upperbound RS subsetD) 1);
    49 by (etac imageI 1);
    50 qed "weak_coinduct_image";
    51 
    52 Goal "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
    53 \    X Un gfp(f) <= f(X Un gfp(f))";
    54 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 
    55 qed "coinduct_lemma";
    56 
    57 (*strong version, thanks to Coen & Frost*)
    58 Goal "[| mono(f);  a: X;  X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
    59 by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
    60 by (REPEAT (ares_tac [UnI1, Un_least] 1));
    61 qed "coinduct";
    62 
    63 Goal "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))";
    64 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 
    65 qed "gfp_fun_UnI2";
    66 
    67 (***  Even Stronger version of coinduct  [by Martin Coen]
    68          - instead of the condition  X <= f(X)
    69                            consider  X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
    70 
    71 Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
    72 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
    73 qed "coinduct3_mono_lemma";
    74 
    75 Goal "[| X <= f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |] ==> \
    76 \    lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
    77 by (rtac subset_trans 1);
    78 by (etac (coinduct3_mono_lemma RS lfp_lemma3) 1);
    79 by (rtac (Un_least RS Un_least) 1);
    80 by (rtac subset_refl 1);
    81 by (assume_tac 1); 
    82 by (rtac (gfp_unfold RS equalityD1 RS subset_trans) 1);
    83 by (assume_tac 1);
    84 by (rtac monoD 1 THEN assume_tac 1);
    85 by (stac (coinduct3_mono_lemma RS lfp_unfold) 1);
    86 by Auto_tac;  
    87 qed "coinduct3_lemma";
    88 
    89 Goal
    90   "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
    91 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
    92 by (resolve_tac [coinduct3_mono_lemma RS lfp_unfold RS ssubst] 1);
    93 by Auto_tac;
    94 qed "coinduct3";
    95 
    96 
    97 (** Definition forms of gfp_unfold and coinduct, to control unfolding **)
    98 
    99 Goal "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
   100 by (auto_tac (claset() addSIs [gfp_unfold], simpset()));  
   101 qed "def_gfp_unfold";
   102 
   103 Goal "[| A==gfp(f);  mono(f);  a:X;  X <= f(X Un A) |] ==> a: A";
   104 by (auto_tac (claset() addSIs [coinduct], simpset()));  
   105 qed "def_coinduct";
   106 
   107 (*The version used in the induction/coinduction package*)
   108 val prems = Goal
   109     "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));  \
   110 \       a: X;  !!z. z: X ==> P (X Un A) z |] ==> \
   111 \    a : A";
   112 by (rtac def_coinduct 1);
   113 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
   114 qed "def_Collect_coinduct";
   115 
   116 Goal "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un A)) |] \
   117 \     ==> a: A";
   118 by (auto_tac (claset() addSIs [coinduct3], simpset()));  
   119 qed "def_coinduct3";
   120 
   121 (*Monotonicity of gfp!*)
   122 val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
   123 by (rtac (gfp_upperbound RS gfp_least) 1);
   124 by (etac (prem RSN (2,subset_trans)) 1);
   125 qed "gfp_mono";