1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_sexp"; 2 3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 4open combinTheory finite_mapTheory stringTheory; 5 6 7infix \\ 8val op \\ = op THEN; 9val RW = REWRITE_RULE; 10val RW1 = ONCE_REWRITE_RULE; 11 12 13(* type *) 14 15val _ = Hol_datatype `SExp = Dot of SExp => SExp | Val of num | Sym of string`; 16val SExp_11 = fetch "-" "SExp_11"; 17val SExp_distinct = fetch "-" "SExp_distinct"; 18 19 20(* definitions *) 21 22val isDot_def = Define ` 23 (isDot (Dot x y) = T) /\ (isDot (Val n) = F) /\ (isDot (Sym s) = F)`; 24val isVal_def = Define ` 25 (isVal (Dot x y) = F) /\ (isVal (Val n) = T) /\ (isVal (Sym s) = F)`; 26val isSym_def = Define ` 27 (isSym (Dot x y) = F) /\ (isSym (Val n) = F) /\ (isSym (Sym s) = T)`; 28 29val getVal_def = Define ` 30 (getVal (Dot x y) = 0) /\ (getVal (Val n) = n) /\ (getVal (Sym s) = 0)`; 31val getSym_def = Define ` 32 (getSym (Dot x y) = "NIL") /\ (getSym (Val n) = "NIL") /\ (getSym (Sym s) = s)`; 33 34val CAR_def = Define ` 35 (CAR (Dot x y) = x) /\ 36 (CAR (Val w) = Sym "NIL") /\ 37 (CAR (Sym s) = Sym "NIL")`; 38 39val CDR_def = Define ` 40 (CDR (Dot x y) = y) /\ 41 (CDR (Val w) = Sym "NIL") /\ 42 (CDR (Sym s) = Sym "NIL")`; 43 44val LISP_CONS_def = Define `LISP_CONS x y = Dot x y`; 45 46val LISP_ADD_def = Define `LISP_ADD x y = Val (getVal x + getVal y)`; 47val LISP_SUB_def = Define `LISP_SUB x y = Val (getVal x - getVal y)`; 48val LISP_MULT_def = Define `LISP_MULT x y = Val (getVal x * getVal y)`; 49val LISP_DIV_def = Define `LISP_DIV x y = Val (getVal x DIV getVal y)`; 50val LISP_MOD_def = Define `LISP_MOD x y = Val (getVal x MOD getVal y)`; 51 52val LISP_TEST_def = Define `LISP_TEST x = if x then Sym "T" else Sym "NIL"`; 53 54val LISP_EQUAL_def = Define `LISP_EQUAL x y = LISP_TEST (x = y)`; 55val LISP_LESS_def = Define `LISP_LESS m n = LISP_TEST (getVal m < getVal n)`; 56val LISP_ATOMP_def = Define `LISP_ATOMP x = LISP_TEST (~(isDot x))`; 57val LISP_CONSP_def = Define `LISP_CONSP x = LISP_TEST (isDot x)`; 58val LISP_NUMBERP_def = Define `LISP_NUMBERP x = LISP_TEST (isVal x)`; 59val LISP_SYMBOLP_def = Define `LISP_SYMBOLP x = LISP_TEST (isSym x)`; 60val LISP_SYMBOL_LESS_def = Define `LISP_SYMBOL_LESS x y = LISP_TEST (getSym x < getSym y)`; 61 62val TASK_CONT_def = Define `TASK_CONT = Sym "T"`; 63val TASK_EVAL_def = Define `TASK_EVAL = Sym "NIL"`; 64val TASK_FUNC_def = Define `TASK_FUNC = Sym "QUOTE"`; 65 66val isQuote_def = Define ` 67 isQuote x = isDot x /\ (CAR x = Sym "QUOTE") /\ 68 isDot (CDR x) /\ (CDR (CDR x) = Sym "NIL")`; 69 70val LSIZE_def = Define ` 71 (LSIZE (Dot x y) = SUC (LSIZE x + LSIZE y)) /\ 72 (LSIZE (Val w) = 0) /\ 73 (LSIZE (Sym s) = 0)`; 74 75val LDEPTH_def = Define ` 76 (LDEPTH (Dot x y) = SUC (MAX (LDEPTH x) (LDEPTH y))) /\ 77 (LDEPTH (Val w) = 0) /\ 78 (LDEPTH (Sym s) = 0)`; 79 80val SUM_LSIZE_def = Define ` 81 (SUM_LSIZE [] = 0) /\ 82 (SUM_LSIZE (x::xs) = LSIZE x + SUM_LSIZE xs)`; 83 84val UPDATE_NTH_def = Define ` 85 (UPDATE_NTH 0 x [] = []) /\ 86 (UPDATE_NTH (SUC n) x [] = []) /\ 87 (UPDATE_NTH 0 x (y::ys) = x::ys) /\ 88 (UPDATE_NTH (SUC n) x (y::ys) = y::UPDATE_NTH n (x:'a) ys)`; 89 90val _ = Hol_datatype ` 91 lisp_primitive_op = 92 opCONS | opEQUAL | opLESS | opSYMBOL_LESS | opADD | opSUB | 93 opCONSP | opNATP | opSYMBOLP | opCAR | opCDR`; 94 95val isTrue_def = Define `isTrue s = ~(s = Sym "NIL")`; 96 97 98(* theorems *) 99 100val SExp_expand = store_thm("SExp_expand", 101 ``!x. (?exp1 exp2. x = Dot exp1 exp2) \/ (?n. x = Val n) \/ (?s. x = Sym s)``, 102 Cases \\ SRW_TAC [] []); 103 104val isDot_thm = store_thm("isDot_thm", 105 ``!z. isDot z = ?a b. z = Dot a b``, 106 Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isDot_def]); 107 108val isVal_thm = store_thm("isVal_thm", 109 ``!z. isVal z = ?a. z = Val a``, 110 Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isVal_def]); 111 112val isSym_thm = store_thm("isSym_thm", 113 ``!z. isSym z = ?a. z = Sym a``, 114 Cases \\ SIMP_TAC std_ss [SExp_11,SExp_distinct,isSym_def]); 115 116val isQuote_thm = store_thm("isQuote_thm", 117 ``!x. isQuote x = ?y. x = Dot (Sym "QUOTE") (Dot y (Sym "NIL"))``, 118 Cases \\ REWRITE_TAC [isQuote_def,isDot_def,CAR_def,CDR_def,SExp_11] 119 \\ SIMP_TAC std_ss [SExp_distinct] \\ Cases_on `S0` 120 \\ REWRITE_TAC [isQuote_def,isDot_def,CAR_def,CDR_def,SExp_11] 121 \\ METIS_TAC [SExp_distinct]); 122 123 124val _ = export_theory(); 125