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