author | wenzelm |
Sat, 16 Aug 2014 13:23:50 +0200 | |
changeset 57948 | 75724d71013c |
parent 54742 | 7a86358a3c0b |
child 57949 | b203a7644bf1 |
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 |
|
57948 | 9 |
val declare_atomize_elim : attribute |
27571 | 10 |
val atomize_elim_conv : Proof.context -> conv |
11 |
val full_atomize_elim_conv : Proof.context -> conv |
|
26582 | 12 |
val atomize_elim_tac : Proof.context -> int -> tactic |
13 |
end |
|
14 |
||
57948 | 15 |
structure Atomize_Elim : ATOMIZE_ELIM = |
26582 | 16 |
struct |
17 |
||
18 |
(* theory data *) |
|
31902 | 19 |
|
20 |
structure AtomizeElimData = Named_Thms |
|
21 |
( |
|
45294 | 22 |
val name = @{binding atomize_elim}; |
27571 | 23 |
val description = "atomize_elim rewrite rule"; |
26582 | 24 |
); |
25 |
||
57948 | 26 |
val _ = Theory.setup AtomizeElimData.setup; |
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 = |
|
33040 | 35 |
(pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0))) |
26582 | 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 |
|
33002 | 43 |
val pi' = 0 :: map (Integer.add 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 |
||
57948 | 51 |
(* convert !!thesis. (!!x y z. ... => thesis) ==> ... |
26582 | 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 = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
45294
diff
changeset
|
60 |
(forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
45294
diff
changeset
|
61 |
then_conv Raw_Simplifier.rewrite ctxt true (AtomizeElimData.get ctxt) |
35625 | 62 |
then_conv (fn ct' => if can Object_Logic.dest_judgment ct' |
26582 | 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 *) |
|
57948 | 72 |
fun is_forall_thesis t = |
27571 | 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 |
|
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
41228
diff
changeset
|
81 |
val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i) |
26582 | 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 *) |
|
57948 | 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 |
||
57948 | 98 |
fun ms_conv ctxt ct = |
26582 | 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 |
|
57948 | 106 |
ms_conv ctxt |
26582 | 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 |
42361 | 116 |
val thy = Proof_Context.theory_of ctxt |
27571 | 117 |
val _ $ thesis = Logic.strip_assums_concl subg |
57948 | 118 |
|
26582 | 119 |
(* Introduce a quantifier first if the thesis is not bound *) |
57948 | 120 |
val quantify_thesis = |
26582 | 121 |
if is_Bound thesis then all_tac |
122 |
else let |
|
27571 | 123 |
val cthesis = cterm_of thy thesis |
57948 | 124 |
val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis] |
26582 | 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 |
||
57948 | 134 |
val _ = |
135 |
Theory.setup |
|
136 |
(Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac)) |
|
137 |
"convert obtains statement to atomic object logic goal") |
|
26582 | 138 |
|
139 |
end |