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
```