src/ZF/Fixedpt.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46820 c656222c4dc1
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 24893
diff changeset
     1
(*  Title:      ZF/Fixedpt.thy
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13220
diff changeset
     6
header{*Least and Greatest Fixed Points; the Knaster-Tarski Theorem*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13220
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14046
diff changeset
     8
theory Fixedpt imports equalities begin
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
     9
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    10
definition 
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    11
  (*monotone operator from Pow(D) to itself*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    12
  bnd_mono :: "[i,i=>i]=>o"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    13
     "bnd_mono(D,h) == h(D)<=D & (\<forall>W X. W<=X \<longrightarrow> X<=D \<longrightarrow> h(W) \<subseteq> h(X))"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    14
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
definition 
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    16
  lfp      :: "[i,i=>i]=>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    17
     "lfp(D,h) == \<Inter>({X: Pow(D). h(X) \<subseteq> X})"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    18
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    19
definition 
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    20
  gfp      :: "[i,i=>i]=>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    21
     "gfp(D,h) == \<Union>({X: Pow(D). X \<subseteq> h(X)})"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    22
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
    23
text{*The theorem is proved in the lattice of subsets of @{term D}, 
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
    24
      namely @{term "Pow(D)"}, with Inter as the greatest lower bound.*}
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    25
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13220
diff changeset
    26
subsection{*Monotone Operators*}
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    27
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    28
lemma bnd_monoI:
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    29
    "[| h(D)<=D;   
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    30
        !!W X. [| W<=D;  X<=D;  W<=X |] ==> h(W) \<subseteq> h(X)   
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    31
     |] ==> bnd_mono(D,h)"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    32
by (unfold bnd_mono_def, clarify, blast)  
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    33
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    34
lemma bnd_monoD1: "bnd_mono(D,h) ==> h(D) \<subseteq> D"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    35
apply (unfold bnd_mono_def)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    36
apply (erule conjunct1)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    37
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    38
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    39
lemma bnd_monoD2: "[| bnd_mono(D,h);  W<=X;  X<=D |] ==> h(W) \<subseteq> h(X)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    40
by (unfold bnd_mono_def, blast)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    41
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    42
lemma bnd_mono_subset:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    43
    "[| bnd_mono(D,h);  X<=D |] ==> h(X) \<subseteq> D"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    44
by (unfold bnd_mono_def, clarify, blast) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    45
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    46
lemma bnd_mono_Un:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    47
     "[| bnd_mono(D,h);  A \<subseteq> D;  B \<subseteq> D |] ==> h(A) \<union> h(B) \<subseteq> h(A \<union> B)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    48
apply (unfold bnd_mono_def)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    49
apply (rule Un_least, blast+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    50
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    51
13220
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    52
(*unused*)
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    53
lemma bnd_mono_UN:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    54
     "[| bnd_mono(D,h);  \<forall>i\<in>I. A(i) \<subseteq> D |] 
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    55
      ==> (\<Union>i\<in>I. h(A(i))) \<subseteq> h((\<Union>i\<in>I. A(i)))"
13220
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    56
apply (unfold bnd_mono_def) 
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    57
apply (rule UN_least)
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    58
apply (elim conjE) 
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    59
apply (drule_tac x="A(i)" in spec)
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    60
apply (drule_tac x="(\<Union>i\<in>I. A(i))" in spec) 
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    61
apply blast 
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    62
done
62c899c77151 tidying
paulson
parents: 13218
diff changeset
    63
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    64
(*Useful??*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    65
lemma bnd_mono_Int:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    66
     "[| bnd_mono(D,h);  A \<subseteq> D;  B \<subseteq> D |] ==> h(A \<inter> B) \<subseteq> h(A) \<inter> h(B)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    67
apply (rule Int_greatest) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    68
apply (erule bnd_monoD2, rule Int_lower1, assumption) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    69
apply (erule bnd_monoD2, rule Int_lower2, assumption) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    70
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    71
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
    72
subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    73
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    74
(*lfp is contained in each pre-fixedpoint*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    75
lemma lfp_lowerbound: 
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    76
    "[| h(A) \<subseteq> A;  A<=D |] ==> lfp(D,h) \<subseteq> A"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    77
by (unfold lfp_def, blast)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    78
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    79
(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    80
lemma lfp_subset: "lfp(D,h) \<subseteq> D"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    81
by (unfold lfp_def Inter_def, blast)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    82
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    83
(*Used in datatype package*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    84
lemma def_lfp_subset:  "A == lfp(D,h) ==> A \<subseteq> D"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    85
apply simp
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    86
apply (rule lfp_subset)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    87
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    88
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    89
lemma lfp_greatest:  
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    90
    "[| h(D) \<subseteq> D;  !!X. [| h(X) \<subseteq> X;  X<=D |] ==> A<=X |] ==> A \<subseteq> lfp(D,h)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    91
by (unfold lfp_def, blast) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    92
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    93
lemma lfp_lemma1:  
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    94
    "[| bnd_mono(D,h);  h(A)<=A;  A<=D |] ==> h(lfp(D,h)) \<subseteq> A"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    95
apply (erule bnd_monoD2 [THEN subset_trans])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    96
apply (rule lfp_lowerbound, assumption+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
    97
done
3923
c257b82a1200 global;
wenzelm
parents: 2469
diff changeset
    98
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
    99
lemma lfp_lemma2: "bnd_mono(D,h) ==> h(lfp(D,h)) \<subseteq> lfp(D,h)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   100
apply (rule bnd_monoD1 [THEN lfp_greatest])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   101
apply (rule_tac [2] lfp_lemma1)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   102
apply (assumption+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   103
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   104
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   105
lemma lfp_lemma3: 
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   106
    "bnd_mono(D,h) ==> lfp(D,h) \<subseteq> h(lfp(D,h))"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   107
apply (rule lfp_lowerbound)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   108
apply (rule bnd_monoD2, assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   109
apply (rule lfp_lemma2, assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   110
apply (erule_tac [2] bnd_mono_subset)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   111
apply (rule lfp_subset)+
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   112
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   113
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   114
lemma lfp_unfold: "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   115
apply (rule equalityI) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   116
apply (erule lfp_lemma3) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   117
apply (erule lfp_lemma2) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   118
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   119
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   120
(*Definition form, to control unfolding*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   121
lemma def_lfp_unfold:
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   122
    "[| A==lfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   123
apply simp
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   124
apply (erule lfp_unfold)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   125
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   126
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13220
diff changeset
   127
subsection{*General Induction Rule for Least Fixedpoints*}
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   128
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   129
lemma Collect_is_pre_fixedpt:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   130
    "[| bnd_mono(D,h);  !!x. x \<in> h(Collect(lfp(D,h),P)) ==> P(x) |]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   131
     ==> h(Collect(lfp(D,h),P)) \<subseteq> Collect(lfp(D,h),P)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   132
by (blast intro: lfp_lemma2 [THEN subsetD] bnd_monoD2 [THEN subsetD] 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   133
                 lfp_subset [THEN subsetD]) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   134
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   135
(*This rule yields an induction hypothesis in which the components of a
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   136
  data structure may be assumed to be elements of lfp(D,h)*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   137
lemma induct:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   138
    "[| bnd_mono(D,h);  a \<in> lfp(D,h);                    
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   139
        !!x. x \<in> h(Collect(lfp(D,h),P)) ==> P(x)         
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   140
     |] ==> P(a)"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   141
apply (rule Collect_is_pre_fixedpt
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   142
              [THEN lfp_lowerbound, THEN subsetD, THEN CollectD2])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   143
apply (rule_tac [3] lfp_subset [THEN Collect_subset [THEN subset_trans]], 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   144
       blast+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   145
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   146
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   147
(*Definition form, to control unfolding*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   148
lemma def_induct:
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   149
    "[| A == lfp(D,h);  bnd_mono(D,h);  a:A;    
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   150
        !!x. x \<in> h(Collect(A,P)) ==> P(x)  
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   151
     |] ==> P(a)"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   152
by (rule induct, blast+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   153
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   154
(*This version is useful when "A" is not a subset of D
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   155
  second premise could simply be h(D \<inter> A) \<subseteq> D or !!X. X<=D ==> h(X)<=D *)
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   156
lemma lfp_Int_lowerbound:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   157
    "[| h(D \<inter> A) \<subseteq> A;  bnd_mono(D,h) |] ==> lfp(D,h) \<subseteq> A" 
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   158
apply (rule lfp_lowerbound [THEN subset_trans])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   159
apply (erule bnd_mono_subset [THEN Int_greatest], blast+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   160
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   161
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   162
(*Monotonicity of lfp, where h precedes i under a domain-like partial order
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   163
  monotonicity of h is not strictly necessary; h must be bounded by D*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   164
lemma lfp_mono:
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   165
  assumes hmono: "bnd_mono(D,h)"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   166
      and imono: "bnd_mono(E,i)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   167
      and subhi: "!!X. X<=D ==> h(X) \<subseteq> i(X)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   168
    shows "lfp(D,h) \<subseteq> lfp(E,i)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   169
apply (rule bnd_monoD1 [THEN lfp_greatest])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   170
apply (rule imono)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   171
apply (rule hmono [THEN [2] lfp_Int_lowerbound])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   172
apply (rule Int_lower1 [THEN subhi, THEN subset_trans])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   173
apply (rule imono [THEN bnd_monoD2, THEN subset_trans], auto) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   174
done
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   176
(*This (unused) version illustrates that monotonicity is not really needed,
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   177
  but both lfp's must be over the SAME set D;  Inter is anti-monotonic!*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   178
lemma lfp_mono2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   179
    "[| i(D) \<subseteq> D;  !!X. X<=D ==> h(X) \<subseteq> i(X)  |] ==> lfp(D,h) \<subseteq> lfp(D,i)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   180
apply (rule lfp_greatest, assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   181
apply (rule lfp_lowerbound, blast, assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   182
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   183
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
   184
lemma lfp_cong:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   185
     "[|D=D'; !!X. X \<subseteq> D' ==> h(X) = h'(X)|] ==> lfp(D,h) = lfp(D',h')"
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
   186
apply (simp add: lfp_def)
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
   187
apply (rule_tac t=Inter in subst_context)
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
   188
apply (rule Collect_cong, simp_all) 
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
   189
done 
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   190
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
   191
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13356
diff changeset
   192
subsection{*Proof of Knaster-Tarski Theorem using @{term gfp}*}
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   193
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   194
(*gfp contains each post-fixedpoint that is contained in D*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   195
lemma gfp_upperbound: "[| A \<subseteq> h(A);  A<=D |] ==> A \<subseteq> gfp(D,h)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   196
apply (unfold gfp_def)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   197
apply (rule PowI [THEN CollectI, THEN Union_upper])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   198
apply (assumption+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   199
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   200
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   201
lemma gfp_subset: "gfp(D,h) \<subseteq> D"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   202
by (unfold gfp_def, blast)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   203
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   204
(*Used in datatype package*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   205
lemma def_gfp_subset: "A==gfp(D,h) ==> A \<subseteq> D"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   206
apply simp
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   207
apply (rule gfp_subset)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   208
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   209
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   210
lemma gfp_least: 
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   211
    "[| bnd_mono(D,h);  !!X. [| X \<subseteq> h(X);  X<=D |] ==> X<=A |] ==>  
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   212
     gfp(D,h) \<subseteq> A"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   213
apply (unfold gfp_def)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   214
apply (blast dest: bnd_monoD1) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   215
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   216
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   217
lemma gfp_lemma1: 
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   218
    "[| bnd_mono(D,h);  A<=h(A);  A<=D |] ==> A \<subseteq> h(gfp(D,h))"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   219
apply (rule subset_trans, assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   220
apply (erule bnd_monoD2)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   221
apply (rule_tac [2] gfp_subset)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   222
apply (simp add: gfp_upperbound)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   223
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   224
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   225
lemma gfp_lemma2: "bnd_mono(D,h) ==> gfp(D,h) \<subseteq> h(gfp(D,h))"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   226
apply (rule gfp_least)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   227
apply (rule_tac [2] gfp_lemma1)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   228
apply (assumption+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   229
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   230
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   231
lemma gfp_lemma3: 
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   232
    "bnd_mono(D,h) ==> h(gfp(D,h)) \<subseteq> gfp(D,h)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   233
apply (rule gfp_upperbound)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   234
apply (rule bnd_monoD2, assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   235
apply (rule gfp_lemma2, assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   236
apply (erule bnd_mono_subset, rule gfp_subset)+
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   237
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   238
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   239
lemma gfp_unfold: "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   240
apply (rule equalityI) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   241
apply (erule gfp_lemma2) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   242
apply (erule gfp_lemma3) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   243
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   244
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   245
(*Definition form, to control unfolding*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   246
lemma def_gfp_unfold:
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   247
    "[| A==gfp(D,h);  bnd_mono(D,h) |] ==> A = h(A)"
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   248
apply simp
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   249
apply (erule gfp_unfold)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   250
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   251
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   252
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13220
diff changeset
   253
subsection{*Coinduction Rules for Greatest Fixed Points*}
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   254
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   255
(*weak version*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   256
lemma weak_coinduct: "[| a: X;  X \<subseteq> h(X);  X \<subseteq> D |] ==> a \<in> gfp(D,h)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   257
by (blast intro: gfp_upperbound [THEN subsetD])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   259
lemma coinduct_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   260
    "[| X \<subseteq> h(X \<union> gfp(D,h));  X \<subseteq> D;  bnd_mono(D,h) |] ==>   
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   261
     X \<union> gfp(D,h) \<subseteq> h(X \<union> gfp(D,h))"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   262
apply (erule Un_least)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   263
apply (rule gfp_lemma2 [THEN subset_trans], assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   264
apply (rule Un_upper2 [THEN subset_trans])
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   265
apply (rule bnd_mono_Un, assumption+) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   266
apply (rule gfp_subset)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   267
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   268
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   269
(*strong version*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   270
lemma coinduct:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   271
     "[| bnd_mono(D,h);  a: X;  X \<subseteq> h(X \<union> gfp(D,h));  X \<subseteq> D |]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   272
      ==> a \<in> gfp(D,h)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   273
apply (rule weak_coinduct)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   274
apply (erule_tac [2] coinduct_lemma)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   275
apply (simp_all add: gfp_subset Un_subset_iff) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   276
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   277
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   278
(*Definition form, to control unfolding*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   279
lemma def_coinduct:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   280
    "[| A == gfp(D,h);  bnd_mono(D,h);  a: X;  X \<subseteq> h(X \<union> A);  X \<subseteq> D |] ==>  
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   281
     a \<in> A"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   282
apply simp
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   283
apply (rule coinduct, assumption+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   284
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   285
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   286
(*The version used in the induction/coinduction package*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   287
lemma def_Collect_coinduct:
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   288
    "[| A == gfp(D, %w. Collect(D,P(w)));  bnd_mono(D, %w. Collect(D,P(w)));   
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   289
        a: X;  X \<subseteq> D;  !!z. z: X ==> P(X \<union> A, z) |] ==>  
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   290
     a \<in> A"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   291
apply (rule def_coinduct, assumption+, blast+)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   292
done
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   294
(*Monotonicity of gfp!*)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   295
lemma gfp_mono:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   296
    "[| bnd_mono(D,h);  D \<subseteq> E;                  
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 35762
diff changeset
   297
        !!X. X<=D ==> h(X) \<subseteq> i(X)  |] ==> gfp(D,h) \<subseteq> gfp(E,i)"
13218
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   298
apply (rule gfp_upperbound)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   299
apply (rule gfp_lemma2 [THEN subset_trans], assumption)
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   300
apply (blast del: subsetI intro: gfp_subset) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   301
apply (blast del: subsetI intro: subset_trans gfp_subset) 
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   302
done
3732064ccbd1 conversion of Fixedpt to Isar script
paulson
parents: 13168
diff changeset
   303
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
end