src/HOL/FixedPoint.thy
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24390 9b5073c79a0b
child 24915 fc90277c0dd7
permissions -rw-r--r--
moved Finite_Set before Datatype
avigad@17006
     1
(*  Title:      HOL/FixedPoint.thy
avigad@17006
     2
    ID:         $Id$
avigad@17006
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
berghofe@21017
     4
    Author:     Stefan Berghofer, TU Muenchen
avigad@17006
     5
    Copyright   1992  University of Cambridge
avigad@17006
     6
*)
avigad@17006
     7
haftmann@22452
     8
header {* Fixed Points and the Knaster-Tarski Theorem*}
avigad@17006
     9
avigad@17006
    10
theory FixedPoint
haftmann@23878
    11
imports Lattices
haftmann@22918
    12
begin
haftmann@22918
    13
berghofe@21017
    14
subsection {* Least and greatest fixed points *}
berghofe@21017
    15
haftmann@22422
    16
definition
haftmann@22452
    17
  lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
haftmann@22422
    18
  "lfp f = Inf {u. f u \<le> u}"    --{*least fixed point*}
avigad@17006
    19
haftmann@22422
    20
definition
haftmann@22452
    21
  gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
haftmann@22422
    22
  "gfp f = Sup {u. u \<le> f u}"    --{*greatest fixed point*}
avigad@17006
    23
avigad@17006
    24
haftmann@22918
    25
subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *}
avigad@17006
    26
avigad@17006
    27
text{*@{term "lfp f"} is the least upper bound of 
berghofe@21017
    28
      the set @{term "{u. f(u) \<le> u}"} *}
berghofe@21017
    29
berghofe@21017
    30
lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
haftmann@22422
    31
  by (auto simp add: lfp_def intro: Inf_lower)
berghofe@21017
    32
berghofe@21017
    33
lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f"
haftmann@22422
    34
  by (auto simp add: lfp_def intro: Inf_greatest)
avigad@17006
    35
berghofe@21017
    36
lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f"
berghofe@21017
    37
  by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
avigad@17006
    38
berghofe@21017
    39
lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)"
berghofe@21017
    40
  by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
berghofe@21017
    41
berghofe@21017
    42
lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)"
berghofe@21017
    43
  by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
avigad@17006
    44
krauss@22356
    45
lemma lfp_const: "lfp (\<lambda>x. t) = t"
krauss@22356
    46
  by (rule lfp_unfold) (simp add:mono_def)
krauss@22356
    47
haftmann@22918
    48
haftmann@22918
    49
subsection {* General induction rules for least fixed points *}
avigad@17006
    50
berghofe@21017
    51
theorem lfp_induct:
haftmann@22422
    52
  assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P"
berghofe@21017
    53
  shows "lfp f <= P"
berghofe@21017
    54
proof -
haftmann@22422
    55
  have "inf (lfp f) P <= lfp f" by (rule inf_le1)
haftmann@22422
    56
  with mono have "f (inf (lfp f) P) <= f (lfp f)" ..
berghofe@21017
    57
  also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
haftmann@22422
    58
  finally have "f (inf (lfp f) P) <= lfp f" .
haftmann@22422
    59
  from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI)
haftmann@22422
    60
  hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound)
haftmann@22422
    61
  also have "inf (lfp f) P <= P" by (rule inf_le2)
berghofe@21017
    62
  finally show ?thesis .
berghofe@21017
    63
qed
avigad@17006
    64
berghofe@21017
    65
lemma lfp_induct_set:
avigad@17006
    66
  assumes lfp: "a: lfp(f)"
avigad@17006
    67
      and mono: "mono(f)"
avigad@17006
    68
      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
avigad@17006
    69
  shows "P(a)"
berghofe@21017
    70
  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
haftmann@22422
    71
    (auto simp: inf_set_eq intro: indhyp)
avigad@17006
    72
avigad@17006
    73
lemma lfp_ordinal_induct: 
avigad@17006
    74
  assumes mono: "mono f"
huffman@24390
    75
  and P_f: "!!S. P S ==> P(f S)"
huffman@24390
    76
  and P_Union: "!!M. !S:M. P S ==> P(Union M)"
huffman@24390
    77
  shows "P(lfp f)"
huffman@24390
    78
proof -
huffman@24390
    79
  let ?M = "{S. S \<subseteq> lfp f & P S}"
huffman@24390
    80
  have "P (Union ?M)" using P_Union by simp
huffman@24390
    81
  also have "Union ?M = lfp f"
huffman@24390
    82
  proof
huffman@24390
    83
    show "Union ?M \<subseteq> lfp f" by blast
huffman@24390
    84
    hence "f (Union ?M) \<subseteq> f (lfp f)" by (rule mono [THEN monoD])
huffman@24390
    85
    hence "f (Union ?M) \<subseteq> lfp f" using mono [THEN lfp_unfold] by simp
huffman@24390
    86
    hence "f (Union ?M) \<in> ?M" using P_f P_Union by simp
huffman@24390
    87
    hence "f (Union ?M) \<subseteq> Union ?M" by (rule Union_upper)
huffman@24390
    88
    thus "lfp f \<subseteq> Union ?M" by (rule lfp_lowerbound)
huffman@24390
    89
  qed
huffman@24390
    90
  finally show ?thesis .
huffman@24390
    91
qed
avigad@17006
    92
avigad@17006
    93
avigad@17006
    94
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
avigad@17006
    95
    to control unfolding*}
avigad@17006
    96
avigad@17006
    97
lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
avigad@17006
    98
by (auto intro!: lfp_unfold)
avigad@17006
    99
avigad@17006
   100
lemma def_lfp_induct: 
berghofe@21017
   101
    "[| A == lfp(f); mono(f);
haftmann@22422
   102
        f (inf A P) \<le> P
berghofe@21017
   103
     |] ==> A \<le> P"
berghofe@21017
   104
  by (blast intro: lfp_induct)
berghofe@21017
   105
berghofe@21017
   106
lemma def_lfp_induct_set: 
avigad@17006
   107
    "[| A == lfp(f);  mono(f);   a:A;                    
avigad@17006
   108
        !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)         
avigad@17006
   109
     |] ==> P(a)"
berghofe@21017
   110
  by (blast intro: lfp_induct_set)
avigad@17006
   111
avigad@17006
   112
(*Monotonicity of lfp!*)
berghofe@21017
   113
lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g"
berghofe@21017
   114
  by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans)
avigad@17006
   115
avigad@17006
   116
haftmann@22918
   117
subsection {* Proof of Knaster-Tarski Theorem using @{term gfp} *}
avigad@17006
   118
avigad@17006
   119
text{*@{term "gfp f"} is the greatest lower bound of 
berghofe@21017
   120
      the set @{term "{u. u \<le> f(u)}"} *}
avigad@17006
   121
berghofe@21017
   122
lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
nipkow@21312
   123
  by (auto simp add: gfp_def intro: Sup_upper)
avigad@17006
   124
berghofe@21017
   125
lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
nipkow@21312
   126
  by (auto simp add: gfp_def intro: Sup_least)
avigad@17006
   127
berghofe@21017
   128
lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
berghofe@21017
   129
  by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
avigad@17006
   130
berghofe@21017
   131
lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f"
berghofe@21017
   132
  by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
avigad@17006
   133
berghofe@21017
   134
lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)"
berghofe@21017
   135
  by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
avigad@17006
   136
haftmann@22918
   137
haftmann@22918
   138
subsection {* Coinduction rules for greatest fixed points *}
avigad@17006
   139
avigad@17006
   140
text{*weak version*}
avigad@17006
   141
lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
avigad@17006
   142
by (rule gfp_upperbound [THEN subsetD], auto)
avigad@17006
   143
avigad@17006
   144
lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
avigad@17006
   145
apply (erule gfp_upperbound [THEN subsetD])
avigad@17006
   146
apply (erule imageI)
avigad@17006
   147
done
avigad@17006
   148
avigad@17006
   149
lemma coinduct_lemma:
haftmann@22422
   150
     "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
berghofe@21017
   151
  apply (frule gfp_lemma2)
haftmann@22422
   152
  apply (drule mono_sup)
haftmann@22422
   153
  apply (rule le_supI)
berghofe@21017
   154
  apply assumption
berghofe@21017
   155
  apply (rule order_trans)
berghofe@21017
   156
  apply (rule order_trans)
berghofe@21017
   157
  apply assumption
haftmann@22422
   158
  apply (rule sup_ge2)
berghofe@21017
   159
  apply assumption
berghofe@21017
   160
  done
avigad@17006
   161
avigad@17006
   162
text{*strong version, thanks to Coen and Frost*}
berghofe@21017
   163
lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
haftmann@22422
   164
by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
berghofe@21017
   165
haftmann@22422
   166
lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
berghofe@21017
   167
  apply (rule order_trans)
haftmann@22422
   168
  apply (rule sup_ge1)
berghofe@21017
   169
  apply (erule gfp_upperbound [OF coinduct_lemma])
berghofe@21017
   170
  apply assumption
berghofe@21017
   171
  done
avigad@17006
   172
avigad@17006
   173
lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
avigad@17006
   174
by (blast dest: gfp_lemma2 mono_Un)
avigad@17006
   175
haftmann@22918
   176
haftmann@22918
   177
subsection {* Even Stronger Coinduction Rule, by Martin Coen *}
avigad@17006
   178
avigad@17006
   179
text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
avigad@17006
   180
  @{term lfp} and @{term gfp}*}
avigad@17006
   181
avigad@17006
   182
lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
nipkow@17589
   183
by (iprover intro: subset_refl monoI Un_mono monoD)
avigad@17006
   184
avigad@17006
   185
lemma coinduct3_lemma:
avigad@17006
   186
     "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |]
avigad@17006
   187
      ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))"
avigad@17006
   188
apply (rule subset_trans)
avigad@17006
   189
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
avigad@17006
   190
apply (rule Un_least [THEN Un_least])
avigad@17006
   191
apply (rule subset_refl, assumption)
avigad@17006
   192
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
avigad@17006
   193
apply (rule monoD, assumption)
avigad@17006
   194
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
avigad@17006
   195
done
avigad@17006
   196
avigad@17006
   197
lemma coinduct3: 
avigad@17006
   198
  "[| mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
avigad@17006
   199
apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
avigad@17006
   200
apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto)
avigad@17006
   201
done
avigad@17006
   202
avigad@17006
   203
avigad@17006
   204
text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, 
avigad@17006
   205
    to control unfolding*}
avigad@17006
   206
avigad@17006
   207
lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
avigad@17006
   208
by (auto intro!: gfp_unfold)
avigad@17006
   209
avigad@17006
   210
lemma def_coinduct:
haftmann@22422
   211
     "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
berghofe@21017
   212
by (iprover intro!: coinduct)
berghofe@21017
   213
berghofe@21017
   214
lemma def_coinduct_set:
avigad@17006
   215
     "[| A==gfp(f);  mono(f);  a:X;  X \<subseteq> f(X Un A) |] ==> a: A"
berghofe@21017
   216
by (auto intro!: coinduct_set)
avigad@17006
   217
avigad@17006
   218
(*The version used in the induction/coinduction package*)
avigad@17006
   219
lemma def_Collect_coinduct:
avigad@17006
   220
    "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));   
avigad@17006
   221
        a: X;  !!z. z: X ==> P (X Un A) z |] ==>  
avigad@17006
   222
     a : A"
berghofe@21017
   223
apply (erule def_coinduct_set, auto) 
avigad@17006
   224
done
avigad@17006
   225
avigad@17006
   226
lemma def_coinduct3:
avigad@17006
   227
    "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
avigad@17006
   228
by (auto intro!: coinduct3)
avigad@17006
   229
avigad@17006
   230
text{*Monotonicity of @{term gfp}!*}
berghofe@21017
   231
lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
berghofe@21017
   232
  by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
avigad@17006
   233
avigad@17006
   234
ML
avigad@17006
   235
{*
avigad@17006
   236
val lfp_def = thm "lfp_def";
avigad@17006
   237
val lfp_lowerbound = thm "lfp_lowerbound";
avigad@17006
   238
val lfp_greatest = thm "lfp_greatest";
avigad@17006
   239
val lfp_unfold = thm "lfp_unfold";
avigad@17006
   240
val lfp_induct = thm "lfp_induct";
avigad@17006
   241
val lfp_ordinal_induct = thm "lfp_ordinal_induct";
avigad@17006
   242
val def_lfp_unfold = thm "def_lfp_unfold";
avigad@17006
   243
val def_lfp_induct = thm "def_lfp_induct";
berghofe@21017
   244
val def_lfp_induct_set = thm "def_lfp_induct_set";
avigad@17006
   245
val lfp_mono = thm "lfp_mono";
avigad@17006
   246
val gfp_def = thm "gfp_def";
avigad@17006
   247
val gfp_upperbound = thm "gfp_upperbound";
avigad@17006
   248
val gfp_least = thm "gfp_least";
avigad@17006
   249
val gfp_unfold = thm "gfp_unfold";
avigad@17006
   250
val weak_coinduct = thm "weak_coinduct";
avigad@17006
   251
val weak_coinduct_image = thm "weak_coinduct_image";
avigad@17006
   252
val coinduct = thm "coinduct";
avigad@17006
   253
val gfp_fun_UnI2 = thm "gfp_fun_UnI2";
avigad@17006
   254
val coinduct3 = thm "coinduct3";
avigad@17006
   255
val def_gfp_unfold = thm "def_gfp_unfold";
avigad@17006
   256
val def_coinduct = thm "def_coinduct";
avigad@17006
   257
val def_Collect_coinduct = thm "def_Collect_coinduct";
avigad@17006
   258
val def_coinduct3 = thm "def_coinduct3";
avigad@17006
   259
val gfp_mono = thm "gfp_mono";
berghofe@21017
   260
val le_funI = thm "le_funI";
berghofe@21017
   261
val le_boolI = thm "le_boolI";
berghofe@21017
   262
val le_boolI' = thm "le_boolI'";
haftmann@22422
   263
val inf_fun_eq = thm "inf_fun_eq";
haftmann@22422
   264
val inf_bool_eq = thm "inf_bool_eq";
berghofe@21017
   265
val le_funE = thm "le_funE";
berghofe@22276
   266
val le_funD = thm "le_funD";
berghofe@21017
   267
val le_boolE = thm "le_boolE";
berghofe@21017
   268
val le_boolD = thm "le_boolD";
berghofe@21017
   269
val le_bool_def = thm "le_bool_def";
berghofe@21017
   270
val le_fun_def = thm "le_fun_def";
avigad@17006
   271
*}
avigad@17006
   272
avigad@17006
   273
end