src/CCL/Gfp.thy
 changeset 20140 98acc6d0fab6 parent 17456 bcf7544875b2 child 21404 eb85850d3eb7
equal 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`