136 (* Everything together *) |
136 (* Everything together *) |
137 (***********************) |
137 (***********************) |
138 |
138 |
139 lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let |
139 lemmas compute_hol = compute_if compute_bool compute_pair compute_option compute_list compute_let |
140 |
140 |
|
141 ML {* |
|
142 signature ComputeHOL = |
|
143 sig |
|
144 val prep_thms : thm list -> thm list |
|
145 val to_meta_eq : thm -> thm |
|
146 val to_hol_eq : thm -> thm |
|
147 val symmetric : thm -> thm |
|
148 val trans : thm -> thm -> thm |
141 end |
149 end |
|
150 |
|
151 structure ComputeHOL : ComputeHOL = |
|
152 struct |
|
153 |
|
154 local |
|
155 fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); |
|
156 in |
|
157 fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", []) |
|
158 | rewrite_conv (eq :: eqs) ct = |
|
159 Thm.instantiate (Thm.match (lhs_of eq, ct)) eq |
|
160 handle Pattern.MATCH => rewrite_conv eqs ct; |
|
161 end |
|
162 |
|
163 val convert_conditions = Conv.fconv_rule (Conv.prems_conv ~1 (Conv.try_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}]))) |
|
164 |
|
165 val eq_th = @{thm "HOL.eq_reflection"} |
|
166 val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"} |
|
167 val bool_to_true = @{thm "ComputeHOL.bool_to_true"} |
|
168 |
|
169 fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th] |
|
170 |
|
171 fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] |
|
172 |
|
173 fun prep_thms ths = map (convert_conditions o to_meta_eq) ths |
|
174 |
|
175 local |
|
176 val sym_HOL = @{thm "HOL.sym"} |
|
177 val sym_Pure = @{thm "ProtoPure.symmetric"} |
|
178 in |
|
179 fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th])) |
|
180 end |
|
181 |
|
182 local |
|
183 val trans_HOL = @{thm "HOL.trans"} |
|
184 val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"} |
|
185 val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"} |
|
186 val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"} |
|
187 fun tr [] th1 th2 = trans_HOL OF [th1, th2] |
|
188 | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) |
|
189 in |
|
190 fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2 |
|
191 end |
|
192 |
|
193 end |
|
194 *} |
|
195 |
|
196 end |