1 signature ComputeHOL = |
|
2 sig |
|
3 val prep_thms : thm list -> thm list |
|
4 val to_meta_eq : thm -> thm |
|
5 val to_hol_eq : thm -> thm |
|
6 val symmetric : thm -> thm |
|
7 val trans : thm -> thm -> thm |
|
8 end |
|
9 |
|
10 structure ComputeHOL : ComputeHOL = |
|
11 struct |
|
12 |
|
13 fun all_prems_conv ci ct = Conv.prems_conv (Logic.count_prems (term_of ct)) ci ct |
|
14 |
|
15 local |
|
16 fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); |
|
17 in |
|
18 fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", []) |
|
19 | rewrite_conv (eq :: eqs) ct = |
|
20 Thm.instantiate (Thm.match (lhs_of eq, ct)) eq |
|
21 handle Pattern.MATCH => rewrite_conv eqs ct; |
|
22 end |
|
23 |
|
24 val convert_conditions = Conv.fconv_rule (all_prems_conv (fn _ => Conv.else_conv (rewrite_conv [@{thm "Trueprop_eq_eq"}], Conv.all_conv))) |
|
25 |
|
26 val eq_th = @{thm "HOL.eq_reflection"} |
|
27 val meta_eq_trivial = @{thm "ComputeHOL.meta_eq_trivial"} |
|
28 val bool_to_true = @{thm "ComputeHOL.bool_to_true"} |
|
29 |
|
30 fun to_meta_eq th = eq_th OF [th] handle THM _ => meta_eq_trivial OF [th] handle THM _ => bool_to_true OF [th] |
|
31 |
|
32 fun to_hol_eq th = @{thm "meta_eq_imp_eq"} OF [th] handle THM _ => @{thm "eq_trivial"} OF [th] |
|
33 |
|
34 fun prep_thms ths = map (convert_conditions o to_meta_eq) ths |
|
35 |
|
36 local |
|
37 val sym_HOL = @{thm "HOL.sym"} |
|
38 val sym_Pure = @{thm "ProtoPure.symmetric"} |
|
39 in |
|
40 fun symmetric th = ((sym_HOL OF [th]) handle THM _ => (sym_Pure OF [th])) |
|
41 end |
|
42 |
|
43 local |
|
44 val trans_HOL = @{thm "HOL.trans"} |
|
45 val trans_HOL_1 = @{thm "ComputeHOL.transmeta_1"} |
|
46 val trans_HOL_2 = @{thm "ComputeHOL.transmeta_2"} |
|
47 val trans_HOL_3 = @{thm "ComputeHOL.transmeta_3"} |
|
48 fun tr [] th1 th2 = trans_HOL OF [th1, th2] |
|
49 | tr (t::ts) th1 th2 = (t OF [th1, th2] handle THM _ => tr ts th1 th2) |
|
50 in |
|
51 fun trans th1 th2 = tr [trans_HOL, trans_HOL_1, trans_HOL_2, trans_HOL_3] th1 th2 |
|
52 end |
|
53 |
|
54 end |
|