src/CCL/Gfp.thy
changeset 20140 98acc6d0fab6
parent 17456 bcf7544875b2
child 21404 eb85850d3eb7
equal deleted inserted replaced
20139:804927db5311 20140:98acc6d0fab6
     8 
     8 
     9 theory Gfp
     9 theory Gfp
    10 imports Lfp
    10 imports Lfp
    11 begin
    11 begin
    12 
    12 
    13 constdefs
    13 definition
    14   gfp :: "['a set=>'a set] => 'a set"    (*greatest fixed point*)
    14   gfp :: "['a set=>'a set] => 'a set"    (*greatest fixed point*)
    15   "gfp(f) == Union({u. u <= f(u)})"
    15   "gfp(f) == Union({u. u <= f(u)})"
    16 
    16 
    17 ML {* use_legacy_bindings (the_context ()) *}
    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
    18 
   132 
    19 end
   133 end