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