EncodeVarScript.sml
1(* -*-sml-*-
2app load
3["bossLib", "CoderTheory"];
4*)
5Theory EncodeVar
6Ancestors
7 list Encode Decode Coder
8Libs
9 simpLib
10
11
12val _ = ParseExtras.temp_loose_equality()
13
14val Suff = Q_TAC SUFF_TAC;
15val Know = Q_TAC KNOW_TAC;
16
17val REVERSE = Tactical.REVERSE;
18
19(*---------------------------------------------------------------------------
20 Fixed size encodings---necessary for encoding variables.
21 ---------------------------------------------------------------------------*)
22
23Definition fixed_width_def:
24 fixed_width n c = !x. domain c x ==> (LENGTH (encoder c x) = n)
25End
26
27local
28 val th = prove
29 (``?of_length. !(l : 'a list) n. l IN of_length n = (LENGTH l = n)``,
30 EXISTS_TAC ``\n (l : 'a list). LENGTH l = n`` THEN
31 SIMP_TAC bool_ss [IN_DEF]);
32in
33 val of_length_def = new_specification ("of_length_def", ["of_length"], th);
34end;
35
36Theorem fixed_width_univ:
37 !(phi : 'a -> bool) c n.
38 wf_coder c /\ fixed_width n c ==>
39 ((!x. domain c x ==> phi x) =
40 !w :: of_length n. phi (decoder c w))
41Proof
42 RW_TAC bool_ss [RES_FORALL_THM, fixed_width_def, of_length_def]
43 >> REPEAT (STRIP_TAC ORELSE EQ_TAC)
44 >> PROVE_TAC [wf_coder, wf_coder_closed]
45QED
46
47Theorem of_length_univ_suc:
48 !phi n.
49 (!w :: of_length (SUC n). phi (w : 'a list)) =
50 (!x. !w :: of_length n. phi (x :: w))
51Proof
52 SIMP_TAC bool_ss [RES_FORALL_THM, of_length_def] THEN
53 REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL
54 [Q.PAT_ASSUM `!x. Q x` MATCH_MP_TAC THEN
55 ASM_SIMP_TAC arith_ss [LENGTH],
56 MP_TAC (ISPEC ``w : 'a list`` list_CASES) THEN
57 STRIP_TAC THENL
58 [FULL_SIMP_TAC arith_ss [LENGTH],
59 FULL_SIMP_TAC arith_ss [LENGTH]]]
60QED
61
62Theorem of_length_univ_zero:
63 !phi. (!w :: of_length 0. phi w) = phi ([] : 'a list)
64Proof
65 SIMP_TAC bool_ss [RES_FORALL_THM, of_length_def, LENGTH_NIL]
66QED
67
68Theorem fixed_width_exists:
69 !(phi : 'a -> bool) c n.
70 wf_coder c /\ fixed_width n c ==>
71 ((?x. domain c x /\ phi x) =
72 ?w :: of_length n. phi (decoder c w))
73Proof
74 RW_TAC bool_ss [RES_EXISTS_THM, fixed_width_def, of_length_def]
75 >> REPEAT (STRIP_TAC ORELSE EQ_TAC)
76 >> PROVE_TAC [wf_coder, wf_coder_closed]
77QED
78
79Theorem of_length_exists_suc:
80 !phi n.
81 (?w :: of_length (SUC n). phi (w : 'a list)) =
82 (?x. ?w :: of_length n. phi (x :: w))
83Proof
84 SIMP_TAC bool_ss [RES_EXISTS_THM, of_length_def] THEN
85 REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL
86 [MP_TAC (ISPEC ``w:'a list`` list_CASES) THEN
87 (STRIP_TAC THEN1 FULL_SIMP_TAC arith_ss [LENGTH]) THEN
88 FULL_SIMP_TAC arith_ss [LENGTH] THEN
89 EXISTS_TAC ``h : 'a`` THEN
90 EXISTS_TAC ``t : 'a list`` THEN
91 ASM_SIMP_TAC bool_ss [],
92 EXISTS_TAC ``(x : 'a) :: w`` THEN
93 ASM_SIMP_TAC arith_ss [LENGTH]]
94QED
95
96Theorem of_length_exists_zero:
97 !phi. (?w :: of_length 0. phi w) = phi ([] : 'a list)
98Proof
99 SIMP_TAC bool_ss [RES_EXISTS_THM, of_length_def, LENGTH_NIL]
100QED
101
102(*---------------------------------------------------------------------------
103 Units
104 ---------------------------------------------------------------------------*)
105
106Theorem fixed_width_unit:
107 !p. fixed_width 0 (unit_coder p)
108Proof
109 SIMP_TAC arith_ss
110 [unit_coder_def, fixed_width_def, domain_def, encoder_def,
111 encode_unit_def, LENGTH]
112QED
113
114(*---------------------------------------------------------------------------
115 Booleans
116 ---------------------------------------------------------------------------*)
117
118Theorem fixed_width_bool:
119 !p. fixed_width 1 (bool_coder p)
120Proof
121 SIMP_TAC arith_ss
122 [bool_coder_def, fixed_width_def, domain_def, encoder_def,
123 encode_bool_def, LENGTH]
124QED
125
126(*---------------------------------------------------------------------------
127 Pairs
128 ---------------------------------------------------------------------------*)
129
130Theorem fixed_width_prod:
131 !c1 c2 n1 n2.
132 fixed_width n1 c1 /\ fixed_width n2 c2 ==>
133 fixed_width (n1 + n2) (prod_coder c1 c2)
134Proof
135 REPEAT GEN_TAC
136 >> Know `?p1 e1 d1. c1 = (p1, e1, d1)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
137 >> Know `?p2 e2 d2. c2 = (p2, e2, d2)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
138 >> RW_TAC std_ss []
139 >> REPEAT (POP_ASSUM MP_TAC)
140 >> RW_TAC std_ss [fixed_width_def, prod_coder_def, domain_def, encoder_def]
141 >> Cases_on `x`
142 >> FULL_SIMP_TAC std_ss [lift_prod_def, encode_prod_def, LENGTH_APPEND]
143QED
144
145(*---------------------------------------------------------------------------
146 Sums
147 ---------------------------------------------------------------------------*)
148
149Theorem fixed_width_sum:
150 !c1 c2 n.
151 fixed_width n c1 /\ fixed_width n c2 ==>
152 fixed_width (SUC n) (sum_coder c1 c2)
153Proof
154 REPEAT GEN_TAC
155 >> Know `?p1 e1 d1. c1 = (p1, e1, d1)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
156 >> Know `?p2 e2 d2. c2 = (p2, e2, d2)` >- PROVE_TAC [pairTheory.ABS_PAIR_THM]
157 >> RW_TAC std_ss []
158 >> REPEAT (POP_ASSUM MP_TAC)
159 >> RW_TAC std_ss [fixed_width_def, sum_coder_def, domain_def, encoder_def]
160 >> Cases_on `x`
161 >> FULL_SIMP_TAC std_ss [lift_sum_def, encode_sum_def, LENGTH]
162QED
163
164(*---------------------------------------------------------------------------
165 Bounded numbers
166 ---------------------------------------------------------------------------*)
167
168Theorem fixed_width_bnum:
169 !m p. fixed_width m (bnum_coder m p)
170Proof
171 RW_TAC std_ss
172 [fixed_width_def, encode_bnum_length, bnum_coder_def, encoder_def]
173QED
174