EVAL_quoteScript.sml

1Theory EVAL_quote
2Ancestors
3  ternaryComparisons
4Libs
5  TotalDefn Datatype BasicProvers
6
7Datatype:
8   index = Left_idx index
9         | Right_idx index
10         | End_idx
11End
12
13Definition index_compare_def:
14   (index_compare End_idx End_idx = EQUAL)
15/\ (index_compare End_idx i = LESS)
16/\ (index_compare i End_idx = GREATER)
17/\ (index_compare (Left_idx n') (Left_idx m') = (index_compare n' m'))
18/\ (index_compare (Left_idx n') (Right_idx m') = LESS)
19/\ (index_compare (Right_idx n') (Right_idx m') = (index_compare n' m'))
20/\ (index_compare (Right_idx n') (Left_idx m') = GREATER)
21End
22
23
24fun type_rws ty = #rewrs (TypeBase.simpls_of ty)
25
26val index_discr = tl (type_rws ``:index``);
27
28
29Theorem compare_index_equal:
30   !i1 i2. (index_compare i1 i2 = EQUAL) = (i1 = i2)
31Proof
32Induct THEN Induct THEN
33RW_TAC bool_ss (index_compare_def :: index_discr)
34QED
35
36
37val compare_list_index = save_thm(
38  "compare_list_index",
39  MATCH_MP compare_equal compare_index_equal);
40
41
42Definition index_lt_def:    index_lt i1 i2 = (index_compare i1 i2 = LESS)
43End
44
45
46Datatype:
47   varmap =
48     Empty_vm
49   | Node_vm 'a varmap varmap
50End
51
52
53Definition varmap_find_def:
54   (varmap_find End_idx        (Node_vm x v1 v2) = x:'a)
55/\ (varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2)
56/\ (varmap_find (Left_idx i1)  (Node_vm x v1 v2) = varmap_find i1 v1)
57/\ (varmap_find i v = @x.T)
58End