1 2open HolKernel Parse boolLib bossLib term_tactic; 3open arithmeticTheory listTheory stringTheory; 4 5val _ = new_theory "source_values"; 6 7(* Values in the source semantics are binary trees where the 8 leaves are natural numbers (num) *) 9Datatype: 10 v = Pair v v | Num num 11End 12 13(* Since strings are not in the representation, we have a function that 14 coverts strings into numbers. Note that parsing and pretty printing 15 is set up so that printing reproduces these strings when possible. *) 16Definition name_def: 17 name [] = 0 ��� 18 name (c::cs) = ORD c * 256 ** (LENGTH cs) + name cs 19End 20 21Overload Name = �����n. Num (name n)��� 22 23(* Lists are terminated with Num 0 *) 24Definition list_def[simp]: 25 list [] = Num 0 ��� 26 list (x::xs) = Pair x (list xs) 27End 28 29(* various convenience functions below, most are automatic rewrites [simp] *) 30 31Definition less_def[simp]: 32 less (Num n) (Num m) <=> n < m 33End 34 35Definition plus_def[simp]: 36 plus (Num n) (Num m) = Num (n + m) 37End 38 39Definition minus_def[simp]: 40 minus (Num n) (Num m) = Num (n - m) 41End 42 43Definition div_def[simp]: 44 div (Num n) (Num m) = Num (n DIV m) 45End 46 47Definition head_def[simp]: 48 head (Pair x y) = x ��� 49 head v = v 50End 51 52Definition tail_def[simp]: 53 tail (Pair x y) = y ��� 54 tail v = v 55End 56 57Definition cons_def[simp]: 58 cons x y = Pair x y 59End 60 61Definition bool_def[simp]: 62 bool T = Num 1 ��� 63 bool F = Num 0 64End 65 66Definition map_def[simp]: 67 map f xs = list (MAP f xs) 68End 69 70Overload "list" = ���map���; 71 72Definition pair_def[simp]: 73 pair f g (x,y) = Pair (f x) (g y) 74End 75 76Definition option_def[simp]: 77 option f NONE = list [] ��� 78 option f (SOME x) = list [f x] 79End 80 81Definition char_def[simp]: 82 char c = Num (ORD c) 83End 84 85Definition isNum_def[simp]: 86 isNum (Num n) = T ��� isNum _ = F 87End 88 89Definition getNum_def[simp]: 90 getNum (Num n) = n ��� 91 getNum _ = 0 92End 93 94Definition el1_def[simp]: 95 el1 v = head (tail v) 96End 97 98Definition el2_def[simp]: 99 el2 v = el1 (tail v) 100End 101 102Definition el3_def[simp]: 103 el3 v = el2 (tail v) 104End 105 106Overload isNil[inferior] = ���isNum���; 107Overload el0[inferior] = ���head���; 108 109Theorem isNum_bool[simp]: 110 isNum (bool b) 111Proof 112 Cases_on ���b��� \\ EVAL_TAC 113QED 114 115Theorem v_size_def[simp] = fetch "-" "v_size_def"; 116 117Theorem all_macro_defs = LIST_CONJ [list_def, cons_def, bool_def, 118 map_def, pair_def, option_def]; 119 120Definition is_upper_def: 121 (* checks whether string (represented as num) starts with uppercase letter *) 122 is_upper n = 123 if n < 256:num then 124 if n < 65 (* ord A = 65 *) then F else 125 if n < 91 (* ord Z = 90 *) then T else F 126 else is_upper (n DIV 256) 127End 128 129Definition otherwise_def[simp]: 130 otherwise x = x 131End 132 133val _ = export_theory(); 134