fixedPointScript.sml

1(* Fixed-points over sets ordered by subset.  Basically, a set-specific
2   instantiation of the general theory in posetTheory
3*)
4Theory fixedPoint[bare]
5Ancestors
6  poset pred_set
7Libs
8  HolKernel Parse boolLib BasicProvers simpLib boolSimps
9  pred_setLib
10
11
12Definition monotone_def[nocompute]:
13  monotone f = !X Y. X SUBSET Y ==> f X SUBSET f Y
14End
15
16val _ = app (ignore o hide) ["lfp", "gfp"]
17Overload po_lfp = “poset$lfp”
18Overload po_gfp = “poset$gfp”
19Definition lfp_def[nocompute]:
20  lfp f = BIGINTER { X | f X SUBSET X }
21End
22
23Definition gfp_def[nocompute]:
24  gfp f = BIGUNION { X | X SUBSET f X }
25End
26
27Definition closed_def[nocompute]:
28  closed f X <=> f X SUBSET X
29End
30
31Definition dense_def[nocompute]:
32  dense f X <=> X SUBSET f X
33End
34
35Theorem SUBSET_poset[simp]:
36  poset (UNIV, $SUBSET)
37Proof
38  SIMP_TAC (srw_ss()) [poset_def] >>
39  PROVE_TAC[SUBSET_ANTISYM, SUBSET_TRANS]
40QED
41
42Theorem SUBSET_complete[simp]:
43  complete (UNIV, $SUBSET)
44Proof
45  SIMP_TAC (srw_ss()) [complete_def, lub_def, glb_def] >>
46  Q.X_GEN_TAC ‘C’ >> conj_tac
47  >- (Q.EXISTS_TAC ‘BIGUNION C’ >> conj_tac
48      >- REWRITE_TAC[SIMP_RULE(srw_ss()) [IN_DEF] SUBSET_BIGUNION_I] >>
49      SIMP_TAC (srw_ss()) [SUBSET_DEF, IN_DEF] >> PROVE_TAC[]) >>
50  Q.EXISTS_TAC ‘BIGINTER C’ >> SIMP_TAC (srw_ss()) [SUBSET_DEF, IN_DEF]
51QED
52
53Theorem monotonic_monotone[simp]:
54  monotonic (UNIV, $SUBSET) f <=> monotone f
55Proof
56  SIMP_TAC (srw_ss())[monotone_def, monotonic_def]
57QED
58
59Theorem lfp_least_closed:
60  !f. monotone f ==> closed f (lfp f) /\ !X. closed f X ==> lfp f SUBSET X
61Proof
62  rpt strip_tac >> rewrite_tac [lfp_def]
63  >- (SIMP_TAC (srw_ss()) [closed_def] >> irule SUBSET_TRANS >>
64      Q.EXISTS_TAC ‘BIGINTER { f X | X | f X SUBSET X }’ >>
65      CONJ_TAC THENL [
66        SIMP_TAC (srw_ss()) [SUBSET_BIGINTER] >> REPEAT STRIP_TAC >>
67        FIRST_X_ASSUM SUBST_ALL_TAC >>
68        ‘BIGINTER { X | f X SUBSET X } SUBSET X’
69          suffices_by PROVE_TAC [monotone_def] >>
70        ONCE_REWRITE_TAC [SUBSET_DEF] >> ASM_SIMP_TAC (srw_ss()) [],
71        ASM_SIMP_TAC (srw_ss()) [SUBSET_DEF, PULL_EXISTS]
72      ]) >>
73
74  ONCE_REWRITE_TAC [SUBSET_DEF] >> FULL_SIMP_TAC (srw_ss()) [closed_def]
75QED
76
77Theorem gfp_greatest_dense:
78  !f. monotone f ==> dense f (gfp f) /\ !X. dense f X ==> X SUBSET gfp f
79Proof
80  REPEAT STRIP_TAC THEN REWRITE_TAC [gfp_def] THENL [
81    SIMP_TAC bool_ss [dense_def] THEN MATCH_MP_TAC SUBSET_TRANS THEN
82    Q.EXISTS_TAC ‘BIGUNION { f X | X | X SUBSET f X }’ THEN
83    CONJ_TAC THENL [
84      CONV_TAC (REWR_CONV SUBSET_DEF) THEN
85      SRW_TAC [][] THEN PROVE_TAC [SUBSET_DEF],
86      SRW_TAC [][BIGUNION_SUBSET] THEN
87      Q_TAC SUFF_TAC ‘X SUBSET BIGUNION {X | X SUBSET f X}’ THEN1
88        PROVE_TAC [monotone_def] THEN
89      ONCE_REWRITE_TAC [SUBSET_DEF] THEN
90      SRW_TAC [][] THEN PROVE_TAC []
91    ],
92
93    ONCE_REWRITE_TAC [SUBSET_DEF] THEN
94    FULL_SIMP_TAC (srw_ss())[dense_def] THEN PROVE_TAC []
95  ]
96QED
97
98Theorem lfp_fixedpoint:
99  !f. monotone f ==> f (lfp f) = lfp f /\ !X. f X = X ==> lfp f SUBSET X
100Proof
101  reverse (rpt strip_tac)
102  >- (‘f X SUBSET X’ by PROVE_TAC [SUBSET_REFL] THEN
103      ‘closed f X’ by PROVE_TAC [closed_def] THEN
104      PROVE_TAC [lfp_least_closed]) >>
105  ‘f (lfp f) SUBSET lfp f’ by PROVE_TAC [closed_def, lfp_least_closed] THEN
106  ‘f (f (lfp f)) SUBSET f (lfp f)’ by PROVE_TAC [monotone_def] THEN
107  ‘closed f (f (lfp f))’ by PROVE_TAC [closed_def] THEN
108  ‘lfp f SUBSET f (lfp f)’ by PROVE_TAC [lfp_least_closed] THEN
109  PROVE_TAC [SUBSET_ANTISYM]
110QED
111
112Theorem lfp_poset_lfp:
113  monotone f ==> po_lfp (UNIV,$SUBSET) f (lfp f)
114Proof
115  SIMP_TAC (srw_ss())[posetTheory.lfp_def, lfp_fixedpoint] >>
116  PROVE_TAC[lfp_least_closed, closed_def]
117QED
118
119Theorem gfp_greatest_fixedpoint:
120  !f. monotone f ==> f (gfp f) = gfp f /\ !X. f X = X ==> X SUBSET gfp f
121Proof
122  rpt strip_tac THENL [
123    ‘gfp f SUBSET f (gfp f)’ by PROVE_TAC [dense_def, gfp_greatest_dense] THEN
124    ‘f (gfp f) SUBSET f (f (gfp f))’ by PROVE_TAC [monotone_def] THEN
125    ‘dense f (f (gfp f))’ by PROVE_TAC [dense_def] THEN
126    ‘f (gfp f) SUBSET gfp f’ by PROVE_TAC [gfp_greatest_dense] THEN
127    PROVE_TAC [SUBSET_ANTISYM],
128    ‘X SUBSET f X’ by PROVE_TAC [SUBSET_REFL] THEN
129    ‘dense f X’ by PROVE_TAC [dense_def] THEN
130    PROVE_TAC [gfp_greatest_dense]
131  ]
132QED
133
134Theorem gfp_poset_gfp:
135  monotone f ==> po_gfp (UNIV,$SUBSET) f (gfp f)
136Proof
137  SIMP_TAC (srw_ss()) [posetTheory.gfp_def, gfp_greatest_fixedpoint] >>
138  PROVE_TAC[dense_def, gfp_greatest_dense]
139QED
140
141Theorem lfp_induction:   !f. monotone f ==> !X. f X SUBSET X ==> lfp f SUBSET X
142Proof PROVE_TAC [lfp_least_closed, closed_def]
143QED
144
145Theorem gfp_coinduction: !f. monotone f ==> !X. X SUBSET f X ==> X SUBSET gfp f
146Proof PROVE_TAC [gfp_greatest_dense, dense_def]
147QED
148
149local
150  val lemma = prove(“monotone f ==> !X. f (X INTER lfp f) SUBSET lfp f”,
151                    PROVE_TAC [INTER_SUBSET, monotone_def, lfp_fixedpoint])
152in
153Theorem lfp_strong_induction =
154  lfp_induction |> SPEC_ALL |> UNDISCH |> Q.SPEC ‘X INTER lfp f’
155                |> REWRITE_RULE [SUBSET_INTER, SUBSET_REFL]
156                |> ASM_SIMP_RULE bool_ss [lemma] |> Q.GEN ‘X’ |> DISCH_ALL
157                |> GEN_ALL;
158end
159
160local
161  val lemma = prove(“monotone f ==> !X. gfp f SUBSET f (X UNION gfp f)”,
162                    PROVE_TAC [SUBSET_UNION, monotone_def,
163                               gfp_greatest_fixedpoint])
164in
165Theorem gfp_strong_coinduction =
166           (GEN_ALL o DISCH_ALL o GEN “X:'a -> bool” o
167            ASM_SIMP_RULE bool_ss [lemma] o
168            REWRITE_RULE [UNION_SUBSET, SUBSET_REFL] o Q.SPEC ‘X UNION gfp f’ o
169            UNDISCH o SPEC_ALL) gfp_coinduction;
170end;
171
172Definition fnsum_def[nocompute]:
173  fnsum f1 f2 X = f1 X UNION f2 X
174End
175
176val _ = set_fixity "++" (Infixl 480)
177Overload "++"[inferior] = “fnsum”
178
179Theorem fnsum_monotone:
180   !f1 f2. monotone f1 /\ monotone f2 ==> monotone (fnsum f1 f2)
181Proof
182  ASM_SIMP_TAC bool_ss [fnsum_def, monotone_def] THEN
183  REPEAT STRIP_TAC THEN
184  ‘f1 X SUBSET f1 Y’ by PROVE_TAC [] THEN
185  ‘f2 X SUBSET f2 Y’ by PROVE_TAC [] THEN
186  PROVE_TAC [SUBSET_DEF, IN_UNION]
187QED
188
189Definition empty_def[nocompute]: empty = \X. {}
190End
191
192Theorem empty_monotone:
193   monotone empty
194Proof
195  SRW_TAC [][monotone_def, empty_def]
196QED
197
198Theorem fnsum_empty:
199   !f. (f ++ empty = f) /\ (empty ++ f = f)
200Proof
201  SRW_TAC [][empty_def, fnsum_def, FUN_EQ_THM]
202QED
203
204Theorem fnsum_ASSOC:
205   !f g h. fnsum f (fnsum g h) = fnsum (fnsum f g) h
206Proof
207  REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
208  SIMP_TAC bool_ss [fnsum_def, UNION_ASSOC]
209QED
210
211Theorem fnsum_COMM:
212   !f g. fnsum f g = fnsum g f
213Proof
214  REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN
215  SIMP_TAC bool_ss [fnsum_def, UNION_COMM]
216QED
217
218
219Theorem fnsum_SUBSET:
220   !f g X. f X SUBSET fnsum f g X /\ g X SUBSET fnsum f g X
221Proof
222  SIMP_TAC bool_ss [fnsum_def, SUBSET_DEF, IN_UNION]
223QED
224
225Theorem lfp_fnsum:
226   !f1 f2. monotone f1 /\ monotone f2 ==>
227            lfp f1 SUBSET lfp (fnsum f1 f2) /\
228            lfp f2 SUBSET lfp (fnsum f1 f2)
229Proof
230  PROVE_TAC [lfp_least_closed, closed_def, fnsum_monotone,
231             fnsum_SUBSET, SUBSET_TRANS, lfp_induction]
232QED
233
234Theorem lfp_rule_applied:
235   !f X y. monotone f /\ X SUBSET lfp f /\ y IN f X ==> y IN lfp f
236Proof
237  REPEAT STRIP_TAC THEN
238  ‘f X SUBSET f (lfp f)’ by PROVE_TAC [monotone_def] THEN
239  PROVE_TAC [lfp_fixedpoint, SUBSET_DEF]
240QED
241
242Theorem lfp_empty:
243   !f x. monotone f /\ x IN f {} ==> x IN lfp f
244Proof
245  PROVE_TAC [EMPTY_SUBSET, lfp_rule_applied]
246QED
247