1open bossLib Theory Datatype Drule Tactical Tactic translateTheory 2open Thm Term Lib listTheory ratTheory testTypesTheory Conv sexpTheory; 3 4val _ = new_theory "testFunctions"; 5 6(*****************************************************************************) 7(* Definitions: *) 8(* FLAT : flatten a list using three clauses *) 9(* *) 10(*****************************************************************************) 11 12val FLAT = Define ` 13 (FLAT [] = []) /\ 14 (FLAT ([]::xs) = FLAT xs) /\ 15 (FLAT (((y:'a)::ys)::xs) = y::FLAT (ys::xs))`; 16 17val SPLIT_def = tDefine "SPLIT" 18 `(split1 [] (X,Y) = (X,Y)) /\ 19 (split1 (x::ys) (X,Y) = split2 ys (x::X,Y)) /\ 20 (split2 [] (X,Y) = (X,Y)) /\ 21 (split2 (x::ys) (X,Y) = split1 ys (X,x::Y))` 22 (WF_REL_TAC `measure (sum_case (LENGTH o FST) (LENGTH o FST))` THEN 23 RW_TAC arith_ss [listTheory.LENGTH]); 24 25val merge_def = Define ` 26 (merge [] [] = []) /\ 27 (merge (a::b) [] = a::b) /\ 28 (merge [] (c::d) = c::d) /\ 29 (merge (a::b) (c::d) = 30 if a < c:num then a :: merge b (c::d) 31 else c :: merge (a::b) d)`; 32 33local 34fun varftac f tac (a,g) = 35let val v = f g 36in tac v (a,g) 37end 38val tactic = 39 completeInduct_on `LENGTH x` THEN 40 Cases THEN 41 TRY (varftac (rand o rand o rand o rand o rator) 42 (fn v => STRUCT_CASES_TAC (ISPEC v list_CASES))) THEN 43 RW_TAC arith_ss [LENGTH,SPLIT_def,arithmeticTheory.ADD1] THEN 44 varftac (rand o rand o rator o rand o rand) 45 (fn v => POP_ASSUM (MP_TAC o ISPEC ``LENGTH (^v)``) THEN RW_TAC arith_ss []) THEN 46 varftac (rand o rand o rator o rand o rand) 47 (fn v => POP_ASSUM (MP_TAC o ISPEC v) THEN RW_TAC arith_ss [] THEN 48 DISJ_CASES_TAC (ISPEC ``1 < LENGTH (^v)`` boolTheory.EXCLUDED_MIDDLE) THEN1 49 METIS_TAC [arithmeticTheory.LESS_TRANS, 50 DECIDE ``SUC a + b < a + (b + 2n)``,LENGTH]) THEN 51 varftac (rand o rand o rator o rand o rand) 52 (fn v => REPEAT (POP_ASSUM MP_TAC) THEN 53 STRUCT_CASES_TAC (ISPEC v listTheory.list_CASES) THEN 54 RW_TAC arith_ss [LENGTH,SPLIT_def,arithmeticTheory.ADD1]) THEN 55 varftac (rand o rand o rator o rand o rand) 56 (fn v => REPEAT (POP_ASSUM MP_TAC) THEN 57 STRUCT_CASES_TAC (ISPEC v list_CASES)) THEN 58 RW_TAC arith_ss [LENGTH,SPLIT_def,arithmeticTheory.ADD1] 59in 60val length_split1_lemma1 = prove(``!x a b. 1 < LENGTH x ==> 61 (LENGTH (FST (split1 x (a,b))) < LENGTH x + LENGTH a)``,tactic); 62val length_split1_lemma2 = prove(``!x a b. 1 < LENGTH x ==> 63 (LENGTH (SND (split1 x (a,b))) < LENGTH x + LENGTH b)``,tactic); 64end; 65 66val merge_sort_def = tDefine "merge_sort" ` 67 (merge_sort xs = 68 if LENGTH xs <= 1 then xs 69 else let (left,right) = split1 xs ([],[]) 70 in merge (merge_sort left) (merge_sort right))` 71 (WF_REL_TAC `measure LENGTH` THEN 72 RW_TAC std_ss [] THEN 73 METIS_TAC [arithmeticTheory.NOT_LESS_EQUAL, 74 SIMP_RULE std_ss [LENGTH] (Q.SPECL [`xs`,`[]`,`[]`] length_split1_lemma2), 75 SIMP_RULE std_ss [LENGTH] (Q.SPECL [`xs`,`[]`,`[]`] length_split1_lemma1), 76 pairTheory.PAIR,pairTheory.PAIR_EQ]); 77 78val EVEN_EXTEND_def= store_thm("EVEN_EXTEND_def", 79 ``(EVEN 0 = T) /\ 80 (EVEN (SUC 0) = F) /\ 81 (!n. EVEN (SUC (SUC n)) = EVEN n)``, 82 RW_TAC arith_ss [arithmeticTheory.EVEN]); 83 84val ODD_EVEN_def = store_thm("ODD_EVEN_def", 85 ``(EVEN 0 = T) /\ (ODD 0 = F) /\ 86 (!n. EVEN (SUC n) = ODD n) /\ (!n. ODD (SUC n) = EVEN n)``, 87 RW_TAC arith_ss [arithmeticTheory.EVEN,arithmeticTheory.ODD, 88 arithmeticTheory.ODD_EVEN]); 89 90val ECASE = Define ` 91 (ECASE 0 _ = T) /\ 92 (ECASE (SUC 0) _ = T) /\ 93 (ECASE (SUC (SUC n)) [] = T)`; 94 95val LCASE = Define ` 96 (LCASE [] _ = T) /\ 97 (LCASE [x] _ = F) /\ 98 (LCASE (x::y::xys) 0n = T)`; 99 100val OLIST = Define ` 101 (OLIST [] = []) /\ 102 (OLIST (SOME x :: xs) = x :: OLIST xs) /\ 103 (OLIST (NONE :: xs) = OLIST xs)`; 104 105val FLATTEN_TREE = Define ` 106 (FLATTEN_TREE (TLeaf a) = [a]) /\ 107 (FLATTEN_TREE (TBranch t1 t2) = FLATTEN_TREE t1 ++ FLATTEN_TREE t2)`; 108 109val FT_FAST = Define ` 110 (FT_FAST (TLeaf a) A = (a::A)) /\ 111 (FT_FAST (TBranch t1 t2) A = FT_FAST t1 (FT_FAST t2 A))`; 112 113val ADDLIST_def = Define ` 114 (ADDLIST [] = 0n) /\ (ADDLIST (x::xs) = x + ADDLIST xs)`; 115 116val GENL_def = Define ` 117 (GENL 0 = []) /\ (GENL (SUC n) = n::GENL n)`; 118 119val ADDN_def = Define ` 120 (ADDN n = ADDLIST (GENL n))`; 121 122val _ = export_theory(); 123 124