src/HOL/Lfp.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15386 06757406d8cf
permissions -rw-r--r--
Constant "If" is now local
clasohm@1475
     1
(*  Title:      HOL/Lfp.thy
clasohm@923
     2
    ID:         $Id$
clasohm@1475
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1992  University of Cambridge
paulson@15386
     5
*)
clasohm@923
     6
paulson@15386
     7
header{*Least Fixed Points and the Knaster-Tarski Theorem*}
clasohm@923
     8
nipkow@15131
     9
theory Lfp
nipkow@15140
    10
imports Product_Type
nipkow@15131
    11
begin
clasohm@1558
    12
clasohm@1558
    13
constdefs
skalberg@14169
    14
  lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
paulson@15386
    15
    "lfp(f) == Inter({u. f(u) \<subseteq> u})"    --{*least fixed point*}
paulson@15386
    16
paulson@15386
    17
paulson@15386
    18
paulson@15386
    19
subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
paulson@15386
    20
paulson@15386
    21
paulson@15386
    22
text{*@{term "lfp f"} is the least upper bound of 
paulson@15386
    23
      the set @{term "{u. f(u) \<subseteq> u}"} *}
paulson@15386
    24
paulson@15386
    25
lemma lfp_lowerbound: "f(A) \<subseteq> A ==> lfp(f) \<subseteq> A"
paulson@15386
    26
by (auto simp add: lfp_def)
paulson@15386
    27
paulson@15386
    28
lemma lfp_greatest: "[| !!u. f(u) \<subseteq> u ==> A\<subseteq>u |] ==> A \<subseteq> lfp(f)"
paulson@15386
    29
by (auto simp add: lfp_def)
paulson@15386
    30
paulson@15386
    31
lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) \<subseteq> lfp(f)"
paulson@15386
    32
by (rules intro: lfp_greatest subset_trans monoD lfp_lowerbound)
paulson@15386
    33
paulson@15386
    34
lemma lfp_lemma3: "mono(f) ==> lfp(f) \<subseteq> f(lfp(f))"
paulson@15386
    35
by (rules intro: lfp_lemma2 monoD lfp_lowerbound)
paulson@15386
    36
paulson@15386
    37
lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))"
paulson@15386
    38
by (rules intro: equalityI lfp_lemma2 lfp_lemma3)
paulson@15386
    39
paulson@15386
    40
subsection{*General induction rules for greatest fixed points*}
paulson@15386
    41
paulson@15386
    42
lemma lfp_induct: 
paulson@15386
    43
  assumes lfp: "a: lfp(f)"
paulson@15386
    44
      and mono: "mono(f)"
paulson@15386
    45
      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
paulson@15386
    46
  shows "P(a)"
paulson@15386
    47
apply (rule_tac a=a in Int_lower2 [THEN subsetD, THEN CollectD]) 
paulson@15386
    48
apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]]) 
paulson@15386
    49
apply (rule Int_greatest)
paulson@15386
    50
 apply (rule subset_trans [OF Int_lower1 [THEN mono [THEN monoD]]
paulson@15386
    51
                              mono [THEN lfp_lemma2]]) 
paulson@15386
    52
apply (blast intro: indhyp) 
paulson@15386
    53
done
paulson@15386
    54
paulson@15386
    55
paulson@15386
    56
text{*Version of induction for binary relations*}
paulson@15386
    57
lemmas lfp_induct2 =  lfp_induct [of "(a,b)", split_format (complete)]
paulson@15386
    58
paulson@15386
    59
paulson@15386
    60
lemma lfp_ordinal_induct: 
paulson@15386
    61
  assumes mono: "mono f"
paulson@15386
    62
  shows "[| !!S. P S ==> P(f S); !!M. !S:M. P S ==> P(Union M) |] 
paulson@15386
    63
         ==> P(lfp f)"
paulson@15386
    64
apply(subgoal_tac "lfp f = Union{S. S \<subseteq> lfp f & P S}")
paulson@15386
    65
 apply (erule ssubst, simp) 
paulson@15386
    66
apply(subgoal_tac "Union{S. S \<subseteq> lfp f & P S} \<subseteq> lfp f")
paulson@15386
    67
 prefer 2 apply blast
paulson@15386
    68
apply(rule equalityI)
paulson@15386
    69
 prefer 2 apply assumption
paulson@15386
    70
apply(drule mono [THEN monoD])
paulson@15386
    71
apply (cut_tac mono [THEN lfp_unfold], simp)
paulson@15386
    72
apply (rule lfp_lowerbound, auto) 
paulson@15386
    73
done
paulson@15386
    74
paulson@15386
    75
paulson@15386
    76
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
paulson@15386
    77
    to control unfolding*}
paulson@15386
    78
paulson@15386
    79
lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
paulson@15386
    80
by (auto intro!: lfp_unfold)
paulson@15386
    81
paulson@15386
    82
lemma def_lfp_induct: 
paulson@15386
    83
    "[| A == lfp(f);  mono(f);   a:A;                    
paulson@15386
    84
        !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)         
paulson@15386
    85
     |] ==> P(a)"
paulson@15386
    86
by (blast intro: lfp_induct)
paulson@15386
    87
paulson@15386
    88
(*Monotonicity of lfp!*)
paulson@15386
    89
lemma lfp_mono: "[| !!Z. f(Z)\<subseteq>g(Z) |] ==> lfp(f) \<subseteq> lfp(g)"
paulson@15386
    90
by (rule lfp_lowerbound [THEN lfp_greatest], blast)
paulson@15386
    91
paulson@15386
    92
paulson@15386
    93
ML
paulson@15386
    94
{*
paulson@15386
    95
val lfp_def = thm "lfp_def";
paulson@15386
    96
val lfp_lowerbound = thm "lfp_lowerbound";
paulson@15386
    97
val lfp_greatest = thm "lfp_greatest";
paulson@15386
    98
val lfp_unfold = thm "lfp_unfold";
paulson@15386
    99
val lfp_induct = thm "lfp_induct";
paulson@15386
   100
val lfp_induct2 = thm "lfp_induct2";
paulson@15386
   101
val lfp_ordinal_induct = thm "lfp_ordinal_induct";
paulson@15386
   102
val def_lfp_unfold = thm "def_lfp_unfold";
paulson@15386
   103
val def_lfp_induct = thm "def_lfp_induct";
paulson@15386
   104
val lfp_mono = thm "lfp_mono";
paulson@15386
   105
*}
clasohm@1558
   106
clasohm@923
   107
end