src/ZF/Fixedpt.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1461 6bcb44e4d6e5
child 2469 b50b8c0eec01
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
     1
(*  Title:      ZF/fixedpt.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For fixedpt.thy.  Least and greatest fixed points; the Knaster-Tarski Theorem
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
open Fixedpt;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(*** Monotone operators ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
val prems = goalw Fixedpt.thy [bnd_mono_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    "[| h(D)<=D;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
\       !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) <= h(X)  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
\    |] ==> bnd_mono(D,h)";  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
by (REPEAT (ares_tac (prems@[conjI,allI,impI]) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
     ORELSE etac subset_trans 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    21
qed "bnd_monoI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
by (rtac (major RS conjunct1) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    25
qed "bnd_monoD1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val major::prems = goalw Fixedpt.thy [bnd_mono_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
    "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) <= h(X)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (REPEAT (resolve_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    31
qed "bnd_monoD2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val [major,minor] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    "[| bnd_mono(D,h);  X<=D |] ==> h(X) <= D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
by (rtac (major RS bnd_monoD2 RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
by (rtac (major RS bnd_monoD1) 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
by (rtac minor 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (rtac subset_refl 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    39
qed "bnd_mono_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
goal Fixedpt.thy "!!A B. [| bnd_mono(D,h);  A <= D;  B <= D |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
\                         h(A) Un h(B) <= h(A Un B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (REPEAT (ares_tac [Un_upper1, Un_upper2, Un_least] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
     ORELSE etac bnd_monoD2 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    45
qed "bnd_mono_Un";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(*Useful??*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
goal Fixedpt.thy "!!A B. [| bnd_mono(D,h);  A <= D;  B <= D |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
\                        h(A Int B) <= h(A) Int h(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (REPEAT (ares_tac [Int_lower1, Int_lower2, Int_greatest] 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
     ORELSE etac bnd_monoD2 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    52
qed "bnd_mono_Int";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
(**** Proof of Knaster-Tarski Theorem for the lfp ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
(*lfp is contained in each pre-fixedpoint*)
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 684
diff changeset
    57
goalw Fixedpt.thy [lfp_def]
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 684
diff changeset
    58
    "!!A. [| h(A) <= A;  A<=D |] ==> lfp(D,h) <= A";
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 684
diff changeset
    59
by (fast_tac ZF_cs 1);
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 684
diff changeset
    60
(*or  by (rtac (PowI RS CollectI RS Inter_lower) 1); *)
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    61
qed "lfp_lowerbound";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
goalw Fixedpt.thy [lfp_def,Inter_def] "lfp(D,h) <= D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    66
qed "lfp_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(*Used in datatype package*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
by (rtac lfp_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    72
qed "def_lfp_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val prems = goalw Fixedpt.thy [lfp_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
    "[| h(D) <= D;  !!X. [| h(X) <= X;  X<=D |] ==> A<=X |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
\    A <= lfp(D,h)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
    77
by (rtac (Pow_top RS CollectI RS Inter_greatest) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    79
qed "lfp_greatest";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
val hmono::prems = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
    "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) <= A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (rtac lfp_lowerbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
by (REPEAT (resolve_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    86
qed "lfp_lemma1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val [hmono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
by (rtac (bnd_monoD1 RS lfp_greatest) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
by (rtac lfp_lemma1 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
by (REPEAT (ares_tac [hmono] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
    93
qed "lfp_lemma2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val [hmono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
    "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
by (rtac lfp_lowerbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
by (rtac (hmono RS bnd_monoD2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
by (rtac (hmono RS lfp_lemma2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
by (rtac (hmono RS bnd_mono_subset) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
by (REPEAT (rtac lfp_subset 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   102
qed "lfp_lemma3";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
val prems = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
    "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   107
qed "lfp_Tarski";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
(*Definition form, to control unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
val [rew,mono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
    "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
by (rtac (mono RS lfp_Tarski) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   114
qed "def_lfp_Tarski";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
(*** General induction rule for least fixedpoints ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
val [hmono,indstep] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    "[| bnd_mono(D,h);  !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
\    |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
by (rtac subsetI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
by (rtac CollectI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
by (etac indstep 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
by (rtac (hmono RS lfp_lemma2 RS subsetD) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
by (rtac (hmono RS bnd_monoD2 RS subsetD) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
by (REPEAT (ares_tac [Collect_subset, lfp_subset] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   127
qed "Collect_is_pre_fixedpt";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
(*This rule yields an induction hypothesis in which the components of a
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
  data structure may be assumed to be elements of lfp(D,h)*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val prems = goal Fixedpt.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
   132
    "[| bnd_mono(D,h);  a : lfp(D,h);                   \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
   133
\       !!x. x : h(Collect(lfp(D,h),P)) ==> P(x)        \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
\    |] ==> P(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
by (rtac (lfp_subset RS (Collect_subset RS subset_trans)) 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (REPEAT (ares_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   138
qed "induct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
(*Definition form, to control unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
val rew::prems = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
    "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
\       !!x. x : h(Collect(A,P)) ==> P(x) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
\    |] ==> P(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
by (rtac induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   147
qed "def_induct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*This version is useful when "A" is not a subset of D;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
  second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
val [hsub,hmono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
    "[| h(D Int A) <= A;  bnd_mono(D,h) |] ==> lfp(D,h) <= A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (rtac (lfp_lowerbound RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
by (REPEAT (resolve_tac [hsub,Int_lower1,Int_lower2] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   156
qed "lfp_Int_lowerbound";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(*Monotonicity of lfp, where h precedes i under a domain-like partial order
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
  monotonicity of h is not strictly necessary; h must be bounded by D*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
val [hmono,imono,subhi] = goal Fixedpt.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
   161
    "[| bnd_mono(D,h);  bnd_mono(E,i);          \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
\       !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(E,i)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   163
by (rtac (bnd_monoD1 RS lfp_greatest) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   164
by (rtac imono 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
by (rtac (Int_lower1 RS subhi RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
by (rtac (imono RS bnd_monoD2 RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
by (REPEAT (ares_tac [Int_lower2] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   169
qed "lfp_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
(*This (unused) version illustrates that monotonicity is not really needed,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
  but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
val [isubD,subhi] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
    "[| i(D) <= D;  !!X. X<=D ==> h(X) <= i(X)  |] ==> lfp(D,h) <= lfp(D,i)";
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   175
by (rtac lfp_greatest 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   176
by (rtac isubD 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
by (rtac lfp_lowerbound 1);
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 0
diff changeset
   178
by (etac (subhi RS subset_trans) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
by (REPEAT (assume_tac 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   180
qed "lfp_mono2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
(**** Proof of Knaster-Tarski Theorem for the gfp ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(*gfp contains each post-fixedpoint that is contained in D*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
val prems = goalw Fixedpt.thy [gfp_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
    "[| A <= h(A);  A<=D |] ==> A <= gfp(D,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
by (rtac (PowI RS CollectI RS Union_upper) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
by (REPEAT (resolve_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   190
qed "gfp_upperbound";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
by (fast_tac ZF_cs 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   194
qed "gfp_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
(*Used in datatype package*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
by (rtac gfp_subset 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   200
qed "def_gfp_subset";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
val hmono::prems = goalw Fixedpt.thy [gfp_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
    "[| bnd_mono(D,h);  !!X. [| X <= h(X);  X<=D |] ==> X<=A |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
\    gfp(D,h) <= A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   206
qed "gfp_least";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
val hmono::prems = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
    "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A <= h(gfp(D,h))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
by (rtac gfp_subset 3);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
by (rtac gfp_upperbound 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
by (REPEAT (resolve_tac prems 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   214
qed "gfp_lemma1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
val [hmono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
    "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
by (rtac gfp_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
by (rtac gfp_lemma1 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
by (REPEAT (ares_tac [hmono] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   221
qed "gfp_lemma2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
val [hmono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
    "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
by (rtac gfp_upperbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
by (rtac (hmono RS bnd_monoD2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
by (rtac (hmono RS gfp_lemma2) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   229
qed "gfp_lemma3";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
val prems = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
    "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   234
qed "gfp_Tarski";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
(*Definition form, to control unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
val [rew,mono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
    "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
by (rtac (mono RS gfp_Tarski) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   241
qed "def_gfp_Tarski";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
(*** Coinduction rules for greatest fixed points ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
(*weak version*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
goal Fixedpt.thy "!!X h. [| a: X;  X <= h(X);  X <= D |] ==> a : gfp(D,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   249
qed "weak_coinduct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
val [subs_h,subs_D,mono] = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
    "[| X <= h(X Un gfp(D,h));  X <= D;  bnd_mono(D,h) |] ==>  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
\    X Un gfp(D,h) <= h(X Un gfp(D,h))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
by (rtac (subs_h RS Un_least) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
by (rtac (mono RS gfp_lemma2 RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
by (rtac (Un_upper2 RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   258
qed "coinduct_lemma";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
(*strong version*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
    "!!X D. [| bnd_mono(D,h);  a: X;  X <= h(X Un gfp(D,h));  X <= D |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
\           a : gfp(D,h)";
647
fb7345cccddc ZF/Fixedpt/coinduct: modified proof to suppress deep unification
lcp
parents: 484
diff changeset
   264
by (rtac weak_coinduct 1);
fb7345cccddc ZF/Fixedpt/coinduct: modified proof to suppress deep unification
lcp
parents: 484
diff changeset
   265
by (etac coinduct_lemma 2);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   267
qed "coinduct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
(*Definition form, to control unfolding*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
val rew::prems = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
    "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X <= h(X Un A);  X <= D |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
\    a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
by (rewtac rew);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
by (rtac coinduct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   276
qed "def_coinduct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
(*Lemma used immediately below!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
val [subsA,XimpP] = goal ZF.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
    "[| X <= A;  !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (assume_tac 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
by (etac XimpP 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   284
qed "subset_Collect";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
(*The version used in the induction/coinduction package*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
val prems = goal Fixedpt.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
    "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
\       a: X;  X <= D;  !!z. z: X ==> P(X Un A, z) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
\    a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
by (rtac def_coinduct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
by (REPEAT (ares_tac (subset_Collect::prems) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   293
qed "def_Collect_coinduct";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
(*Monotonicity of gfp!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
val [hmono,subde,subhi] = goal Fixedpt.thy
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 760
diff changeset
   297
    "[| bnd_mono(D,h);  D <= E;                 \
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
\       !!X. X<=D ==> h(X) <= i(X)  |] ==> gfp(D,h) <= gfp(E,i)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
by (rtac gfp_upperbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   300
by (rtac (hmono RS gfp_lemma2 RS subset_trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
by (rtac (gfp_subset RS subhi) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
by (rtac ([gfp_subset, subde] MRS subset_trans) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   303
qed "gfp_mono";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304