1
2open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_synthesis_demo";
3
4open arithmeticTheory listTheory pairTheory lisp_sexpTheory lisp_synthesisLib;
5
6infix \\ val op \\ = op THEN;
7
8
9(* we start by proving a lemma which helps with termination proofs *)
10
11val term_lemma = prove(
12  ``!x. isDot x ==> LSIZE (CAR x) < LSIZE x /\ LSIZE (CDR x) < LSIZE x``,
13  Cases \\ EVAL_TAC \\ DECIDE_TAC);
14
15
16(* we define a few shallow embeddings *)
17
18val append_def = lisp_tDefine "append" `
19  append x y = if isDot x then Dot (CAR x) (append (CDR x) y) else y`
20  (WF_REL_TAC `measure (LSIZE o FST)` \\ SIMP_TAC std_ss [term_lemma]);
21
22val rev_def = lisp_tDefine "rev" `
23  rev x = if isDot x then append (rev (CDR x)) (Dot (CAR x) (Sym "NIL")) else x`
24  (WF_REL_TAC `measure (LSIZE)` \\ SIMP_TAC std_ss [term_lemma]);
25
26val len_def = lisp_tDefine "len" `
27  len x = if isDot x then LISP_ADD (len (CDR x)) (Val 1) else Val 0`
28  (WF_REL_TAC `measure (LSIZE)` \\ SIMP_TAC std_ss [term_lemma]);
29
30val part_def = lisp_tDefine "part" `
31  part pivot x res1 res2 =
32    if isDot x then
33      if isTrue (LISP_LESS (CAR x) pivot)
34      then part pivot (CDR x) (Dot (CAR x) res1) res2
35      else part pivot (CDR x) res1 (Dot (CAR x) res2)
36    else Dot res1 res2`
37  (WF_REL_TAC `measure (LSIZE o FST o SND)` \\ SIMP_TAC std_ss [term_lemma]);
38
39val LIZE_EQ_SUC = prove(
40  ``!x. (LSIZE x = SUC n) ==> LSIZE (CAR x) <= n /\ LSIZE (CDR x) <= n``,
41  Cases \\ EVAL_TAC \\ DECIDE_TAC);
42
43val part_LSIZE = prove(
44  ``!y x x1 x2.
45      LSIZE (part x y x1 x2) = SUC (LSIZE y + LSIZE x1 + LSIZE x2)``,
46  REVERSE Induct \\ ONCE_REWRITE_TAC [part_def]
47  \\ SIMP_TAC std_ss [isDot_def,LSIZE_def,CAR_def,CDR_def]
48  \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC)
49  |> Q.SPECL [`b`,`a`,`Sym "NIL"`,`Sym "NIL"`] |> MATCH_MP LIZE_EQ_SUC
50  |> REWRITE_RULE [ADD_0,LSIZE_def];
51
52val NOT_LISP_LESS_TWO = prove(
53  ``!x. ~isTrue (LISP_LESS (len x) (Val 2)) ==> isDot x``,
54  Cases \\ ONCE_REWRITE_TAC [len_def] \\ SIMP_TAC std_ss [isDot_def] \\ EVAL_TAC);
55
56val qsort_def = lisp_tDefine "qsort" `
57  qsort x =
58    if isTrue (LISP_LESS (len x) (Val 2)) then x else
59      let pivot = CAR x in
60      let res = part pivot (CDR x) (Sym "NIL") (Sym "NIL") in
61        append (qsort (CAR res)) (Dot pivot (qsort (CDR res)))`
62 (WF_REL_TAC `measure LSIZE` \\ REPEAT STRIP_TAC
63  \\ IMP_RES_TAC NOT_LISP_LESS_TWO
64  \\ FULL_SIMP_TAC std_ss [isDot_thm,LSIZE_def,CAR_def,CDR_def]
65  \\ STRIP_ASSUME_TAC part_LSIZE \\ DECIDE_TAC)
66
67
68(* we use our tool to derive corresponding deep embeddings *)
69
70val thms = synthesise_deep_embeddings ()
71
72val _ = export_theory();
73