1(* interactive mode
2loadPath := ["../ho_prover","../subtypes","../formalize"] @ !loadPath;
3app load
4  ["bossLib","realLib","ho_proverTools","extra_pred_setTools",
5   "sequenceTools","prob_canonTools","prob_algebraTheory","probTheory"];
6quietdec := true;
7*)
8
9open HolKernel Parse boolLib bossLib arithmeticTheory pred_setTheory
10     listTheory sequenceTheory state_transformerTheory
11     HurdUseful extra_numTheory combinTheory
12     pairTheory realTheory realLib extra_boolTheory
13     extra_pred_setTheory extra_realTheory extra_pred_setTools numTheory
14     simpLib seqTheory sequenceTools subtypeTheory res_quanTheory;
15
16open util_probTheory measureTheory probabilityTheory;
17open prob_algebraTheory probTheory;
18
19(* interactive mode
20quietdec := false;
21*)
22
23val _ = new_theory "prob_geometric";
24
25val EXISTS_DEF = boolTheory.EXISTS_DEF;
26val std_ss' = std_ss ++ boolSimps.ETA_ss;
27val Rewr = DISCH_THEN (REWRITE_TAC o wrap);
28val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap);
29val STRONG_DISJ_TAC = CONV_TAC (REWR_CONV (GSYM IMP_DISJ_THM)) >> STRIP_TAC;
30val Cond =
31  DISCH_THEN
32  (fn mp_th =>
33   let
34     val cond = fst (dest_imp (concl mp_th))
35   in
36     KNOW_TAC cond >| [ALL_TAC, DISCH_THEN (MP_TAC o MP mp_th)]
37   end);
38
39(* ------------------------------------------------------------------------- *)
40(* The definition of the geometric(1/2) random number generator.             *)
41(* ------------------------------------------------------------------------- *)
42
43val prob_geometric_iter_def = Define
44  `prob_geometric_iter s = BIND sdest (\b. UNIT (b, SUC (SND s)))`;
45
46val prob_geometric_loop_def = Define
47  `prob_geometric_loop = prob_while FST prob_geometric_iter`;
48
49val prob_geometric_def = Define
50  `prob_geometric =
51   BIND (BIND (UNIT (T, 0)) prob_geometric_loop) (\s. UNIT (SND s - 1))`;
52
53(* ------------------------------------------------------------------------- *)
54(* Theorems leading to:                                                      *)
55(* 1. prob_geometric IN indep_fn                                             *)
56(* 2. !n. prob {s | FST (prob_geometric s) = n} = (1 / 2) pow (n + 1)        *)
57(* ------------------------------------------------------------------------- *)
58
59val INDEP_FN_PROB_GEOMETRIC_ITER = store_thm
60  ("INDEP_FN_PROB_GEOMETRIC_ITER",
61   ``!a. prob_geometric_iter a IN indep_fn``,
62   RW_TAC std_ss [prob_geometric_iter_def, INDEP_FN_SDEST, INDEP_FN_BIND,
63                  INDEP_FN_UNIT]);
64
65val PROB_GEOMETRIC_LOOP_TERMINATES = store_thm
66  ("PROB_GEOMETRIC_LOOP_TERMINATES",
67   ``prob_while_terminates FST prob_geometric_iter``,
68   MATCH_MP_TAC PROB_WHILE_TERMINATES_SUFFICIENT
69   >> RW_TAC std_ss [INDEP_FN_PROB_GEOMETRIC_ITER, possibly_bern_def,
70                     possibly_def] \\
71    ( RW_TAC std_ss [prob_geometric_iter_def, UNIT_DEF, BIND_DEF, o_DEF,
72                     UNCURRY]
73   >> Suff `{s | ~FST (sdest s)} = halfspace F`
74   >- (RW_TAC std_ss [EVENTS_BERN_HALFSPACE, PROB_BERN_HALFSPACE]
75       >> PROVE_TAC [REAL_LT_LE, HALF_POS])
76   >> SET_EQ_TAC
77   >> RW_TAC std_ss [GSPECIFICATION, IN_HALFSPACE, sdest_def] ));
78
79val INDEP_FN_PROB_GEOMETRIC_LOOP = store_thm
80  ("INDEP_FN_PROB_GEOMETRIC_LOOP",
81   ``!a. prob_geometric_loop a IN indep_fn``,
82   RW_TAC std_ss [prob_geometric_loop_def, INDEP_FN_PROB_WHILE,
83                  PROB_GEOMETRIC_LOOP_TERMINATES,
84                  INDEP_FN_PROB_GEOMETRIC_ITER]);
85
86val INDEP_FN_PROB_GEOMETRIC = store_thm
87  ("INDEP_FN_PROB_GEOMETRIC",
88   ``prob_geometric IN indep_fn``,
89   RW_TAC std_ss [prob_geometric_def, INDEP_FN_BIND, INDEP_FN_UNIT,
90                  INDEP_FN_PROB_GEOMETRIC_LOOP]);
91
92val PROB_GEOMETRIC_LOOP_F = store_thm
93  ("PROB_GEOMETRIC_LOOP_F",
94   ``!n. !*s. FST (prob_geometric_loop (F, n) s) = (F, n)``,
95   RW_TAC std_ss [prob_geometric_loop_def]
96   >> MP_TAC (Q.ISPEC `\w : bool # num. w = (F, n)` PROB_WHILE)
97   >> RW_TAC std_ss []
98   >> POP_ASSUM MATCH_MP_TAC
99   >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_TERMINATES,
100                     INDEP_FN_PROB_GEOMETRIC_ITER]
101   >> MATCH_MP_TAC DEFINITELY_PROBABLY
102   >> Cases_on `n'`
103   >> RW_TAC std_ss [prob_while_cut_def, BIND_DEF, o_THM, UNCURRY,
104                     prob_geometric_iter_def, UNIT_DEF, sdest_def]);
105
106val PROB_GEOMETRIC_LOOP_T_RANGE = store_thm
107  ("PROB_GEOMETRIC_LOOP_T_RANGE",
108   ``!n. !*s. n < SND (FST (prob_geometric_loop (T,n) s))``,
109   RW_TAC std_ss [prob_geometric_loop_def]
110   >> MP_TAC (Q.ISPEC `\w : bool # num. n < SND w` PROB_WHILE)
111   >> RW_TAC std_ss []
112   >> POP_ASSUM MATCH_MP_TAC
113   >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_TERMINATES,
114                     INDEP_FN_PROB_GEOMETRIC_ITER]
115   >> MATCH_MP_TAC DEFINITELY_PROBABLY
116   >> Q.SPEC_TAC (`n`, `n`)
117   >> Induct_on `n'` >- RW_TAC std_ss [prob_while_cut_def, UNIT_DEF]
118   >> REPEAT GEN_TAC
119   >> (REVERSE (Cases_on `shd s`)
120       >> RW_TAC std_ss [prob_while_cut_def, BIND_DEF, o_THM, UNCURRY,
121                         prob_geometric_iter_def, UNIT_DEF, sdest_def])
122   >- (POP_ASSUM MP_TAC
123       >> Cases_on `n'`
124       >> RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF])
125   >> MATCH_MP_TAC LESS_TRANS
126   >> Q.EXISTS_TAC `SUC n`
127   >> CONJ_TAC >- DECIDE_TAC
128   >> Q.PAT_X_ASSUM `!s. P s` MATCH_MP_TAC
129   >> RW_TAC std_ss []);
130
131val PROB_GEOMETRIC_LOOP_STOPS = store_thm
132  ("PROB_GEOMETRIC_LOOP_STOPS",
133   ``!n. !*s. (SND (FST (prob_geometric_loop (b,n) s)) = n) = ~b``,
134   RW_TAC std_ss [prob_geometric_loop_def]
135   >> MP_TAC (Q.ISPEC `\w : bool # num. (SND w = n) = ~b` PROB_WHILE)
136   >> RW_TAC std_ss []
137   >> POP_ASSUM MATCH_MP_TAC
138   >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_TERMINATES,
139                     INDEP_FN_PROB_GEOMETRIC_ITER]
140   >> Cases_on `n'`
141   >- (RW_TAC std_ss [prob_while_cut_def, UNIT_DEF]
142       >> MATCH_MP_TAC DEFINITELY_PROBABLY
143       >> RW_TAC std_ss [])
144   >> RW_TAC std_ss [prob_while_cut_def, UNIT_DEF, PROBABLY_TRUE, BIND_DEF,
145                     UNCURRY, o_THM, prob_geometric_iter_def, sdest_def]
146   >> MATCH_MP_TAC DEFINITELY_PROBABLY
147   >> RW_TAC std_ss []
148   >> KILL_TAC
149   >> Know `!a b : num. b < a ==> ~(a = b)` >- DECIDE_TAC
150   >> DISCH_THEN MATCH_MP_TAC
151   >> Know `n < SUC n` >- DECIDE_TAC
152   >> Q.SPEC_TAC (`SUC n`, `m`)
153   >> Q.SPEC_TAC (`shd s`, `b`)
154   >> Q.SPEC_TAC (`stl s`, `s`)
155   >> Induct_on `n''` >- RW_TAC arith_ss [prob_while_cut_def, UNIT_DEF]
156   >> RW_TAC arith_ss [prob_while_cut_def, BIND_DEF, UNIT_DEF, UNCURRY, o_THM,
157                       prob_geometric_iter_def, sdest_def]);
158
159val PROB_BERN_GEOMETRIC_LOOP_LEMMA = store_thm
160  ("PROB_BERN_GEOMETRIC_LOOP_LEMMA",
161   ``!d n.
162       prob bern
163       ((\x. SND x = n + SUC d) o FST o
164        BIND sdest (\a. BIND (UNIT (a,SUC n)) prob_geometric_loop)) =
165       1 / 2 *
166       prob bern
167       ((\x. SND x = n + SUC d) o FST o
168        (\a. BIND (UNIT (a,SUC n)) prob_geometric_loop) T) +
169       1 / 2 *
170       prob bern
171       ((\x. SND x = n + SUC d) o FST o
172        (\a. BIND (UNIT (a,SUC n)) prob_geometric_loop) F)``,
173   REPEAT GEN_TAC
174   >> (MP_TAC o
175       Q.SPECL
176       [`sdest`,
177        `\a. BIND (UNIT (a,SUC n)) (prob_while FST prob_geometric_iter)`,
178        `1 / 2`,
179        `\x. SND x = n + SUC d`] o
180       INST_TYPE [alpha |-> ``:bool # num``])
181      PROB_BERN_BIND_BOOL
182   >> Cond
183   >- (REVERSE (RW_TAC std_ss [INDEP_FN_SDEST])
184       >- (Suff `FST o sdest = halfspace T`
185           >- RW_TAC std_ss [PROB_BERN_HALFSPACE]
186           >> SET_EQ_TAC
187           >> RW_TAC std_ss [IN_HALFSPACE, sdest_def, IN_o]
188           >> RW_TAC std_ss [SPECIFICATION])
189       >> MATCH_MP_TAC INDEP_FN_BIND
190       >> RW_TAC std_ss [INDEP_FN_UNIT]
191       >> MATCH_MP_TAC INDEP_FN_PROB_WHILE
192       >> RW_TAC std_ss [INDEP_FN_PROB_GEOMETRIC_ITER,
193                         PROB_GEOMETRIC_LOOP_TERMINATES])
194   >> RW_TAC std_ss [ONE_MINUS_HALF, prob_geometric_loop_def]);
195
196val PROB_BERN_GEOMETRIC_LOOP = store_thm
197  ("PROB_BERN_GEOMETRIC_LOOP",
198   ``!n d.
199       prob bern {s | SND (FST (prob_geometric_loop (T,n) s)) = n + SUC d} =
200       (1 / 2) pow SUC d``,
201   RW_TAC std_ss [prob_geometric_loop_def]
202   >> RW_TAC std_ss [PROB_WHILE_ADVANCE, INDEP_FN_PROB_GEOMETRIC_ITER,
203                     PROB_GEOMETRIC_LOOP_TERMINATES, prob_geometric_iter_def,
204                     GSYM BIND_ASSOC]
205   >> Know
206      `!f : (num -> bool) -> (bool # num) # (num -> bool).
207         {s | SND (FST (f s)) = n + SUC d} = (\x. SND x = n + SUC d) o FST o f`
208   >- (SET_EQ_TAC
209       >> PSET_TAC []
210       >> RW_TAC std_ss [SPECIFICATION, o_THM])
211   >> Rewr
212   >> RW_TAC std_ss [GSYM prob_geometric_loop_def]
213   >> Q.SPEC_TAC (`n`, `n`)
214   >> Induct_on `d`
215   >- (RW_TAC std_ss [PROB_BERN_GEOMETRIC_LOOP_LEMMA]
216       >> RW_TAC real_ss [ADD_CLAUSES, pow, o_DEF, BIND_DEF, UNCURRY, UNIT_DEF,
217                          prob_geometric_loop_def]
218       >> Know
219          `prob bern
220           (\x.
221              SND (FST (prob_while FST prob_geometric_iter (F,SUC n) x)) =
222              n + 1) =
223           prob bern UNIV`
224       >- (REWRITE_TAC [GSYM ADD1]
225           >> MATCH_MP_TAC PROB_BERN_UNIVERSAL
226           >> Q.EXISTS_TAC
227              `\s. (SND (FST (prob_geometric_loop (F, SUC n) s)) = SUC n) = ~F`
228           >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_STOPS, EVENTS_BERN_UNIV,
229                             IN_UNIV]
230           >- (RW_TAC std_ss [SYM prob_geometric_loop_def]
231               >> Suff
232                  `(\x. SND (FST (prob_geometric_loop (F,SUC n) x)) = SUC n) =
233                   (\x. SND x = SUC n) o FST o prob_geometric_loop (F, SUC n)`
234               >- (Rewr
235                   >> PROVE_TAC [INDEP_FN_FST_EVENTS,
236                                 INDEP_FN_PROB_GEOMETRIC_LOOP])
237               >> FUN_EQ_TAC
238               >> RW_TAC std_ss [o_DEF])
239           >> RW_TAC std_ss [SPECIFICATION, GSYM prob_geometric_loop_def])
240       >> Rewr
241       >> Know
242          `prob bern
243           (\x.
244              SND (FST (prob_while FST prob_geometric_iter (T,SUC n) x)) =
245              n + 1) =
246           prob bern {}`
247       >- (REWRITE_TAC [GSYM ADD1]
248           >> MATCH_MP_TAC PROB_BERN_UNIVERSAL
249           >> Q.EXISTS_TAC
250              `\s. (SND (FST (prob_geometric_loop (T, SUC n) s)) = SUC n) = ~T`
251           >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_STOPS, EVENTS_BERN_EMPTY,
252                             NOT_IN_EMPTY]
253           >- (RW_TAC std_ss [SYM prob_geometric_loop_def]
254               >> Suff
255                  `(\x. SND (FST (prob_geometric_loop (T,SUC n) x)) = SUC n) =
256                   (\x. SND x = SUC n) o FST o prob_geometric_loop (T, SUC n)`
257               >- (Rewr
258                   >> PROVE_TAC [INDEP_FN_FST_EVENTS,
259                                 INDEP_FN_PROB_GEOMETRIC_LOOP])
260               >> FUN_EQ_TAC
261               >> RW_TAC std_ss [o_DEF])
262           >> RW_TAC std_ss [SPECIFICATION, GSYM prob_geometric_loop_def])
263       >> Rewr
264       >> RW_TAC real_ss [PROB_BERN_BASIC])
265   >> RW_TAC std_ss [PROB_BERN_GEOMETRIC_LOOP_LEMMA]
266   >> RW_TAC std_ss [prob_geometric_loop_def, BIND_DEF, o_DEF, UNCURRY,
267                     UNIT_DEF]
268   >> RW_TAC std_ss [PROB_WHILE_ADVANCE, INDEP_FN_PROB_GEOMETRIC_ITER,
269                     PROB_GEOMETRIC_LOOP_TERMINATES, prob_geometric_iter_def,
270                     GSYM BIND_ASSOC, UNIT_DEF]
271   >> Know `!n d. (SUC n = n + SUC (SUC d)) = F` >- DECIDE_TAC
272   >> Rewr
273   >> RW_TAC bool_ss [GSYM EMPTY_DEF, PROB_BERN_EMPTY, REAL_MUL_RZERO,
274                      GSYM prob_geometric_loop_def, REAL_ADD_RID]
275   >> ONCE_REWRITE_TAC [pow]
276   >> RW_TAC std_ss [REAL_EQ_MUL_LCANCEL]
277   >> DISJ2_TAC
278   >> Suff
279      `(\x.
280         SND
281           (FST
282              (BIND sdest
283                 (\a. BIND (\s. ((a,SUC (SUC n)),s)) prob_geometric_loop) x)) =
284         n + SUC (SUC d)) =
285         ((\x. SND x = SUC n + SUC d) o FST o
286           BIND sdest (\a. BIND (UNIT (a,SUC (SUC n))) prob_geometric_loop))`
287   >- (Rewr
288       >> RW_TAC std_ss [])
289   >> FUN_EQ_TAC
290   >> RW_TAC std_ss [BIND_DEF, UNIT_DEF, o_DEF, UNCURRY, ADD_CLAUSES]);
291
292val PROB_BERN_GEOMETRIC = store_thm
293  ("PROB_BERN_GEOMETRIC",
294   ``!n. prob bern {s | FST (prob_geometric s) = n} = (1 / 2) pow (n + 1)``,
295   RW_TAC std_ss [prob_geometric_def, BIND_DEF, o_THM, UNCURRY, UNIT_DEF]
296   >> Suff
297      `prob bern {s | SND (FST (prob_geometric_loop (T,0) s)) - 1 = n} =
298       prob bern {s | SND (FST (prob_geometric_loop (T,0) s)) = 0 + (n + 1)}`
299   >- (Rewr
300       >> RW_TAC bool_ss [GSYM ADD1, PROB_BERN_GEOMETRIC_LOOP])
301   >> MATCH_MP_TAC PROB_BERN_UNIVERSAL
302   >> Q.EXISTS_TAC `\s. 0 < SND (FST (prob_geometric_loop (T,0) s))`
303   >> RW_TAC std_ss [PROB_GEOMETRIC_LOOP_T_RANGE] >|
304   [Suff
305    `{s | SND (FST (prob_geometric_loop (T,0) s)) - 1 = n} =
306     (\x. SND x - 1 = n) o FST o prob_geometric_loop (T, 0)`
307    >- (Rewr
308        >> PROVE_TAC [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_GEOMETRIC_LOOP])
309    >> SET_EQ_TAC
310    >> PSET_TAC []
311    >> RW_TAC std_ss [SPECIFICATION, o_DEF],
312    Suff
313    `{s | SND (FST (prob_geometric_loop (T,0) s)) = n + 1} =
314     (\x. SND x = n + 1) o FST o prob_geometric_loop (T, 0)`
315    >- (Rewr
316        >> PROVE_TAC [INDEP_FN_FST_EVENTS, INDEP_FN_PROB_GEOMETRIC_LOOP])
317    >> SET_EQ_TAC
318    >> PSET_TAC []
319    >> RW_TAC std_ss [SPECIFICATION, o_DEF],
320    RW_TAC std_ss [GSPECIFICATION]
321    >> DECIDE_TAC]);
322
323val _ = export_theory ();
324