cv_typeScript.sml

1(*
2  Definitions and theorems that support cv_typeLib
3*)
4Theory cv_type
5Ancestors
6  cv one[qualified] option[qualified] list[qualified]
7  sum[qualified] pair[qualified] words integer rat
8
9Overload c2n[local] = “cv$c2n”
10Overload c2b[local] = “cv$c2b”
11Overload Num[local] = “cv$Num”
12Overload Pair[local] = “cv$Pair”
13
14(* every from/to function must satisfy: *)
15
16Definition from_to_def:
17  from_to (f:'a -> cv) (t:cv -> 'a) = !x. t (f x) = x
18End
19
20(* unit *)
21
22Definition from_unit_def:
23  from_unit () = (Num 0):cv
24End
25
26Definition to_unit_def:
27  to_unit (x:cv) = ()
28End
29
30Theorem from_to_unit:
31  from_to from_unit to_unit
32Proof
33  fs [from_to_def]
34QED
35
36(* bool *)
37
38Theorem from_to_bool:
39  from_to b2c c2b
40Proof
41  fs [from_to_def] \\ Cases \\ fs [b2c_def]
42QED
43
44(* num *)
45
46Theorem from_to_num:
47  from_to Num c2n
48Proof
49  fs [from_to_def]
50QED
51
52(* char *)
53
54Definition from_char_def:
55  from_char (c:char) = Num (ORD c)
56End
57
58Definition to_char_def:
59  to_char x = CHR (c2n x)
60End
61
62Theorem from_to_char:
63  from_to from_char to_char
64Proof
65  fs [from_to_def] \\ Cases \\ fs [from_char_def,to_char_def]
66QED
67
68(* int *)
69
70Definition from_int_def:
71  from_int (i:int) =
72    if integer$int_lt i (integer$int_of_num 0) then
73      Pair (Num (integer$Num i)) (Num 0)
74    else Num (integer$Num i)
75End
76
77Definition to_int_def:
78  to_int (Num n) = integer$int_of_num n /\
79  to_int (Pair x y) = integer$int_neg (integer$int_of_num (c2n x))
80End
81
82Theorem from_to_int:
83  from_to from_int to_int
84Proof
85  fs [from_to_def] \\ Cases \\ fs [from_int_def,to_int_def]
86QED
87
88(* rat *)
89
90Definition from_rat_def:
91  from_rat (r:rat) =
92    Pair (from_int $ rat$RATN r) (Num $ rat$RATD r)
93End
94
95Definition to_rat_def:
96  to_rat (Num n) = rat$rat_of_num 0 /\
97  to_rat (Pair x y) =
98    rat$rat_div (rat$rat_of_int (to_int x)) (rat$rat_of_num (c2n y))
99End
100
101Theorem from_to_rat:
102  from_to from_rat to_rat
103Proof
104  rw[from_to_def, from_rat_def, to_rat_def] >>
105  assume_tac from_to_int >> gvs[from_to_def]
106QED
107
108(* word *)
109
110Definition from_word_def:
111  from_word (w:'a words$word) = Num (words$w2n w)
112End
113
114Definition to_word_def:
115  to_word n = words$n2w (c2n n) :'a words$word
116End
117
118Theorem from_to_word:
119  from_to from_word to_word
120Proof
121  fs [from_to_def] \\ Cases \\ fs [from_word_def,to_word_def]
122QED
123
124(* option *)
125
126Definition from_option_def:
127  from_option f NONE = Num 0 /\
128  from_option f (SOME x) = Pair (Num 1) (f x)
129End
130
131Definition to_option_def:
132  to_option t (Num n) = NONE /\
133  to_option t (Pair x y) = SOME (t y)
134End
135
136Theorem from_to_option:
137  from_to f t ==>
138  from_to (from_option f) (to_option t)
139Proof
140  fs [from_to_def] \\ strip_tac
141  \\ Cases \\ fs [from_option_def,to_option_def]
142QED
143
144(* pair *)
145
146Definition from_pair_def:
147  from_pair f1 f2 (x,y) = Pair (f1 x) (f2 y)
148End
149
150Definition to_pair_def:
151  to_pair t1 t2 (Pair x y) = (t1 x, t2 y) /\
152  to_pair t1 t2 _ = ARB
153End
154
155Theorem from_to_pair:
156  from_to f1 t1 /\ from_to f2 t2 ==>
157  from_to (from_pair f1 f2) (to_pair t1 t2)
158Proof
159  fs [from_to_def] \\ strip_tac
160  \\ Cases \\ fs [from_pair_def,to_pair_def]
161QED
162
163(* sum *)
164
165Definition from_sum_def:
166  from_sum f1 f2 (INL x) = Pair (Num 0) (f1 x) /\
167  from_sum f1 f2 (INR y) = Pair (Num 1) (f2 y)
168End
169
170Definition to_sum_def:
171  to_sum t1 t2 (Num n) = ARB /\
172  to_sum t1 t2 (Pair x y) =
173    if x = Num 0 then INL (t1 y) else INR (t2 y)
174End
175
176Theorem from_to_sum:
177  from_to f1 t1 /\ from_to f2 t2 ==>
178  from_to (from_sum f1 f2) (to_sum t1 t2)
179Proof
180  fs [from_to_def] \\ strip_tac
181  \\ Cases \\ fs [from_sum_def,to_sum_def]
182QED
183
184(* list *)
185
186Definition from_list_def:
187  from_list f [] = Num 0 /\
188  from_list f (x::xs) = Pair (f x) (from_list f xs)
189End
190
191Definition to_list_def[nocompute]:
192  to_list f (Num n) = [] /\
193  to_list f (Pair x y) = f x :: to_list f y
194End
195
196Theorem from_to_list:
197  from_to f t ==>
198  from_to (from_list f) (to_list t)
199Proof
200  fs [from_to_def] \\ strip_tac
201  \\ Induct \\ fs [from_list_def,to_list_def]
202QED
203
204Definition to_list_tr_def:
205  to_list_tr f (Num n) acc = REVERSE acc /\
206  to_list_tr f (Pair x y) acc = to_list_tr f y (f x :: acc)
207End
208
209Theorem to_list_tr_eq_lemma[local]:
210  !v acc. to_list_tr f v acc = REVERSE acc ++ to_list f v
211Proof
212  Induct \\ rw[to_list_def, to_list_tr_def]
213QED
214
215Theorem to_list_tr_eq[compute]:
216  to_list f v = to_list_tr f v []
217Proof
218  rw[to_list_tr_eq_lemma]
219QED
220
221(* used in definitions of to-functions of user-defined datatype *)
222
223Definition cv_has_shape_def:
224  cv_has_shape (SOME n::xs) (Pair x y) = (x = Num n /\ cv_has_shape xs y) /\
225  cv_has_shape (NONE::xs) (Pair x y) = cv_has_shape xs y /\
226  cv_has_shape (_::xs) (Num _) = F /\
227  cv_has_shape [] c = T
228End
229
230Theorem cv_has_shape_expand:
231  cv_has_shape [] cv = T /\
232  cv_has_shape (NONE::xs) cv = (?x y. cv = Pair x y /\ cv_has_shape xs y) /\
233  cv_has_shape (SOME n::xs) cv = (?y. cv = Pair (Num n) y /\ cv_has_shape xs y)
234Proof
235  Cases_on ‘cv’ \\ fs [cv_has_shape_def]
236QED
237
238(* lemmas for automation *)
239
240Theorem get_to_pair:
241  (if cv_has_shape [NONE] v then (t1 (cv_fst v),t2 (cv_snd v)) else ARB) =
242  to_pair t1 t2 v
243Proof
244  Cases_on ‘v’
245  \\ fs [to_pair_def,cv_has_shape_def]
246QED
247
248Theorem get_to_option:
249  (if cv_has_shape [NONE] v then SOME (t (cv_snd v)) else NONE) = to_option t v
250Proof
251  Cases_on ‘v’
252  \\ fs [to_option_def,cv_has_shape_def]
253QED
254
255Theorem get_to_sum:
256  (if cv_has_shape [SOME 0] v then INL (t1 (cv_snd v))
257   else if cv_has_shape [NONE] v then INR (t2 (cv_snd v))
258   else ARB) = to_sum t1 t2 v
259Proof
260  Cases_on ‘v’
261  \\ fs [to_sum_def,cv_has_shape_def]
262QED
263
264Theorem get_from_sum:
265  (case v of INL x => Pair (Num 0) (f0 x) | INR y => Pair (Num 1) (f1 y)) =
266  from_sum f0 f1 v
267Proof
268  Cases_on ‘v’ \\ fs [from_sum_def]
269QED
270
271Theorem get_from_option:
272  (case v of NONE => Num 0 | SOME x => Pair (Num 1) (f x)) =
273  from_option f v
274Proof
275  Cases_on ‘v’ \\ fs [from_option_def]
276QED
277
278Theorem get_from_pair:
279  (case v of (v0,v1) => Pair (f0 v0) (f1 v1)) =
280  from_pair f0 f1 v
281Proof
282  Cases_on ‘v’ \\ fs [from_pair_def]
283QED
284
285Theorem from_pair_eq_IMP:
286  from_pair f1 f2 x = Pair y1 y2 ==>
287  f1 (FST x) = y1 /\ f2 (SND x) = y2
288Proof
289  Cases_on ‘x’ \\ rw [] \\ gvs [from_pair_def]
290QED
291
292Theorem IMP_from_pair_eq:
293  f1 (FST x) = y1 /\ f2 (SND x) = y2 ==>
294  from_pair f1 f2 x = Pair y1 y2
295Proof
296  Cases_on ‘x’ \\ rw [] \\ gvs [from_pair_def]
297QED
298
299Theorem from_option_eq_IMP:
300  from_option f1 x = Pair (Num 1) y1 ==>
301  f1 (THE x) = y1 /\ IS_SOME x
302Proof
303  Cases_on ‘x’ \\ rw [] \\ gvs [from_option_def]
304QED
305
306Theorem IMP_from_option_eq:
307  f1 (THE x) = y1 /\ IS_SOME x ==>
308  from_option f1 x = Pair (Num 1) y1
309Proof
310  Cases_on ‘x’ \\ rw [] \\ gvs [from_option_def]
311QED
312
313Theorem to_pair_IMP:
314  x = to_pair t1 t2 (Pair x1 x2) ==>
315  FST x = t1 x1 /\ SND x = t2 x2
316Proof
317  rw [to_pair_def]
318QED
319
320Theorem IMP_to_pair:
321  FST x = y1 /\ SND x = y2 ==> x = (y1,y2)
322Proof
323  Cases_on ‘x’ \\ gvs []
324QED
325
326Theorem to_option_IMP:
327  x = to_option t1 (Pair x1 x2) ==>
328  THE x = t1 x2 /\ IS_SOME x
329Proof
330  rw [to_option_def]
331QED
332
333Theorem IMP_to_option:
334  THE x = y1 /\ IS_SOME x ==> x = SOME y1
335Proof
336  Cases_on ‘x’ \\ gvs []
337QED
338