author | wenzelm |
Fri, 13 Mar 2009 19:58:26 +0100 | |
changeset 30510 | 4120fc59dd85 |
parent 30161 | c26e515f1c29 |
child 30515 | bca05b17b618 |
permissions | -rw-r--r-- |
26582 | 1 |
(* Title: Tools/atomize_elim.ML |
2 |
Author: Alexander Krauss, TU Muenchen |
|
3 |
||
4 |
Turn elimination rules into atomic expressions in the object logic. |
|
5 |
*) |
|
6 |
||
7 |
signature ATOMIZE_ELIM = |
|
8 |
sig |
|
9 |
val declare_atomize_elim : attribute |
|
10 |
||
27571 | 11 |
val atomize_elim_conv : Proof.context -> conv |
12 |
val full_atomize_elim_conv : Proof.context -> conv |
|
26582 | 13 |
|
14 |
val atomize_elim_tac : Proof.context -> int -> tactic |
|
15 |
||
16 |
val setup : theory -> theory |
|
17 |
end |
|
18 |
||
19 |
structure AtomizeElim : ATOMIZE_ELIM = |
|
20 |
struct |
|
21 |
||
22 |
(* theory data *) |
|
27571 | 23 |
structure AtomizeElimData = NamedThmsFun( |
24 |
val name = "atomize_elim"; |
|
25 |
val description = "atomize_elim rewrite rule"; |
|
26582 | 26 |
); |
27 |
||
27571 | 28 |
val declare_atomize_elim = AtomizeElimData.add |
26582 | 29 |
|
30 |
(* More conversions: *) |
|
31 |
local open Conv in |
|
32 |
||
33 |
(* Compute inverse permutation *) |
|
34 |
fun invert_perm pi = |
|
35 |
(pi @ ((0 upto (fold (curry Int.max) pi 0)) \\ pi)) |
|
36 |
|> map_index I |
|
37 |
|> sort (int_ord o pairself snd) |
|
38 |
|> map fst |
|
39 |
||
40 |
(* rearrange_prems as a conversion *) |
|
41 |
fun rearrange_prems_conv pi ct = |
|
42 |
let |
|
43 |
val pi' = 0 :: map (curry op + 1) pi |
|
27571 | 44 |
val fwd = Thm.trivial ct |
26582 | 45 |
|> Drule.rearrange_prems pi' |
27571 | 46 |
val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd))) |
26582 | 47 |
|> Drule.rearrange_prems (invert_perm pi') |
27571 | 48 |
in Thm.equal_intr fwd back end |
26582 | 49 |
|
50 |
||
51 |
(* convert !!thesis. (!!x y z. ... => thesis) ==> ... |
|
52 |
==> (!!a b c. ... => thesis) |
|
53 |
==> thesis |
|
54 |
||
55 |
to |
|
56 |
||
57 |
(EX x y z. ...) | ... | (EX a b c. ...) |
|
58 |
*) |
|
27571 | 59 |
fun atomize_elim_conv ctxt ct = |
26582 | 60 |
(forall_conv (K (prems_conv ~1 ObjectLogic.atomize_prems)) ctxt |
27571 | 61 |
then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt) |
26582 | 62 |
then_conv (fn ct' => if can ObjectLogic.dest_judgment ct' |
63 |
then all_conv ct' |
|
64 |
else raise CTERM ("atomize_elim", [ct', ct]))) |
|
65 |
ct |
|
66 |
||
67 |
||
68 |
(* Move the thesis-quantifier inside over other quantifiers and unrelated prems *) |
|
69 |
fun thesis_miniscope_conv inner_cv ctxt = |
|
70 |
let |
|
71 |
(* check if the outermost quantifier binds the conclusion *) |
|
27571 | 72 |
fun is_forall_thesis t = |
73 |
case Logic.strip_assums_concl t of |
|
74 |
(_ $ Bound i) => i = length (Logic.strip_params t) - 1 |
|
75 |
| _ => false |
|
26582 | 76 |
|
77 |
(* move unrelated assumptions out of the quantification *) |
|
78 |
fun movea_conv ctxt ct = |
|
79 |
let |
|
80 |
val _ $ Abs (_, _, b) = term_of ct |
|
81 |
val idxs = fold_index (fn (i, t) => not (loose_bvar1 (t, 0)) ? cons i) |
|
82 |
(Logic.strip_imp_prems b) [] |
|
83 |
|> rev |
|
84 |
||
85 |
fun skip_over_assm cv = rewr_conv (Thm.symmetric Drule.norm_hhf_eq) |
|
86 |
then_conv (implies_concl_conv cv) |
|
87 |
in |
|
88 |
(forall_conv (K (rearrange_prems_conv idxs)) ctxt |
|
89 |
then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt))) |
|
90 |
ct |
|
91 |
end |
|
92 |
||
93 |
(* move current quantifier to the right *) |
|
94 |
fun moveq_conv ctxt = |
|
27571 | 95 |
(rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt)) |
26582 | 96 |
else_conv (movea_conv ctxt) |
97 |
||
98 |
fun ms_conv ctxt ct = |
|
99 |
if is_forall_thesis (term_of ct) |
|
100 |
then moveq_conv ctxt ct |
|
101 |
else (implies_concl_conv (ms_conv ctxt) |
|
102 |
else_conv |
|
27571 | 103 |
(forall_conv (ms_conv o snd) ctxt)) |
26582 | 104 |
ct |
105 |
in |
|
106 |
ms_conv ctxt |
|
107 |
end |
|
108 |
||
27571 | 109 |
val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv |
26582 | 110 |
|
111 |
end |
|
112 |
||
113 |
||
27571 | 114 |
fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) => |
26582 | 115 |
let |
27571 | 116 |
val thy = ProofContext.theory_of ctxt |
117 |
val _ $ thesis = Logic.strip_assums_concl subg |
|
26582 | 118 |
|
119 |
(* Introduce a quantifier first if the thesis is not bound *) |
|
120 |
val quantify_thesis = |
|
121 |
if is_Bound thesis then all_tac |
|
122 |
else let |
|
27571 | 123 |
val cthesis = cterm_of thy thesis |
26582 | 124 |
val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] |
125 |
@{thm meta_spec} |
|
126 |
in |
|
27571 | 127 |
compose_tac (false, rule, 1) i |
26582 | 128 |
end |
129 |
in |
|
130 |
quantify_thesis |
|
27571 | 131 |
THEN (CONVERSION (full_atomize_elim_conv ctxt) i) |
26582 | 132 |
end) |
133 |
||
134 |
val setup = Method.add_methods |
|
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30161
diff
changeset
|
135 |
[("atomize_elim", Method.ctxt_args (SIMPLE_METHOD' o atomize_elim_tac), |
26582 | 136 |
"convert obtains statement to atomic object logic goal")] |
27571 | 137 |
#> AtomizeElimData.setup |
26582 | 138 |
|
139 |
end |