src/CCL/Gfp.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 21404 eb85850d3eb7
child 32153 a0e57fb1b930
permissions -rw-r--r--
merged
     1 (*  Title:      CCL/Gfp.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 *)
     6 
     7 header {* Greatest fixed points *}
     8 
     9 theory Gfp
    10 imports Lfp
    11 begin
    12 
    13 definition
    14   gfp :: "['a set=>'a set] => 'a set" where -- "greatest fixed point"
    15   "gfp(f) == Union({u. u <= f(u)})"
    16 
    17 (* gfp(f) is the least upper bound of {u. u <= f(u)} *)
    18 
    19 lemma gfp_upperbound: "[| A <= f(A) |] ==> A <= gfp(f)"
    20   unfolding gfp_def by blast
    21 
    22 lemma gfp_least: "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A"
    23   unfolding gfp_def by blast
    24 
    25 lemma gfp_lemma2: "mono(f) ==> gfp(f) <= f(gfp(f))"
    26   by (rule gfp_least, rule subset_trans, assumption, erule monoD,
    27     rule gfp_upperbound, assumption)
    28 
    29 lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) <= gfp(f)"
    30   by (rule gfp_upperbound, frule monoD, rule gfp_lemma2, assumption+)
    31 
    32 lemma gfp_Tarski: "mono(f) ==> gfp(f) = f(gfp(f))"
    33   by (rule equalityI gfp_lemma2 gfp_lemma3 | assumption)+
    34 
    35 
    36 (*** Coinduction rules for greatest fixed points ***)
    37 
    38 (*weak version*)
    39 lemma coinduct: "[| a: A;  A <= f(A) |] ==> a : gfp(f)"
    40   by (blast dest: gfp_upperbound)
    41 
    42 lemma coinduct2_lemma:
    43   "[| A <= f(A) Un gfp(f);  mono(f) |] ==>   
    44     A Un gfp(f) <= f(A Un gfp(f))"
    45   apply (rule subset_trans)
    46    prefer 2
    47    apply (erule mono_Un)
    48   apply (rule subst, erule gfp_Tarski)
    49   apply (erule Un_least)
    50   apply (rule Un_upper2)
    51   done
    52 
    53 (*strong version, thanks to Martin Coen*)
    54 lemma coinduct2:
    55   "[| a: A;  A <= f(A) Un gfp(f);  mono(f) |] ==> a : gfp(f)"
    56   apply (rule coinduct)
    57    prefer 2
    58    apply (erule coinduct2_lemma, assumption)
    59   apply blast
    60   done
    61 
    62 (***  Even Stronger version of coinduct  [by Martin Coen]
    63          - instead of the condition  A <= f(A)
    64                            consider  A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***)
    65 
    66 lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un A Un B)"
    67   by (rule monoI) (blast dest: monoD)
    68 
    69 lemma coinduct3_lemma:
    70   assumes prem: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))"
    71     and mono: "mono(f)"
    72   shows "lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))"
    73   apply (rule subset_trans)
    74    apply (rule mono [THEN coinduct3_mono_lemma, THEN lfp_lemma3])
    75   apply (rule Un_least [THEN Un_least])
    76     apply (rule subset_refl)
    77    apply (rule prem)
    78   apply (rule mono [THEN gfp_Tarski, THEN equalityD1, THEN subset_trans])
    79   apply (rule mono [THEN monoD])
    80   apply (subst mono [THEN coinduct3_mono_lemma, THEN lfp_Tarski])
    81   apply (rule Un_upper2)
    82   done
    83 
    84 lemma coinduct3:
    85   assumes 1: "a:A"
    86     and 2: "A <= f(lfp(%x. f(x) Un A Un gfp(f)))"
    87     and 3: "mono(f)"
    88   shows "a : gfp(f)"
    89   apply (rule coinduct)
    90    prefer 2
    91    apply (rule coinduct3_lemma [OF 2 3])
    92   apply (subst lfp_Tarski [OF coinduct3_mono_lemma, OF 3])
    93   using 1 apply blast
    94   done
    95 
    96 
    97 subsection {* Definition forms of @{text "gfp_Tarski"}, to control unfolding *}
    98 
    99 lemma def_gfp_Tarski: "[| h==gfp(f);  mono(f) |] ==> h = f(h)"
   100   apply unfold
   101   apply (erule gfp_Tarski)
   102   done
   103 
   104 lemma def_coinduct: "[| h==gfp(f);  a:A;  A <= f(A) |] ==> a: h"
   105   apply unfold
   106   apply (erule coinduct)
   107   apply assumption
   108   done
   109 
   110 lemma def_coinduct2: "[| h==gfp(f);  a:A;  A <= f(A) Un h; mono(f) |] ==> a: h"
   111   apply unfold
   112   apply (erule coinduct2)
   113    apply assumption
   114   apply assumption
   115   done
   116 
   117 lemma def_coinduct3: "[| h==gfp(f);  a:A;  A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h"
   118   apply unfold
   119   apply (erule coinduct3)
   120    apply assumption
   121   apply assumption
   122   done
   123 
   124 (*Monotonicity of gfp!*)
   125 lemma gfp_mono: "[| mono(f);  !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)"
   126   apply (rule gfp_upperbound)
   127   apply (rule subset_trans)
   128    apply (rule gfp_lemma2)
   129    apply assumption
   130   apply (erule meta_spec)
   131   done
   132 
   133 end