cvScript.sml

1Theory cv[bare]
2Ancestors
3  arithmetic numeral[qualified]
4Libs
5  HolKernel Parse boolLib IndDefLib DefnBase BasicProvers simpLib
6  newtypeTools[qualified] metisLib[qualified]
7
8fun simp ths = ASM_SIMP_TAC (srw_ss()) ths
9fun SRULE ths = SIMP_RULE (srw_ss()) ths
10
11val N0_def = new_definition("N0_def",
12  “N0 (m:num) n = if n = 0 then m+1 else 0”);
13
14val P0_def = new_definition("P0_def",
15  “P0 (c:num -> num) d n =
16   if n = 0 then 0
17   else if ODD n then c (n DIV 2)
18   else d ((n-2) DIV 2)”);
19
20Theorem N0_11[local,simp]:
21  N0 m = N0 n <=> m = n
22Proof
23  simp[FUN_EQ_THM, N0_def, EQ_IMP_THM] >>
24  disch_then $ Q.SPEC_THEN ‘0’ mp_tac >> simp[EQ_MONO_ADD_EQ]
25QED
26
27Theorem simple_inequalities[local,simp]:
28  1 <> 0 /\ 2 <> 0
29Proof
30  simp[ONE, TWO]
31QED
32
33Theorem ODD12[local,simp]:
34  ODD 1 /\ ~ODD 2
35Proof
36  simp[ONE, TWO, ODD]
37QED
38
39Theorem ONE_DIV2[local,simp]:
40  1 DIV 2 = 0
41Proof
42  simp[ONE, TWO, prim_recTheory.LESS_MONO_EQ, prim_recTheory.LESS_0,
43       LESS_DIV_EQ_ZERO]
44QED
45
46Theorem P0_11[local,simp]:
47  P0 c d = P0 e f <=> c = e /\ d = f
48Proof
49  simp[FUN_EQ_THM, P0_def, EQ_IMP_THM] >> rpt strip_tac
50  >- (Q.RENAME_TAC [‘c x = e x’] >>
51      pop_assum $ Q.SPEC_THEN ‘2 * x + 1’ mp_tac >>
52      simp[ADD_EQ_0, ADD_CLAUSES, ODD_ADD, ODD_MULT]) >>
53  Q.RENAME_TAC [‘d x = f x’] >>
54  pop_assum $ Q.SPEC_THEN ‘2 * x + 2’ mp_tac >>
55  simp[ADD_EQ_0, ADD_CLAUSES, ODD_ADD, ODD_MULT, MULT_EQ_0, ADD_SUB]
56QED
57
58Inductive iscv:
59[~num:] (!m. iscv (N0 m))
60[~pair:] (!c d. iscv c /\ iscv d ==> iscv (P0 c d))
61End
62
63val cv_tydefrec = newtypeTools.rich_new_type
64   {tyname = "cv",
65    exthm  = prove(“?cv. iscv cv”,
66                   Q.EXISTS_TAC ‘N0 0’ >> REWRITE_TAC[iscv_num]),
67    ABS    = "cv_ABS",
68    REP    = "cv_REP"};
69
70val Pair_def = new_definition("Pair_def",
71  “Pair c d = cv_ABS (P0 (cv_REP c) (cv_REP d))”);
72
73Theorem Pair_11:
74  Pair c d = Pair e f <=> c = e /\ d = f
75Proof
76  simp[Pair_def, EQ_IMP_THM] >> strip_tac >>
77  drule_at (Pat ‘cv_ABS _ = cv_ABS _’)
78           (iffLR $ #term_ABS_pseudo11 cv_tydefrec) >>
79  simp[#termP_term_REP cv_tydefrec, iscv_pair, #term_REP_11 cv_tydefrec]
80QED
81
82val Num_def = new_definition("Num_def", “Num n = cv_ABS (N0 n)”);
83
84Theorem Num_11:
85  Num m = Num n <=> m = n
86Proof
87  simp[Num_def, EQ_IMP_THM] >> strip_tac >>
88  drule_at (Pat ‘cv_ABS _ = cv_ABS _’)
89           (iffLR $ #term_ABS_pseudo11 cv_tydefrec) >>
90  simp[iscv_num]
91QED
92
93Theorem cv_distinct:
94  Num n <> Pair c d
95Proof
96  simp[Num_def, Pair_def] >> strip_tac >>
97  drule_at (Pat ‘cv_ABS _ = cv_ABS _’)
98           (iffLR $ #term_ABS_pseudo11 cv_tydefrec) >>
99  simp[iscv_num, iscv_pair, #termP_term_REP cv_tydefrec] >>
100  simp[N0_def, P0_def, FUN_EQ_THM] >> Q.EXISTS_TAC ‘0’ >>
101  simp[ADD_EQ_0]
102QED
103
104Theorem cv_induction =
105        iscv_strongind |> Q.SPEC ‘λc0. P (cv_ABS c0)’
106                       |> BETA_RULE
107                       |> SRULE [GSYM Num_def]
108                       |> SRULE [#termP_exists cv_tydefrec, PULL_EXISTS,
109                                 GSYM Pair_def, #absrep_id cv_tydefrec]
110                       |> Q.GEN ‘P’
111
112Inductive cvrel:
113[~num:]
114  (!n. cvrel f g (Num n) (f n))
115[~pair:]
116  (!c d rc rd. cvrel f g c rc /\ cvrel f g d rd ==>
117               cvrel f g (Pair c d) (g c d rc rd))
118End
119
120Theorem cvrel_exists:
121  !f g c. ?r. cvrel f g c r
122Proof
123  ntac 2 gen_tac >> ho_match_mp_tac cv_induction >> rpt strip_tac
124  >- irule_at Any cvrel_num >>
125  irule_at Any cvrel_pair >> rpt (first_assum $ irule_at Any)
126QED
127
128Theorem cvrel_unique:
129  !c r1. cvrel f g c r1 ==>
130         !r2. cvrel f g c r2 ==> r1 = r2
131Proof
132  ho_match_mp_tac cvrel_strongind >> rpt strip_tac
133  >- (pop_assum mp_tac >> simp[Once cvrel_cases] >>
134      simp[Num_11,cv_distinct]) >>
135  Q.PAT_X_ASSUM ‘cvrel _ _ (Pair _ _) _’ mp_tac>>
136  simp[Once cvrel_cases] >> simp[cv_distinct, Pair_11]>>
137  metisLib.METIS_TAC[]
138QED
139
140val cvrelf_def = new_definition("cvrelf_def",
141                                “cvrelf f g c = @r. cvrel f g c r”);
142
143Theorem cvrelf_Pair:
144  cvrelf f g (Pair c d) = g c d (cvrelf f g c) (cvrelf f g d)
145Proof
146  CONV_TAC (LAND_CONV (SIMP_CONV (srw_ss()) [cvrelf_def])) >>
147  SELECT_ELIM_TAC>> conj_tac
148  >- (irule_at Any cvrel_exists) >>
149  simp[Once cvrel_cases, cv_distinct, Pair_11, PULL_EXISTS] >>
150  rpt strip_tac >>
151  Q.SUBGOAL_THEN ‘cvrelf f g c = rc /\ cvrelf f g d = rd’ strip_assume_tac
152  >- (simp[cvrelf_def] >> conj_tac >> SELECT_ELIM_TAC >>
153      metisLib.METIS_TAC[cvrel_unique]) >>
154  simp[]
155QED
156
157Theorem cv_Axiom:
158  !f g. ?h. (!n. h (Num n) = f n) /\
159            (!c d. h (Pair c d) = g c d (h c) (h d))
160Proof
161  rpt gen_tac >> Q.EXISTS_TAC ‘cvrelf f g’ >> simp[cvrelf_Pair] >>
162  simp[cvrelf_def, Once cvrel_cases, Num_11, cv_distinct]
163QED
164
165(* helpers/auxiliaries *)
166val c2b_def = new_definition ("c2b_def", “c2b x = ?k. x = Num (SUC k)”);
167val cv_if_def0 = new_definition(
168  "cv_if_def0",
169  “cv_if p (q:cv) (r:cv) = if c2b p then q else r”);
170Theorem cv_if_def:
171  cv_if (Num (SUC m)) (p:cv) (q:cv) = p /\
172  cv_if (Num 0) p q = q /\
173  cv_if (Pair r s) p q = q
174Proof
175  simp[c2b_def, cv_if_def0, Num_11, cv_distinct]
176QED
177
178Theorem c2b_thm[simp]:
179  (c2b (Num (SUC n)) = T) /\
180  (c2b (Num 1) = T) /\
181  (c2b (Num 0) = F) /\
182  (c2b (Num (NUMERAL ZERO)) = F) /\
183  (c2b (Pair x y) = F)
184Proof
185  rewrite_tac [c2b_def,Num_11,prim_recTheory.INV_SUC_EQ]
186  \\ rewrite_tac [GSYM boolTheory.EXISTS_REFL,NORM_0]
187  \\ rewrite_tac [SUC_NOT]
188  \\ once_rewrite_tac [EQ_SYM_EQ]
189  \\ rewrite_tac [cv_distinct]
190  \\ EXISTS_TAC “0:num”
191  \\ rewrite_tac [ADD1,ADD_CLAUSES]
192QED
193
194val cv_case_def = Prim_rec.new_recursive_definition {
195  name = "cv_case_def",
196  rec_axiom = cv_Axiom,
197  def = “cv_CASE (Num n) nmf prf = nmf n /\
198         cv_CASE (Pair c d) nmf prf = prf c d”};
199
200Overload case = “cv_CASE”
201
202val cv_size_def = Prim_rec.new_recursive_definition {
203  name = "cv_size_def",
204  rec_axiom = cv_Axiom,
205  def = “cv_size (Num n) = n /\
206         cv_size (Pair c d) = 1 + (cv_size c + cv_size d)”};
207
208val _ = TypeBase.export (
209    TypeBasePure.gen_datatype_info{
210      ax = cv_Axiom, ind = cv_induction, case_defs = [cv_case_def]
211    } |> map (TypeBasePure.put_size (“cv_size”, TypeBasePure.ORIG cv_size_def))
212)
213
214fun recdef (n,t) =
215  Prim_rec.new_recursive_definition{name = n, def = t, rec_axiom = cv_Axiom}
216
217val cv_fst_def = recdef("cv_fst_def",
218                       “cv_fst (Pair p q) = p /\ cv_fst (Num m) = Num 0”);
219val cv_snd_def = recdef("cv_snd_def",
220                       “cv_snd (Pair p q) = q /\ cv_snd (Num m) = Num 0”);
221val cv_ispair_def = recdef("cv_ispair_def",
222                           “cv_ispair (Pair p q) = Num (SUC 0) /\
223                            cv_ispair (Num m) = Num 0”);
224val _ = export_rewrites ["cv_fst_def", "cv_snd_def", "cv_ispair_def",
225                         "cv_size_def"];
226
227val b2c_def = Prim_rec.new_recursive_definition{
228  def = “b2c T = Num (SUC 0) /\ b2c F = Num 0”,
229  rec_axiom = TypeBase.axiom_of “:bool”,
230  name = "b2c_def"};
231val _ = BasicProvers.export_rewrites ["b2c_def"]
232
233Theorem b2c[simp]:
234  ((b2c x = Num 1) = x) /\
235  (b2c x = Num (SUC 0)) = x
236Proof
237  ASM_CASES_TAC “x:bool” \\ simp[ONE]
238QED
239
240
241Theorem b2c_if:
242  b2c g = if g then Num (SUC 0) else Num 0
243Proof
244  Cases_on ‘g’ >> simp[b2c_def]
245QED
246
247val cv_lt_def0 = recdef(
248  "cv_lt_def0",
249  “cv_lt (Num m) c = (case c of | Num n => b2c (m < n) | _ => Num 0) /\
250   cv_lt (Pair c d) e = Num 0”);
251
252Theorem cv_lt_def[simp]:
253  cv_lt (Num m) (Num n) = Num (if m < n then SUC 0 else 0) /\
254  cv_lt (Num m) (Pair p q) = Num 0 /\
255  cv_lt (Pair p q) (Num n) = Num 0 /\
256  cv_lt (Pair p q) (Pair r s) = Num 0
257Proof
258  simp[cv_lt_def0, b2c_if, SF boolSimps.COND_elim_ss]
259QED
260
261Inductive isnseq:
262[~nil:] isnseq (Num 0)
263[~cons:] (!n c. isnseq c ==> isnseq (Pair n c))
264End
265
266val cvnumval_def = recdef(
267  "cvnumval_def",
268  “cvnumval (Num n) = n /\ cvnumval (Pair c d) = 0”
269);
270
271val cvnum_map2_def = new_definition(
272  "cvnum_map2_def",
273  “cvnum_map2 f c d = Num (f (cvnumval c) (cvnumval d))”);
274
275val cv_add_def0 = new_definition ("cv_add_def0", “cv_add = cvnum_map2 $+”);
276Theorem cv_add_def[simp]:
277  cv_add (Num m) (Num n) = Num (m + n) /\
278  cv_add (Num m) (Pair p q) = Num m /\
279  cv_add (Pair p q) (Num n) = Num n /\
280  cv_add (Pair p q) (Pair r s) = Num 0
281Proof
282  simp[cv_add_def0, FUN_EQ_THM,cvnumval_def, cvnum_map2_def, ADD_CLAUSES]
283QED
284
285val cv_sub_def0 = new_definition("cv_sub_def0", “cv_sub = cvnum_map2 $-”);
286Theorem cv_sub_def[simp]:
287  cv_sub (Num m) (Num n) = Num (m - n) /\
288  cv_sub (Num m) (Pair p q) = Num m /\
289  cv_sub (Pair p q) (Num n) = Num 0 /\
290  cv_sub (Pair p q) (Pair r s) = Num 0
291Proof
292  simp[cv_sub_def0, FUN_EQ_THM, cvnum_map2_def, cvnumval_def, SUB_0]
293QED
294
295val cv_mul_def0 = new_definition("cv_mul_def0", “cv_mul = cvnum_map2 $*”);
296Theorem cv_mul_def[simp]:
297  cv_mul (Num m) (Num n) = Num (m * n) /\
298  cv_mul (Num m) (Pair p q) = Num 0 /\
299  cv_mul (Pair p q) (Num n) = Num 0 /\
300  cv_mul (Pair p q) (Pair r s) = Num 0
301Proof
302  simp[cv_mul_def0, FUN_EQ_THM, cvnum_map2_def, cvnumval_def]
303QED
304
305val cv_div_def0 = new_definition("cv_div_def0", “cv_div = cvnum_map2 $DIV”);
306Theorem cv_div_def[simp]:
307  cv_div (Num m) (Num n) = Num (m DIV n) /\
308  cv_div (Num m) (Pair p q) = Num 0 /\
309  cv_div (Pair p q) (Num n) = Num 0 /\
310  cv_div (Pair p q) (Pair r s) = Num 0
311Proof
312  simp[cv_div_def0, FUN_EQ_THM, cvnum_map2_def, cvnumval_def]
313QED
314
315val cv_mod_def0 = new_definition("cv_mod_def0", “cv_mod = cvnum_map2 $MOD”);
316Theorem cv_mod_def[simp]:
317  cv_mod (Num m) (Num n) = Num (m MOD n) /\
318  cv_mod (Num m) (Pair p q) = Num m /\
319  cv_mod (Pair p q) (Num n) = Num 0 /\
320  cv_mod (Pair p q) (Pair r s) = Num 0
321Proof
322  simp[cv_mod_def0, FUN_EQ_THM, cvnum_map2_def, cvnumval_def]
323QED
324
325val cv_eq_def0 = new_definition("cv_eq_def0", “cv_eq (c:cv) d = b2c (c = d)”);
326Theorem cv_eq_def:
327  cv_eq p q = Num (if p = q then SUC 0 else 0)
328Proof
329  simp[cv_eq_def0, b2c_if, SF boolSimps.COND_elim_ss]
330QED
331Theorem cv_eq[simp]:
332  (cv_eq (Pair x y) (Pair x' y') = b2c (x = x' /\ y = y')) /\
333  (cv_eq (Num m) (Num n) = b2c (m = n)) /\
334  (cv_eq (Pair x y) (Num n) = b2c F) /\
335  (cv_eq (Num n) (Pair x y) = b2c F)
336Proof
337  simp [cv_eq_def0]
338QED
339
340(* -------------------------------------------------------------------------
341 * Extra characteristic theorems
342 * ------------------------------------------------------------------------- *)
343
344Theorem lemma[local]:
345  n:num <= m ==> (m - n = k <=> m = n + k)
346Proof
347  simp[SUB_RIGHT_EQ, LESS_EQ_0, EQ_IMP_THM, DISJ_IMP_THM, ADD_CLAUSES] >>
348  metisLib.METIS_TAC[LESS_EQUAL_ANTISYM]
349QED
350
351Theorem DIV_RECURSIVE:
352  m DIV n =
353    if n = 0 then 0 else
354    if m < n then 0 else
355      SUC ((m - n) DIV n)
356Proof
357  IF_CASES_TAC >- simp[] >>
358  IF_CASES_TAC >- simp[LESS_DIV_EQ_ZERO] >>
359  irule DIV_UNIQUE >>
360  Q.SUBGOAL_THEN ‘0 < n’ ASSUME_TAC >- ASM_REWRITE_TAC[GSYM NOT_ZERO_LT_ZERO] >>
361  drule_then (Q.SPEC_THEN ‘m - n’ strip_assume_tac) DIVISION >>
362  simp [ADD1, LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB, MULT_LEFT_1] >>
363  Q.EXISTS_TAC ‘(m - n) MOD n’ >> simp[] >>
364  RULE_ASSUM_TAC (SRULE [NOT_LESS]) >> Q.PAT_X_ASSUM ‘m - n = _’ mp_tac >>
365  simp[lemma] >> disch_then (CONV_TAC o LAND_CONV o K) >>
366  simp[AC ADD_COMM ADD_ASSOC]
367QED
368
369Theorem MOD_RECURSIVE:
370  m MOD n = if n = 0 then m else if m < n then m else (m - n) MOD n
371Proof
372  IF_CASES_TAC >> simp[] >> IF_CASES_TAC >> simp[LESS_MOD] >>
373  RULE_ASSUM_TAC (SRULE[NOT_LESS, NOT_ZERO_LT_ZERO]) >>
374  simp[SUB_MOD]
375QED
376
377Theorem CV_EQ:
378  ((Pair p q = Pair r s) = (if p = r then q = s else F)) /\
379  ((Pair p q = Num n) = F) /\
380  ((Num m = Num n) = (m = n))
381Proof
382  simp []
383QED
384
385Theorem LT_RECURSIVE:
386  ((m < 0) = F) /\
387  ((m < SUC n) = (if m = n then T else m < n))
388Proof
389  simp[prim_recTheory.LESS_THM, prim_recTheory.NOT_LESS_0]
390QED
391
392Theorem SUC_EQ:
393  ((SUC m = 0) = F) /\
394  ((SUC m = SUC n) = (m = n))
395Proof
396  simp[]
397QED
398
399Theorem cv_if_cong[defncong]:
400  (c2b P = c2b Q) /\
401  (c2b Q ==> x = x') /\
402  (~c2b Q ==> y = y') ==>
403    cv_if P x y = cv_if Q x' y'
404Proof
405  Cases_on ‘P’ >> Cases_on ‘Q’ >> simp[c2b_def, cv_if_def] >>
406  rpt (Q.RENAME_TAC [‘cv_if (Num m) _ _’] >> Cases_on ‘m’ >>
407       simp[c2b_def, cv_if_def])
408QED
409
410Theorem cv_if[simp]:
411  cv_if x y z = if c2b x then y else z
412Proof
413  simp[cv_if_def0]
414QED
415
416Theorem cv_extras[simp]:
417  (cv_lt v (Pair x y) = Num 0) /\
418  (cv_lt (Pair x y) v = Num 0) /\
419  (cv_add (Pair x y) v = case v of Pair a b => Num 0 | _ => v) /\
420  (cv_add v (Pair x y) = case v of Pair a b => Num 0 | _ => v) /\
421  (cv_sub (Pair x y) v = Num 0) /\
422  (cv_sub v (Pair x y) = case v of Pair a b => Num 0 | _ => v) /\
423  (cv_mul (Pair x y) v = Num 0) /\
424  (cv_mul v (Pair x y) = Num 0) /\
425  (cv_div (Pair x y) v = Num 0) /\
426  (cv_div v (Pair x y) = case v of Pair a b => Num 0 | _ => Num 0) /\
427  (cv_mod (Pair x y) v = Num 0) /\
428  (cv_mod v (Pair x y) = case v of Pair a b => Num 0 | _ => v)
429Proof
430  Cases_on `v` \\ simp [cv_lt_def, cv_add_def, cv_sub_def, cv_mul_def,
431                        cv_div_def, cv_mod_def]
432QED
433
434(* -------------------------------------------------------------------------
435 * Theorems used in automation
436 * ------------------------------------------------------------------------- *)
437
438Theorem c2b_if[local]:
439  c2b (Num (if b then SUC 0 else 0)) = b
440Proof
441  Cases_on ‘b’
442  \\ rewrite_tac [c2b_def,Num_11,SUC_EQ]
443  \\ once_rewrite_tac [EQ_SYM_EQ]
444  \\ rewrite_tac [SUC_EQ,EXISTS_REFL]
445QED
446
447Theorem neq_to_cv:
448  !m n. m = n <=> c2b (cv_eq (Num m) (Num n))
449Proof
450  rewrite_tac [cv_eq_def,c2b_if,Num_11]
451QED
452
453Theorem lt_to_cv:
454  m < n <=> c2b (cv_lt (Num m) (Num n))
455Proof
456  rewrite_tac [cv_lt_def,c2b_if,Num_11]
457QED
458
459Theorem gt_to_cv:
460  m > n <=> c2b (cv_lt (Num n) (Num m))
461Proof
462  rewrite_tac [cv_lt_def,c2b_if,Num_11,GREATER_DEF]
463QED
464
465Theorem le_to_cv:
466  m <= n <=> ~c2b (cv_lt (Num n) (Num m))
467Proof
468  rewrite_tac [GSYM NOT_LESS,lt_to_cv]
469QED
470
471Theorem ge_to_cv:
472  n >= m <=> ~c2b (cv_lt (Num n) (Num m))
473Proof
474  rewrite_tac [le_to_cv,GREATER_EQ]
475QED
476
477Theorem ODD_to_cv:
478  ODD n <=> c2b (cv_mod (Num n) (Num 2))
479Proof
480  rewrite_tac [ODD_EVEN,cv_mod_def]
481  \\ rewrite_tac [c2b_def,Num_11,EVEN_MOD2]
482  \\ Cases_on ‘n MOD 2’
483  \\ rewrite_tac [numTheory.NOT_SUC]
484  \\ once_rewrite_tac [EQ_SYM_EQ]
485  \\ rewrite_tac [numTheory.NOT_SUC,SUC_EQ,EXISTS_REFL]
486QED
487
488Theorem EVEN_to_cv:
489  EVEN n <=> ~c2b (cv_mod (Num n) (Num 2))
490Proof
491  rewrite_tac [EVEN_ODD,ODD_to_cv]
492QED
493
494Theorem c2n_def[simp,allow_rebind] = Prim_rec.new_recursive_definition {
495  name = "c2n_def",
496  rec_axiom = cv_Axiom,
497  def = “c2n (Num n) = n /\
498         c2n (Pair c d) = 0”
499};
500
501Theorem add_to_cv:
502  m + n = c2n (cv_add (Num m) (Num n))
503Proof
504  rewrite_tac [c2n_def,cv_add_def]
505QED
506
507Theorem suc_to_cv:
508  SUC m = c2n (cv_add (Num m) (Num 1))
509Proof
510  rewrite_tac [c2n_def,cv_add_def,ADD1]
511QED
512
513Theorem sub_to_cv:
514  m - n = c2n (cv_sub (Num m) (Num n))
515Proof
516  rewrite_tac [c2n_def,cv_sub_def]
517QED
518
519Theorem pre_to_cv:
520  PRE m = c2n (cv_sub (Num m) (Num 1))
521Proof
522  rewrite_tac [c2n_def,cv_sub_def,PRE_SUB1]
523QED
524
525Theorem mul_to_cv:
526  m * n = c2n (cv_mul (Num m) (Num n))
527Proof
528  rewrite_tac [c2n_def,cv_mul_def]
529QED
530
531Theorem div_to_cv:
532  m DIV n = c2n (cv_div (Num m) (Num n))
533Proof
534  rewrite_tac [c2n_def,cv_div_def]
535QED
536
537Theorem mod_to_cv:
538  m MOD n = c2n (cv_mod (Num m) (Num n))
539Proof
540  rewrite_tac [c2n_def,cv_mod_def]
541QED
542
543val cv_exp_def = new_definition("cv_exp_def",
544  “cv_exp m n = Num (c2n m ** c2n n)”);
545
546Theorem cv_exp_eq:
547  cv_exp b e =
548    cv_if e                                        (* e is a positive number *)
549          (cv_if (cv_mod e (Num 2))                (* e is odd               *)
550                 (cv_mul b (cv_exp b (cv_sub e (Num 1))))
551                 (let x = cv_exp b (cv_div e (Num 2))
552                  in cv_mul x x))
553          (Num 1)
554Proof
555  Cases_on ‘e’
556  \\ rewrite_tac [c2n_def,cv_exp_def,cv_if_def,EXP]
557  \\ Cases_on ‘m’
558  \\ rewrite_tac [c2n_def,cv_exp_def,cv_if_def,EXP,LET_THM]
559  \\ CONV_TAC (DEPTH_CONV BETA_CONV)
560  \\ rewrite_tac [cv_mul_def,cv_mod_def,cv_if_def]
561  \\ Cases_on ‘SUC n MOD 2’
562  \\ rewrite_tac [cv_if_def,Num_11,GSYM EXP_ADD, GSYM TIMES2,cv_div_def,
563                  cv_sub_def, GSYM PRE_SUB1,prim_recTheory.PRE,c2n_def]
564  \\ rewrite_tac [GSYM EXP]
565  >-
566   (AP_TERM_TAC
567    \\ ‘0 < 2’
568      by rewrite_tac [numeralTheory.numeral_distrib,numeralTheory.numeral_lt]
569    \\ imp_res_tac DIVISION
570    \\ pop_assum (K ALL_TAC)
571    \\ first_x_assum $ Q.SPEC_THEN ‘SUC n’ mp_tac
572    \\ asm_rewrite_tac [ADD_CLAUSES]
573    \\ strip_tac
574    \\ once_rewrite_tac [MULT_COMM]
575    \\ pop_assum $ assume_tac o GSYM \\ asm_rewrite_tac [])
576  \\ Cases_on ‘b’
577  \\ rewrite_tac [cv_mul_def,c2n_def,EXP,MULT_CLAUSES]
578QED
579
580Theorem exp_to_cv:
581  m ** n = c2n (cv_exp (Num m) (Num n))
582Proof
583  rewrite_tac [c2n_def,cv_exp_def]
584QED
585
586(* Properties that can help with manual termination proofs *)
587
588Theorem cv_ispair_cv_add[simp]:
589  cv_ispair (cv_add x y) = Num 0
590Proof
591  Cases_on`x` \\ Cases_on`y` \\ simp[]
592QED
593
594Theorem c2n_cv_add[simp]:
595  c2n (cv_add v1 v2) = c2n v1 + c2n v2
596Proof
597  Cases_on`v1` \\ Cases_on`v2` \\ simp[ADD_CLAUSES]
598QED
599
600Theorem c2n_cv_mul[simp]:
601  c2n (cv_mul v1 v2) = c2n v1 * c2n v2
602Proof
603  Cases_on`v1` \\ Cases_on`v2` \\ simp[]
604QED
605
606Theorem cv_lt_Num_0:
607  (c2b $ cv_lt (Num 0) x) = ∃n. x = Num (SUC n)
608Proof
609  Cases_on`x` \\ simp[cv_lt_def]
610  \\ Cases_on`m` \\ simp[LT, LESS_0_CASES]
611QED
612
613val _ = app Parse.permahide [“c2n”,“c2b”,“Num”,“Pair”];
614
615val _ = app delete_const ["P0", "N0", "iscv", "cvrel", "cvrelf",
616                          "cv_ABS", "cv_REP", "cvnum_map2", "cvnumval"];