1structure nestedCases (* :> nestedCases *) =
2struct
3
4open HolKernel Parse boolLib pairLib PairRules bossLib pairSyntax;
5
6(*-----------------------------------------------------------------------------------------*)
7(* This transformation deals with logical functions and case expressions written with      *)
8(* patterns.                                                                               *)
9(*-----------------------------------------------------------------------------------------*)
10
11(*-----------------------------------------------------------------------------------------*)
12(* Convert nested case expressions into conditional statements.                            *)
13(*-----------------------------------------------------------------------------------------*)
14
15(*-----------------------------------------------------------------------------------------*)
16(* For num_case.                                                                           *)
17(*-----------------------------------------------------------------------------------------*)
18
19val is_0_def = Define `
20  (is_0 0 = T) /\
21  (is_0 _ = F)`;
22
23val is_0_lem = Q.prove (
24  `is_0 z = (z = 0)`,
25  Cases_on `z` THEN
26  RW_TAC std_ss [is_0_def]
27  )
28
29val is_suc_def = Define `
30  (is_suc 0 = F) /\
31  (is_suc _ = T)`;
32
33val destruct_suc_def = Define `
34  (destruct_suc (SUC x) = x)`;
35
36val num_case_lem = Q.prove (
37  `num_case b f2 z =
38     if is_0 z then b
39     else let v = destruct_suc z in f2 v`,
40  Cases_on `z` THEN
41  RW_TAC std_ss [arithmeticTheory.num_case_compute, is_0_def, destruct_suc_def]
42  );
43
44
45(*-----------------------------------------------------------------------------------------*)
46(* Conversion.                                                                             *)
47(*-----------------------------------------------------------------------------------------*)
48
49val lems = [pairTheory.FORALL_PROD, pairTheory.pair_case_thm, num_case_lem, is_0_lem];
50
51fun elim_pattern_match defs =
52  List.map (SIMP_RULE std_ss lems) defs
53
54(*-----------------------------------------------------------------------------------------*)
55(* Example 1.                                                                              *)
56(*-----------------------------------------------------------------------------------------*)
57
58(*
59val gcd_def = Define `
60  (gcd (0, y) = y) /\
61  (gcd (SUC x, 0) = SUC x) /\
62  (gcd (SUC x, SUC y) = if y <= x then gcd (x - y, SUC y) else gcd (SUC x, y - x))`;
63
64val gcd_lem = Q.prove (
65  `!z. gcd z = pair_case (\v v1. num_case v1 (\v2. num_case (SUC v2)
66             (\v3. if v3 <= v2 then gcd(v2 - v3, SUC v3) else gcd (SUC v2, v3 - v2)) v1) v) z`,
67  SIMP_TAC std_ss [pairTheory.FORALL_PROD] THEN
68  Cases_on `p_1` THEN Cases_on `p_2` THEN
69  RW_TAC arith_ss [gcd_def]
70  );
71
72val results = elim_pattern_match [gcd_lem]
73
74*)
75
76(*-----------------------------------------------------------------------------------------*)
77
78end (* struct *)