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