src/HOL/Gfp.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2036 62ff902eeffc
child 3842 b55686a7b22c
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@1465
     1
(*  Title:      HOL/gfp
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
For gfp.thy.  The Knaster-Tarski Theorem for greatest fixed points.
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
open Gfp;
clasohm@923
    10
clasohm@923
    11
(*** Proof of Knaster-Tarski Theorem using gfp ***)
clasohm@923
    12
clasohm@923
    13
(* gfp(f) is the least upper bound of {u. u <= f(u)} *)
clasohm@923
    14
clasohm@923
    15
val prems = goalw Gfp.thy [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
clasohm@923
    16
by (rtac (CollectI RS Union_upper) 1);
clasohm@923
    17
by (resolve_tac prems 1);
clasohm@923
    18
qed "gfp_upperbound";
clasohm@923
    19
clasohm@923
    20
val prems = goalw Gfp.thy [gfp_def]
clasohm@923
    21
    "[| !!u. u <= f(u) ==> u<=X |] ==> gfp(f) <= X";
clasohm@923
    22
by (REPEAT (ares_tac ([Union_least]@prems) 1));
clasohm@923
    23
by (etac CollectD 1);
clasohm@923
    24
qed "gfp_least";
clasohm@923
    25
clasohm@923
    26
val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
clasohm@923
    27
by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
clasohm@1465
    28
            rtac (mono RS monoD), rtac gfp_upperbound, atac]);
clasohm@923
    29
qed "gfp_lemma2";
clasohm@923
    30
clasohm@923
    31
val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
clasohm@923
    32
by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), 
clasohm@1465
    33
            rtac gfp_lemma2, rtac mono]);
clasohm@923
    34
qed "gfp_lemma3";
clasohm@923
    35
clasohm@923
    36
val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
clasohm@923
    37
by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
clasohm@923
    38
qed "gfp_Tarski";
clasohm@923
    39
clasohm@923
    40
(*** Coinduction rules for greatest fixed points ***)
clasohm@923
    41
clasohm@923
    42
(*weak version*)
clasohm@923
    43
val prems = goal Gfp.thy
clasohm@923
    44
    "[| a: X;  X <= f(X) |] ==> a : gfp(f)";
clasohm@923
    45
by (rtac (gfp_upperbound RS subsetD) 1);
clasohm@923
    46
by (REPEAT (ares_tac prems 1));
clasohm@923
    47
qed "weak_coinduct";
clasohm@923
    48
clasohm@923
    49
val [prem,mono] = goal Gfp.thy
clasohm@923
    50
    "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
clasohm@923
    51
\    X Un gfp(f) <= f(X Un gfp(f))";
clasohm@923
    52
by (rtac (prem RS Un_least) 1);
clasohm@923
    53
by (rtac (mono RS gfp_lemma2 RS subset_trans) 1);
clasohm@923
    54
by (rtac (Un_upper2 RS subset_trans) 1);
clasohm@923
    55
by (rtac (mono RS mono_Un) 1);
clasohm@923
    56
qed "coinduct_lemma";
clasohm@923
    57
clasohm@923
    58
(*strong version, thanks to Coen & Frost*)
clasohm@923
    59
goal Gfp.thy
clasohm@923
    60
    "!!X. [| mono(f);  a: X;  X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
clasohm@923
    61
by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
clasohm@923
    62
by (REPEAT (ares_tac [UnI1, Un_least] 1));
clasohm@923
    63
qed "coinduct";
clasohm@923
    64
clasohm@923
    65
val [mono,prem] = goal Gfp.thy
clasohm@923
    66
    "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))";
clasohm@1465
    67
by (rtac (mono RS mono_Un RS subsetD) 1);
clasohm@1465
    68
by (rtac (mono RS gfp_lemma2 RS subsetD RS UnI2) 1);
clasohm@923
    69
by (rtac prem 1);
clasohm@923
    70
qed "gfp_fun_UnI2";
clasohm@923
    71
clasohm@923
    72
(***  Even Stronger version of coinduct  [by Martin Coen]
clasohm@923
    73
         - instead of the condition  X <= f(X)
clasohm@923
    74
                           consider  X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
clasohm@923
    75
clasohm@923
    76
val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un X Un B)";
clasohm@923
    77
by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
clasohm@923
    78
qed "coinduct3_mono_lemma";
clasohm@923
    79
clasohm@923
    80
val [prem,mono] = goal Gfp.thy
clasohm@923
    81
    "[| X <= f(lfp(%x.f(x) Un X Un gfp(f)));  mono(f) |] ==> \
clasohm@923
    82
\    lfp(%x.f(x) Un X Un gfp(f)) <= f(lfp(%x.f(x) Un X Un gfp(f)))";
clasohm@923
    83
by (rtac subset_trans 1);
clasohm@923
    84
by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1);
clasohm@923
    85
by (rtac (Un_least RS Un_least) 1);
clasohm@923
    86
by (rtac subset_refl 1);
clasohm@923
    87
by (rtac prem 1);
clasohm@923
    88
by (rtac (mono RS gfp_Tarski RS equalityD1 RS subset_trans) 1);
clasohm@923
    89
by (rtac (mono RS monoD) 1);
paulson@2036
    90
by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1);
clasohm@923
    91
by (rtac Un_upper2 1);
clasohm@923
    92
qed "coinduct3_lemma";
clasohm@923
    93
clasohm@923
    94
val prems = goal Gfp.thy
clasohm@923
    95
    "[| mono(f);  a:X;  X <= f(lfp(%x.f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
clasohm@923
    96
by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
clasohm@923
    97
by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
clasohm@923
    98
by (rtac (UnI2 RS UnI1) 1);
clasohm@923
    99
by (REPEAT (resolve_tac prems 1));
clasohm@923
   100
qed "coinduct3";
clasohm@923
   101
clasohm@923
   102
clasohm@923
   103
(** Definition forms of gfp_Tarski and coinduct, to control unfolding **)
clasohm@923
   104
clasohm@923
   105
val [rew,mono] = goal Gfp.thy "[| A==gfp(f);  mono(f) |] ==> A = f(A)";
clasohm@923
   106
by (rewtac rew);
clasohm@923
   107
by (rtac (mono RS gfp_Tarski) 1);
clasohm@923
   108
qed "def_gfp_Tarski";
clasohm@923
   109
clasohm@923
   110
val rew::prems = goal Gfp.thy
clasohm@923
   111
    "[| A==gfp(f);  mono(f);  a:X;  X <= f(X Un A) |] ==> a: A";
clasohm@923
   112
by (rewtac rew);
clasohm@923
   113
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct]) 1));
clasohm@923
   114
qed "def_coinduct";
clasohm@923
   115
clasohm@923
   116
(*The version used in the induction/coinduction package*)
clasohm@923
   117
val prems = goal Gfp.thy
clasohm@923
   118
    "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));  \
clasohm@923
   119
\       a: X;  !!z. z: X ==> P (X Un A) z |] ==> \
clasohm@923
   120
\    a : A";
clasohm@923
   121
by (rtac def_coinduct 1);
clasohm@923
   122
by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1));
clasohm@923
   123
qed "def_Collect_coinduct";
clasohm@923
   124
clasohm@923
   125
val rew::prems = goal Gfp.thy
clasohm@923
   126
    "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x.f(x) Un X Un A)) |] ==> a: A";
clasohm@923
   127
by (rewtac rew);
clasohm@923
   128
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
clasohm@923
   129
qed "def_coinduct3";
clasohm@923
   130
clasohm@923
   131
(*Monotonicity of gfp!*)
clasohm@923
   132
val prems = goal Gfp.thy
clasohm@923
   133
    "[| mono(f);  !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
clasohm@923
   134
by (rtac gfp_upperbound 1);
clasohm@923
   135
by (rtac subset_trans 1);
clasohm@923
   136
by (rtac gfp_lemma2 1);
clasohm@923
   137
by (resolve_tac prems 1);
clasohm@923
   138
by (resolve_tac prems 1);
clasohm@923
   139
val gfp_mono = result();
clasohm@923
   140
clasohm@923
   141
(*Monotonicity of gfp!*)
clasohm@923
   142
val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
clasohm@1465
   143
by (rtac (gfp_upperbound RS gfp_least) 1);
clasohm@1465
   144
by (etac (prem RSN (2,subset_trans)) 1);
clasohm@923
   145
qed "gfp_mono";