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 *)