src/HOL/FixedPoint.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 23131 29e913950928
child 23707 745799215e02
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
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@22452
    11
imports Product_Type
avigad@17006
    12
begin
avigad@17006
    13
berghofe@21017
    14
subsection {* Complete lattices *}
haftmann@22422
    15
haftmann@22452
    16
class complete_lattice = lattice +
haftmann@22918
    17
  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
haftmann@22845
    18
  assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
haftmann@22845
    19
  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
haftmann@22918
    20
begin
haftmann@22918
    21
haftmann@22918
    22
definition
haftmann@22918
    23
  Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
haftmann@22918
    24
where
haftmann@23108
    25
  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<^loc>\<le> b}"
haftmann@23108
    26
haftmann@23108
    27
lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<^loc>\<le> a}"
haftmann@23108
    28
  unfolding Sup_def by (auto intro: Inf_greatest Inf_lower)
haftmann@22918
    29
haftmann@22918
    30
lemma Sup_upper: "x \<in> A \<Longrightarrow> x \<^loc>\<le> \<Squnion>A"
haftmann@22918
    31
  by (auto simp: Sup_def intro: Inf_greatest)
haftmann@22918
    32
haftmann@22918
    33
lemma Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<^loc>\<le> z) \<Longrightarrow> \<Squnion>A \<^loc>\<le> z"
haftmann@22918
    34
  by (auto simp: Sup_def intro: Inf_lower)
haftmann@22918
    35
haftmann@22918
    36
lemma top_greatest [simp]: "x \<^loc>\<le> \<Sqinter>{}"
haftmann@22918
    37
  by (rule Inf_greatest) simp
haftmann@22918
    38
haftmann@22918
    39
lemma bot_least [simp]: "\<Squnion>{} \<^loc>\<le> x"
haftmann@22918
    40
  by (rule Sup_least) simp
haftmann@22918
    41
haftmann@23108
    42
lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
haftmann@23108
    43
  unfolding Sup_def by auto
haftmann@23108
    44
haftmann@23108
    45
lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
haftmann@23108
    46
  unfolding Inf_Sup by auto
haftmann@23108
    47
haftmann@22918
    48
lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
haftmann@22918
    49
  apply (rule antisym)
haftmann@22918
    50
  apply (rule le_infI)
haftmann@22918
    51
  apply (rule Inf_lower)
haftmann@22918
    52
  apply simp
haftmann@22918
    53
  apply (rule Inf_greatest)
haftmann@22918
    54
  apply (rule Inf_lower)
haftmann@22918
    55
  apply simp
haftmann@22918
    56
  apply (rule Inf_greatest)
haftmann@22918
    57
  apply (erule insertE)
haftmann@22918
    58
  apply (rule le_infI1)
haftmann@22918
    59
  apply simp
haftmann@22918
    60
  apply (rule le_infI2)
haftmann@22918
    61
  apply (erule Inf_lower)
haftmann@22918
    62
  done
haftmann@22918
    63
haftmann@22918
    64
lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
haftmann@22918
    65
  apply (rule antisym)
haftmann@22918
    66
  apply (rule Sup_least)
haftmann@22918
    67
  apply (erule insertE)
haftmann@22918
    68
  apply (rule le_supI1)
haftmann@22918
    69
  apply simp
haftmann@22918
    70
  apply (rule le_supI2)
haftmann@22918
    71
  apply (erule Sup_upper)
haftmann@22918
    72
  apply (rule le_supI)
haftmann@22918
    73
  apply (rule Sup_upper)
haftmann@22918
    74
  apply simp
haftmann@22918
    75
  apply (rule Sup_least)
haftmann@22918
    76
  apply (rule Sup_upper)
haftmann@22918
    77
  apply simp
haftmann@22918
    78
  done
haftmann@22918
    79
haftmann@22918
    80
lemma Inf_singleton [simp]:
haftmann@22918
    81
  "\<Sqinter>{a} = a"
haftmann@22918
    82
  by (auto intro: antisym Inf_lower Inf_greatest)
haftmann@22918
    83
haftmann@22918
    84
lemma Sup_singleton [simp]:
haftmann@22918
    85
  "\<Squnion>{a} = a"
haftmann@22918
    86
  by (auto intro: antisym Sup_upper Sup_least)
haftmann@22918
    87
haftmann@22918
    88
lemma Inf_insert_simp:
haftmann@22918
    89
  "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
haftmann@22918
    90
  by (cases "A = {}") (simp_all, simp add: Inf_insert)
haftmann@22918
    91
haftmann@22918
    92
lemma Sup_insert_simp:
haftmann@22918
    93
  "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
haftmann@22918
    94
  by (cases "A = {}") (simp_all, simp add: Sup_insert)
haftmann@22918
    95
haftmann@22918
    96
lemma Inf_binary:
haftmann@22918
    97
  "\<Sqinter>{a, b} = a \<sqinter> b"
haftmann@22918
    98
  by (simp add: Inf_insert_simp)
haftmann@22918
    99
haftmann@22918
   100
lemma Sup_binary:
haftmann@22918
   101
  "\<Squnion>{a, b} = a \<squnion> b"
haftmann@22918
   102
  by (simp add: Sup_insert_simp)
haftmann@22918
   103
haftmann@22918
   104
end
haftmann@22918
   105
haftmann@23108
   106
lemmas Sup_def = Sup_def [folded complete_lattice_class.Sup]
haftmann@23108
   107
lemmas Sup_upper = Sup_upper [folded complete_lattice_class.Sup]
haftmann@23108
   108
lemmas Sup_least = Sup_least [folded complete_lattice_class.Sup]
haftmann@22918
   109
haftmann@23108
   110
lemmas bot_least [simp] = bot_least [folded complete_lattice_class.Sup]
haftmann@23108
   111
lemmas Sup_insert [code func] = Sup_insert [folded complete_lattice_class.Sup]
haftmann@23108
   112
lemmas Sup_singleton [simp, code func] = Sup_singleton [folded complete_lattice_class.Sup]
haftmann@23108
   113
lemmas Sup_insert_simp = Sup_insert_simp [folded complete_lattice_class.Sup]
haftmann@23108
   114
lemmas Sup_binary = Sup_binary [folded complete_lattice_class.Sup]
berghofe@21017
   115
berghofe@22430
   116
definition
haftmann@22452
   117
  SUPR :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
berghofe@22430
   118
  "SUPR A f == Sup (f ` A)"
berghofe@22430
   119
berghofe@22430
   120
definition
haftmann@22452
   121
  INFI :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> 'b" where
berghofe@22430
   122
  "INFI A f == Inf (f ` A)"
berghofe@22430
   123
berghofe@22430
   124
syntax
wenzelm@22439
   125
  "_SUP1"     :: "pttrns => 'b => 'b"           ("(3SUP _./ _)" [0, 10] 10)
wenzelm@22439
   126
  "_SUP"      :: "pttrn => 'a set => 'b => 'b"  ("(3SUP _:_./ _)" [0, 10] 10)
wenzelm@22439
   127
  "_INF1"     :: "pttrns => 'b => 'b"           ("(3INF _./ _)" [0, 10] 10)
wenzelm@22439
   128
  "_INF"      :: "pttrn => 'a set => 'b => 'b"  ("(3INF _:_./ _)" [0, 10] 10)
berghofe@22430
   129
berghofe@22430
   130
translations
berghofe@22430
   131
  "SUP x y. B"   == "SUP x. SUP y. B"
berghofe@22430
   132
  "SUP x. B"     == "CONST SUPR UNIV (%x. B)"
berghofe@22430
   133
  "SUP x. B"     == "SUP x:UNIV. B"
berghofe@22430
   134
  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
berghofe@22430
   135
  "INF x y. B"   == "INF x. INF y. B"
berghofe@22430
   136
  "INF x. B"     == "CONST INFI UNIV (%x. B)"
berghofe@22430
   137
  "INF x. B"     == "INF x:UNIV. B"
berghofe@22430
   138
  "INF x:A. B"   == "CONST INFI A (%x. B)"
berghofe@22430
   139
berghofe@22430
   140
(* To avoid eta-contraction of body: *)
berghofe@22430
   141
print_translation {*
berghofe@22430
   142
let
berghofe@22430
   143
  fun btr' syn (A :: Abs abs :: ts) =
berghofe@22430
   144
    let val (x,t) = atomic_abs_tr' abs
berghofe@22430
   145
    in list_comb (Syntax.const syn $ x $ A $ t, ts) end
berghofe@22430
   146
  val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
berghofe@22430
   147
in
berghofe@22430
   148
[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
berghofe@22430
   149
end
berghofe@22430
   150
*}
berghofe@22430
   151
berghofe@22430
   152
lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
berghofe@22430
   153
  by (auto simp add: SUPR_def intro: Sup_upper)
berghofe@22430
   154
berghofe@22430
   155
lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
berghofe@22430
   156
  by (auto simp add: SUPR_def intro: Sup_least)
berghofe@22430
   157
berghofe@22430
   158
lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
berghofe@22430
   159
  by (auto simp add: INFI_def intro: Inf_lower)
berghofe@22430
   160
berghofe@22430
   161
lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
berghofe@22430
   162
  by (auto simp add: INFI_def intro: Inf_greatest)
berghofe@22430
   163
haftmann@22422
   164
lemma mono_inf: "mono f \<Longrightarrow> f (inf A B) <= inf (f A) (f B)"
nipkow@21312
   165
  by (auto simp add: mono_def)
berghofe@21017
   166
haftmann@22422
   167
lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)"
nipkow@21312
   168
  by (auto simp add: mono_def)
nipkow@21312
   169
berghofe@22430
   170
lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
berghofe@22430
   171
  by (auto intro: order_antisym SUP_leI le_SUPI)
nipkow@21312
   172
berghofe@22430
   173
lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
berghofe@22430
   174
  by (auto intro: order_antisym INF_leI le_INFI)
berghofe@21017
   175
berghofe@21017
   176
berghofe@21017
   177
subsection {* Some instances of the type class of complete lattices *}
berghofe@21017
   178
berghofe@21017
   179
subsubsection {* Booleans *}
berghofe@21017
   180
haftmann@22452
   181
instance bool :: complete_lattice
haftmann@22452
   182
  Inf_bool_def: "Inf A \<equiv> \<forall>x\<in>A. x"
berghofe@21017
   183
  apply intro_classes
haftmann@22422
   184
  apply (unfold Inf_bool_def)
berghofe@21017
   185
  apply (iprover intro!: le_boolI elim: ballE)
berghofe@21017
   186
  apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
berghofe@21017
   187
  done
berghofe@21017
   188
haftmann@22452
   189
theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
berghofe@21017
   190
  apply (rule order_antisym)
nipkow@21312
   191
  apply (rule Sup_least)
berghofe@21017
   192
  apply (rule le_boolI)
berghofe@21017
   193
  apply (erule bexI, assumption)
berghofe@21017
   194
  apply (rule le_boolI)
berghofe@21017
   195
  apply (erule bexE)
berghofe@21017
   196
  apply (rule le_boolE)
nipkow@21312
   197
  apply (rule Sup_upper)
berghofe@21017
   198
  apply assumption+
berghofe@21017
   199
  done
berghofe@21017
   200
haftmann@23108
   201
lemma Inf_empty_bool [simp]:
haftmann@23108
   202
  "Inf {}"
haftmann@23108
   203
  unfolding Inf_bool_def by auto
haftmann@23108
   204
haftmann@23108
   205
lemma not_Sup_empty_bool [simp]:
haftmann@23108
   206
  "\<not> Sup {}"
haftmann@23108
   207
  unfolding Sup_def Inf_bool_def by auto
haftmann@22422
   208
berghofe@21017
   209
subsubsection {* Functions *}
berghofe@21017
   210
haftmann@22452
   211
instance "fun" :: (type, complete_lattice) complete_lattice
haftmann@22452
   212
  Inf_fun_def: "Inf A \<equiv> (\<lambda>x. Inf {y. \<exists>f\<in>A. y = f x})"
berghofe@21017
   213
  apply intro_classes
haftmann@22422
   214
  apply (unfold Inf_fun_def)
berghofe@21017
   215
  apply (rule le_funI)
haftmann@22422
   216
  apply (rule Inf_lower)
berghofe@21017
   217
  apply (rule CollectI)
berghofe@21017
   218
  apply (rule bexI)
berghofe@21017
   219
  apply (rule refl)
berghofe@21017
   220
  apply assumption
berghofe@21017
   221
  apply (rule le_funI)
haftmann@22422
   222
  apply (rule Inf_greatest)
berghofe@21017
   223
  apply (erule CollectE)
berghofe@21017
   224
  apply (erule bexE)
berghofe@21017
   225
  apply (iprover elim: le_funE)
berghofe@21017
   226
  done
berghofe@21017
   227
haftmann@22845
   228
lemmas [code func del] = Inf_fun_def
haftmann@22744
   229
haftmann@22452
   230
theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
berghofe@21017
   231
  apply (rule order_antisym)
nipkow@21312
   232
  apply (rule Sup_least)
berghofe@21017
   233
  apply (rule le_funI)
nipkow@21312
   234
  apply (rule Sup_upper)
berghofe@21017
   235
  apply fast
berghofe@21017
   236
  apply (rule le_funI)
nipkow@21312
   237
  apply (rule Sup_least)
berghofe@21017
   238
  apply (erule CollectE)
berghofe@21017
   239
  apply (erule bexE)
nipkow@21312
   240
  apply (drule le_funD [OF Sup_upper])
berghofe@21017
   241
  apply simp
berghofe@21017
   242
  done
berghofe@21017
   243
haftmann@23131
   244
lemma Inf_empty_fun:
haftmann@23131
   245
  "Inf {} = (\<lambda>_. Inf {})"
haftmann@23108
   246
  by rule (auto simp add: Inf_fun_def)
haftmann@23108
   247
haftmann@23131
   248
lemma Sup_empty_fun:
haftmann@23131
   249
  "Sup {} = (\<lambda>_. Sup {})"
haftmann@23131
   250
proof -
haftmann@23131
   251
  have aux: "\<And>x. {y. \<exists>f. y = f x} = UNIV" by auto
haftmann@23131
   252
  show ?thesis
haftmann@23131
   253
  by (auto simp add: Sup_def Inf_fun_def Inf_binary inf_bool_eq aux)
haftmann@23131
   254
qed
haftmann@23108
   255
haftmann@22452
   256
berghofe@21017
   257
subsubsection {* Sets *}
berghofe@21017
   258
haftmann@22452
   259
instance set :: (type) complete_lattice
haftmann@22452
   260
  Inf_set_def: "Inf S \<equiv> \<Inter>S"
haftmann@22422
   261
  by intro_classes (auto simp add: Inf_set_def)
berghofe@21017
   262
haftmann@22845
   263
lemmas [code func del] = Inf_set_def
haftmann@22744
   264
nipkow@21312
   265
theorem Sup_set_eq: "Sup S = \<Union>S"
berghofe@21017
   266
  apply (rule subset_antisym)
nipkow@21312
   267
  apply (rule Sup_least)
berghofe@21017
   268
  apply (erule Union_upper)
berghofe@21017
   269
  apply (rule Union_least)
nipkow@21312
   270
  apply (erule Sup_upper)
berghofe@21017
   271
  done
berghofe@21017
   272
berghofe@21017
   273
berghofe@21017
   274
subsection {* Least and greatest fixed points *}
berghofe@21017
   275
haftmann@22422
   276
definition
haftmann@22452
   277
  lfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
haftmann@22422
   278
  "lfp f = Inf {u. f u \<le> u}"    --{*least fixed point*}
avigad@17006
   279
haftmann@22422
   280
definition
haftmann@22452
   281
  gfp :: "('a\<Colon>complete_lattice \<Rightarrow> 'a) \<Rightarrow> 'a" where
haftmann@22422
   282
  "gfp f = Sup {u. u \<le> f u}"    --{*greatest fixed point*}
avigad@17006
   283
avigad@17006
   284
haftmann@22918
   285
subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *}
avigad@17006
   286
avigad@17006
   287
text{*@{term "lfp f"} is the least upper bound of 
berghofe@21017
   288
      the set @{term "{u. f(u) \<le> u}"} *}
berghofe@21017
   289
berghofe@21017
   290
lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
haftmann@22422
   291
  by (auto simp add: lfp_def intro: Inf_lower)
berghofe@21017
   292
berghofe@21017
   293
lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f"
haftmann@22422
   294
  by (auto simp add: lfp_def intro: Inf_greatest)
avigad@17006
   295
berghofe@21017
   296
lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f"
berghofe@21017
   297
  by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
avigad@17006
   298
berghofe@21017
   299
lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)"
berghofe@21017
   300
  by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
berghofe@21017
   301
berghofe@21017
   302
lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)"
berghofe@21017
   303
  by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
avigad@17006
   304
krauss@22356
   305
lemma lfp_const: "lfp (\<lambda>x. t) = t"
krauss@22356
   306
  by (rule lfp_unfold) (simp add:mono_def)
krauss@22356
   307
haftmann@22918
   308
haftmann@22918
   309
subsection {* General induction rules for least fixed points *}
avigad@17006
   310
berghofe@21017
   311
theorem lfp_induct:
haftmann@22422
   312
  assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P"
berghofe@21017
   313
  shows "lfp f <= P"
berghofe@21017
   314
proof -
haftmann@22422
   315
  have "inf (lfp f) P <= lfp f" by (rule inf_le1)
haftmann@22422
   316
  with mono have "f (inf (lfp f) P) <= f (lfp f)" ..
berghofe@21017
   317
  also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
haftmann@22422
   318
  finally have "f (inf (lfp f) P) <= lfp f" .
haftmann@22422
   319
  from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI)
haftmann@22422
   320
  hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound)
haftmann@22422
   321
  also have "inf (lfp f) P <= P" by (rule inf_le2)
berghofe@21017
   322
  finally show ?thesis .
berghofe@21017
   323
qed
avigad@17006
   324
berghofe@21017
   325
lemma lfp_induct_set:
avigad@17006
   326
  assumes lfp: "a: lfp(f)"
avigad@17006
   327
      and mono: "mono(f)"
avigad@17006
   328
      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
avigad@17006
   329
  shows "P(a)"
berghofe@21017
   330
  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
haftmann@22422
   331
    (auto simp: inf_set_eq intro: indhyp)
avigad@17006
   332
haftmann@22452
   333
text {* Version of induction for binary relations *}
haftmann@22452
   334
lemmas lfp_induct2 =  lfp_induct_set [of "(a, b)", split_format (complete)]
avigad@17006
   335
avigad@17006
   336
lemma lfp_ordinal_induct: 
avigad@17006
   337
  assumes mono: "mono f"
avigad@17006
   338
  shows "[| !!S. P S ==> P(f S); !!M. !S:M. P S ==> P(Union M) |] 
avigad@17006
   339
         ==> P(lfp f)"
avigad@17006
   340
apply(subgoal_tac "lfp f = Union{S. S \<subseteq> lfp f & P S}")
avigad@17006
   341
 apply (erule ssubst, simp) 
avigad@17006
   342
apply(subgoal_tac "Union{S. S \<subseteq> lfp f & P S} \<subseteq> lfp f")
avigad@17006
   343
 prefer 2 apply blast
avigad@17006
   344
apply(rule equalityI)
avigad@17006
   345
 prefer 2 apply assumption
avigad@17006
   346
apply(drule mono [THEN monoD])
avigad@17006
   347
apply (cut_tac mono [THEN lfp_unfold], simp)
avigad@17006
   348
apply (rule lfp_lowerbound, auto) 
avigad@17006
   349
done
avigad@17006
   350
avigad@17006
   351
avigad@17006
   352
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
avigad@17006
   353
    to control unfolding*}
avigad@17006
   354
avigad@17006
   355
lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
avigad@17006
   356
by (auto intro!: lfp_unfold)
avigad@17006
   357
avigad@17006
   358
lemma def_lfp_induct: 
berghofe@21017
   359
    "[| A == lfp(f); mono(f);
haftmann@22422
   360
        f (inf A P) \<le> P
berghofe@21017
   361
     |] ==> A \<le> P"
berghofe@21017
   362
  by (blast intro: lfp_induct)
berghofe@21017
   363
berghofe@21017
   364
lemma def_lfp_induct_set: 
avigad@17006
   365
    "[| A == lfp(f);  mono(f);   a:A;                    
avigad@17006
   366
        !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)         
avigad@17006
   367
     |] ==> P(a)"
berghofe@21017
   368
  by (blast intro: lfp_induct_set)
avigad@17006
   369
avigad@17006
   370
(*Monotonicity of lfp!*)
berghofe@21017
   371
lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g"
berghofe@21017
   372
  by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans)
avigad@17006
   373
avigad@17006
   374
haftmann@22918
   375
subsection {* Proof of Knaster-Tarski Theorem using @{term gfp} *}
avigad@17006
   376
avigad@17006
   377
text{*@{term "gfp f"} is the greatest lower bound of 
berghofe@21017
   378
      the set @{term "{u. u \<le> f(u)}"} *}
avigad@17006
   379
berghofe@21017
   380
lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
nipkow@21312
   381
  by (auto simp add: gfp_def intro: Sup_upper)
avigad@17006
   382
berghofe@21017
   383
lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
nipkow@21312
   384
  by (auto simp add: gfp_def intro: Sup_least)
avigad@17006
   385
berghofe@21017
   386
lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
berghofe@21017
   387
  by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
avigad@17006
   388
berghofe@21017
   389
lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f"
berghofe@21017
   390
  by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
avigad@17006
   391
berghofe@21017
   392
lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)"
berghofe@21017
   393
  by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
avigad@17006
   394
haftmann@22918
   395
haftmann@22918
   396
subsection {* Coinduction rules for greatest fixed points *}
avigad@17006
   397
avigad@17006
   398
text{*weak version*}
avigad@17006
   399
lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
avigad@17006
   400
by (rule gfp_upperbound [THEN subsetD], auto)
avigad@17006
   401
avigad@17006
   402
lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
avigad@17006
   403
apply (erule gfp_upperbound [THEN subsetD])
avigad@17006
   404
apply (erule imageI)
avigad@17006
   405
done
avigad@17006
   406
avigad@17006
   407
lemma coinduct_lemma:
haftmann@22422
   408
     "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
berghofe@21017
   409
  apply (frule gfp_lemma2)
haftmann@22422
   410
  apply (drule mono_sup)
haftmann@22422
   411
  apply (rule le_supI)
berghofe@21017
   412
  apply assumption
berghofe@21017
   413
  apply (rule order_trans)
berghofe@21017
   414
  apply (rule order_trans)
berghofe@21017
   415
  apply assumption
haftmann@22422
   416
  apply (rule sup_ge2)
berghofe@21017
   417
  apply assumption
berghofe@21017
   418
  done
avigad@17006
   419
avigad@17006
   420
text{*strong version, thanks to Coen and Frost*}
berghofe@21017
   421
lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
haftmann@22422
   422
by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
berghofe@21017
   423
haftmann@22422
   424
lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
berghofe@21017
   425
  apply (rule order_trans)
haftmann@22422
   426
  apply (rule sup_ge1)
berghofe@21017
   427
  apply (erule gfp_upperbound [OF coinduct_lemma])
berghofe@21017
   428
  apply assumption
berghofe@21017
   429
  done
avigad@17006
   430
avigad@17006
   431
lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
avigad@17006
   432
by (blast dest: gfp_lemma2 mono_Un)
avigad@17006
   433
haftmann@22918
   434
haftmann@22918
   435
subsection {* Even Stronger Coinduction Rule, by Martin Coen *}
avigad@17006
   436
avigad@17006
   437
text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
avigad@17006
   438
  @{term lfp} and @{term gfp}*}
avigad@17006
   439
avigad@17006
   440
lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
nipkow@17589
   441
by (iprover intro: subset_refl monoI Un_mono monoD)
avigad@17006
   442
avigad@17006
   443
lemma coinduct3_lemma:
avigad@17006
   444
     "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |]
avigad@17006
   445
      ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))"
avigad@17006
   446
apply (rule subset_trans)
avigad@17006
   447
apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
avigad@17006
   448
apply (rule Un_least [THEN Un_least])
avigad@17006
   449
apply (rule subset_refl, assumption)
avigad@17006
   450
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
avigad@17006
   451
apply (rule monoD, assumption)
avigad@17006
   452
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
avigad@17006
   453
done
avigad@17006
   454
avigad@17006
   455
lemma coinduct3: 
avigad@17006
   456
  "[| mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
avigad@17006
   457
apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
avigad@17006
   458
apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto)
avigad@17006
   459
done
avigad@17006
   460
avigad@17006
   461
avigad@17006
   462
text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, 
avigad@17006
   463
    to control unfolding*}
avigad@17006
   464
avigad@17006
   465
lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
avigad@17006
   466
by (auto intro!: gfp_unfold)
avigad@17006
   467
avigad@17006
   468
lemma def_coinduct:
haftmann@22422
   469
     "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
berghofe@21017
   470
by (iprover intro!: coinduct)
berghofe@21017
   471
berghofe@21017
   472
lemma def_coinduct_set:
avigad@17006
   473
     "[| A==gfp(f);  mono(f);  a:X;  X \<subseteq> f(X Un A) |] ==> a: A"
berghofe@21017
   474
by (auto intro!: coinduct_set)
avigad@17006
   475
avigad@17006
   476
(*The version used in the induction/coinduction package*)
avigad@17006
   477
lemma def_Collect_coinduct:
avigad@17006
   478
    "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));   
avigad@17006
   479
        a: X;  !!z. z: X ==> P (X Un A) z |] ==>  
avigad@17006
   480
     a : A"
berghofe@21017
   481
apply (erule def_coinduct_set, auto) 
avigad@17006
   482
done
avigad@17006
   483
avigad@17006
   484
lemma def_coinduct3:
avigad@17006
   485
    "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
avigad@17006
   486
by (auto intro!: coinduct3)
avigad@17006
   487
avigad@17006
   488
text{*Monotonicity of @{term gfp}!*}
berghofe@21017
   489
lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
berghofe@21017
   490
  by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
avigad@17006
   491
avigad@17006
   492
ML
avigad@17006
   493
{*
avigad@17006
   494
val lfp_def = thm "lfp_def";
avigad@17006
   495
val lfp_lowerbound = thm "lfp_lowerbound";
avigad@17006
   496
val lfp_greatest = thm "lfp_greatest";
avigad@17006
   497
val lfp_unfold = thm "lfp_unfold";
avigad@17006
   498
val lfp_induct = thm "lfp_induct";
avigad@17006
   499
val lfp_induct2 = thm "lfp_induct2";
avigad@17006
   500
val lfp_ordinal_induct = thm "lfp_ordinal_induct";
avigad@17006
   501
val def_lfp_unfold = thm "def_lfp_unfold";
avigad@17006
   502
val def_lfp_induct = thm "def_lfp_induct";
berghofe@21017
   503
val def_lfp_induct_set = thm "def_lfp_induct_set";
avigad@17006
   504
val lfp_mono = thm "lfp_mono";
avigad@17006
   505
val gfp_def = thm "gfp_def";
avigad@17006
   506
val gfp_upperbound = thm "gfp_upperbound";
avigad@17006
   507
val gfp_least = thm "gfp_least";
avigad@17006
   508
val gfp_unfold = thm "gfp_unfold";
avigad@17006
   509
val weak_coinduct = thm "weak_coinduct";
avigad@17006
   510
val weak_coinduct_image = thm "weak_coinduct_image";
avigad@17006
   511
val coinduct = thm "coinduct";
avigad@17006
   512
val gfp_fun_UnI2 = thm "gfp_fun_UnI2";
avigad@17006
   513
val coinduct3 = thm "coinduct3";
avigad@17006
   514
val def_gfp_unfold = thm "def_gfp_unfold";
avigad@17006
   515
val def_coinduct = thm "def_coinduct";
avigad@17006
   516
val def_Collect_coinduct = thm "def_Collect_coinduct";
avigad@17006
   517
val def_coinduct3 = thm "def_coinduct3";
avigad@17006
   518
val gfp_mono = thm "gfp_mono";
berghofe@21017
   519
val le_funI = thm "le_funI";
berghofe@21017
   520
val le_boolI = thm "le_boolI";
berghofe@21017
   521
val le_boolI' = thm "le_boolI'";
haftmann@22422
   522
val inf_fun_eq = thm "inf_fun_eq";
haftmann@22422
   523
val inf_bool_eq = thm "inf_bool_eq";
berghofe@21017
   524
val le_funE = thm "le_funE";
berghofe@22276
   525
val le_funD = thm "le_funD";
berghofe@21017
   526
val le_boolE = thm "le_boolE";
berghofe@21017
   527
val le_boolD = thm "le_boolD";
berghofe@21017
   528
val le_bool_def = thm "le_bool_def";
berghofe@21017
   529
val le_fun_def = thm "le_fun_def";
avigad@17006
   530
*}
avigad@17006
   531
avigad@17006
   532
end