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