src/HOL/Gfp.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5316 7a8975451a89
child 9422 4b6bc2b347e5
permissions -rw-r--r--
tidying
     1 (*  Title:      HOL/gfp
     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 open Gfp;
    10 
    11 (*** Proof of Knaster-Tarski Theorem using gfp ***)
    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.thy [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_Tarski";
    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 val [prem,mono] = goal Gfp.thy
    48     "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
    49 \    X Un gfp(f) <= f(X Un gfp(f))";
    50 by (rtac (prem RS Un_least) 1);
    51 by (rtac (mono RS gfp_lemma2 RS subset_trans) 1);
    52 by (rtac (Un_upper2 RS subset_trans) 1);
    53 by (rtac (mono RS mono_Un) 1);
    54 qed "coinduct_lemma";
    55 
    56 (*strong version, thanks to Coen & Frost*)
    57 Goal "[| mono(f);  a: X;  X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
    58 by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
    59 by (REPEAT (ares_tac [UnI1, Un_least] 1));
    60 qed "coinduct";
    61 
    62 val [mono,prem] = goal Gfp.thy
    63     "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))";
    64 by (rtac (mono RS mono_Un RS subsetD) 1);
    65 by (rtac (mono RS gfp_lemma2 RS subsetD RS UnI2) 1);
    66 by (rtac prem 1);
    67 qed "gfp_fun_UnI2";
    68 
    69 (***  Even Stronger version of coinduct  [by Martin Coen]
    70          - instead of the condition  X <= f(X)
    71                            consider  X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
    72 
    73 Goal "mono(f) ==> mono(%x. f(x) Un X Un B)";
    74 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono] 1 ORELSE etac monoD 1));
    75 qed "coinduct3_mono_lemma";
    76 
    77 val [prem,mono] = goal Gfp.thy
    78     "[| X <= f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |] ==> \
    79 \    lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))";
    80 by (rtac subset_trans 1);
    81 by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1);
    82 by (rtac (Un_least RS Un_least) 1);
    83 by (rtac subset_refl 1);
    84 by (rtac prem 1);
    85 by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
    86 by (rtac (mono RS monoD) 1);
    87 by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1);
    88 by (rtac Un_upper2 1);
    89 qed "coinduct3_lemma";
    90 
    91 Goal
    92   "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
    93 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
    94 by (resolve_tac [coinduct3_mono_lemma RS lfp_Tarski RS ssubst] 1);
    95 by Auto_tac;
    96 qed "coinduct3";
    97 
    98 
    99 (** Definition forms of gfp_Tarski and coinduct, to control unfolding **)
   100 
   101 val [rew,mono] = goal Gfp.thy "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
   102 by (rewtac rew);
   103 by (rtac (mono RS gfp_Tarski) 1);
   104 qed "def_gfp_Tarski";
   105 
   106 val rew::prems = goal Gfp.thy
   107     "[| A==gfp(f);  mono(f);  a:X;  X <= f(X Un A) |] ==> a: A";
   108 by (rewtac rew);
   109 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1));
   110 qed "def_coinduct";
   111 
   112 (*The version used in the induction/coinduction package*)
   113 val prems = Goal
   114     "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));  \
   115 \       a: X;  !!z. z: X ==> P (X Un A) z |] ==> \
   116 \    a : A";
   117 by (rtac def_coinduct 1);
   118 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
   119 qed "def_Collect_coinduct";
   120 
   121 val rew::prems = goal Gfp.thy
   122     "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A";
   123 by (rewtac rew);
   124 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
   125 qed "def_coinduct3";
   126 
   127 (*Monotonicity of gfp!*)
   128 val [prem] = Goal "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
   129 by (rtac (gfp_upperbound RS gfp_least) 1);
   130 by (etac (prem RSN (2,subset_trans)) 1);
   131 qed "gfp_mono";