src/HOL/Gfp.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10186 499637e8f2c6
child 11335 c150861633da
permissions -rw-r--r--
improved theory reference in comment
     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 (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
    12 
    13 Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
    14 by (etac (CollectI RS Union_upper) 1);
    15 qed "gfp_upperbound";
    16 
    17 val prems = Goalw [gfp_def]
    18     "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X";
    19 by (REPEAT (ares_tac ([Union_least]@prems) 1));
    20 by (etac CollectD 1);
    21 qed "gfp_least";
    22 
    23 Goal "mono(f) ==> gfp(f) <= f(gfp(f))";
    24 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
    25             etac monoD, rtac gfp_upperbound, atac]);
    26 qed "gfp_lemma2";
    27 
    28 Goal "mono(f) ==> f(gfp(f)) <= gfp(f)";
    29 by (EVERY1 [rtac gfp_upperbound, rtac monoD, assume_tac,
    30             etac gfp_lemma2]);
    31 qed "gfp_lemma3";
    32 
    33 Goal "mono(f) ==> gfp(f) = f(gfp(f))";
    34 by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1));
    35 qed "gfp_unfold";
    36 
    37 (*** Coinduction rules for greatest fixed points ***)
    38 
    39 (*weak version*)
    40 Goal "[| a: X;  X <= f(X) |] ==> a : gfp(f)";
    41 by (rtac (gfp_upperbound RS subsetD) 1);
    42 by Auto_tac;
    43 qed "weak_coinduct";
    44 
    45 Goal "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
    46 \    X Un gfp(f) <= f(X Un gfp(f))";
    47 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 
    48 qed "coinduct_lemma";
    49 
    50 (*strong version, thanks to Coen & Frost*)
    51 Goal "[| mono(f);  a: X;  X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
    52 by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
    53 by (REPEAT (ares_tac [UnI1, Un_least] 1));
    54 qed "coinduct";
    55 
    56 Goal "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))";
    57 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1); 
    58 qed "gfp_fun_UnI2";
    59 
    60 (***  Even Stronger version of coinduct  [by Martin Coen]
    61          - instead of the condition  X <= f(X)
    62                            consider  X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
    63 
    64 Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
    65 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
    66 qed "coinduct3_mono_lemma";
    67 
    68 Goal "[| X <= f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |] ==> \
    69 \    lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
    70 by (rtac subset_trans 1);
    71 by (etac (coinduct3_mono_lemma RS lfp_lemma3) 1);
    72 by (rtac (Un_least RS Un_least) 1);
    73 by (rtac subset_refl 1);
    74 by (assume_tac 1); 
    75 by (rtac (gfp_unfold RS equalityD1 RS subset_trans) 1);
    76 by (assume_tac 1);
    77 by (rtac monoD 1 THEN assume_tac 1);
    78 by (stac (coinduct3_mono_lemma RS lfp_unfold) 1);
    79 by Auto_tac;  
    80 qed "coinduct3_lemma";
    81 
    82 Goal
    83   "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
    84 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
    85 by (resolve_tac [coinduct3_mono_lemma RS lfp_unfold RS ssubst] 1);
    86 by Auto_tac;
    87 qed "coinduct3";
    88 
    89 
    90 (** Definition forms of gfp_unfold and coinduct, to control unfolding **)
    91 
    92 Goal "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
    93 by (auto_tac (claset() addSIs [gfp_unfold], simpset()));  
    94 qed "def_gfp_unfold";
    95 
    96 Goal "[| A==gfp(f);  mono(f);  a:X;  X <= f(X Un A) |] ==> a: A";
    97 by (auto_tac (claset() addSIs [coinduct], simpset()));  
    98 qed "def_coinduct";
    99 
   100 (*The version used in the induction/coinduction package*)
   101 val prems = Goal
   102     "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));  \
   103 \       a: X;  !!z. z: X ==> P (X Un A) z |] ==> \
   104 \    a : A";
   105 by (rtac def_coinduct 1);
   106 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
   107 qed "def_Collect_coinduct";
   108 
   109 Goal "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un A)) |] \
   110 \     ==> a: A";
   111 by (auto_tac (claset() addSIs [coinduct3], simpset()));  
   112 qed "def_coinduct3";
   113 
   114 (*Monotonicity of gfp!*)
   115 val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
   116 by (rtac (gfp_upperbound RS gfp_least) 1);
   117 by (etac (prem RSN (2,subset_trans)) 1);
   118 qed "gfp_mono";