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