author | wenzelm |
Sat, 02 Apr 2016 23:29:05 +0200 | |
changeset 62826 | eb94e570c1a4 |
parent 60801 | 7664e0916eec |
child 67149 | e61557884799 |
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 |
|
27571 | 9 |
val atomize_elim_conv : Proof.context -> conv |
10 |
val full_atomize_elim_conv : Proof.context -> conv |
|
26582 | 11 |
val atomize_elim_tac : Proof.context -> int -> tactic |
12 |
end |
|
13 |
||
57948 | 14 |
structure Atomize_Elim : ATOMIZE_ELIM = |
26582 | 15 |
struct |
16 |
||
57949 | 17 |
(* atomize_elim rules *) |
31902 | 18 |
|
57949 | 19 |
val named_theorems = |
20 |
Context.>>> (Context.map_theory_result |
|
21 |
(Named_Target.theory_init #> |
|
22 |
Named_Theorems.declare @{binding atomize_elim} "atomize_elim rewrite rule" ##> |
|
23 |
Local_Theory.exit_global)); |
|
26582 | 24 |
|
25 |
||
26 |
(* More conversions: *) |
|
27 |
local open Conv in |
|
28 |
||
29 |
(* Compute inverse permutation *) |
|
30 |
fun invert_perm pi = |
|
33040 | 31 |
(pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0))) |
26582 | 32 |
|> map_index I |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58956
diff
changeset
|
33 |
|> sort (int_ord o apply2 snd) |
26582 | 34 |
|> map fst |
35 |
||
36 |
(* rearrange_prems as a conversion *) |
|
37 |
fun rearrange_prems_conv pi ct = |
|
38 |
let |
|
33002 | 39 |
val pi' = 0 :: map (Integer.add 1) pi |
27571 | 40 |
val fwd = Thm.trivial ct |
26582 | 41 |
|> Drule.rearrange_prems pi' |
59582 | 42 |
val back = Thm.trivial (snd (Thm.dest_implies (Thm.cprop_of fwd))) |
26582 | 43 |
|> Drule.rearrange_prems (invert_perm pi') |
27571 | 44 |
in Thm.equal_intr fwd back end |
26582 | 45 |
|
46 |
||
57948 | 47 |
(* convert !!thesis. (!!x y z. ... => thesis) ==> ... |
26582 | 48 |
==> (!!a b c. ... => thesis) |
49 |
==> thesis |
|
50 |
||
51 |
to |
|
52 |
||
53 |
(EX x y z. ...) | ... | (EX a b c. ...) |
|
54 |
*) |
|
27571 | 55 |
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
|
56 |
(forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt |
57949 | 57 |
then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems) |
59970 | 58 |
then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct' |
26582 | 59 |
then all_conv ct' |
60 |
else raise CTERM ("atomize_elim", [ct', ct]))) |
|
61 |
ct |
|
62 |
||
63 |
||
64 |
(* Move the thesis-quantifier inside over other quantifiers and unrelated prems *) |
|
65 |
fun thesis_miniscope_conv inner_cv ctxt = |
|
66 |
let |
|
67 |
(* check if the outermost quantifier binds the conclusion *) |
|
57948 | 68 |
fun is_forall_thesis t = |
27571 | 69 |
case Logic.strip_assums_concl t of |
70 |
(_ $ Bound i) => i = length (Logic.strip_params t) - 1 |
|
71 |
| _ => false |
|
26582 | 72 |
|
73 |
(* move unrelated assumptions out of the quantification *) |
|
74 |
fun movea_conv ctxt ct = |
|
75 |
let |
|
59582 | 76 |
val _ $ Abs (_, _, b) = Thm.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
|
77 |
val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i) |
26582 | 78 |
(Logic.strip_imp_prems b) [] |
79 |
|> rev |
|
80 |
||
81 |
fun skip_over_assm cv = rewr_conv (Thm.symmetric Drule.norm_hhf_eq) |
|
82 |
then_conv (implies_concl_conv cv) |
|
83 |
in |
|
84 |
(forall_conv (K (rearrange_prems_conv idxs)) ctxt |
|
85 |
then_conv (funpow (length idxs) skip_over_assm (inner_cv ctxt))) |
|
86 |
ct |
|
87 |
end |
|
88 |
||
89 |
(* move current quantifier to the right *) |
|
57948 | 90 |
fun moveq_conv ctxt = |
27571 | 91 |
(rewr_conv @{thm swap_params} then_conv (forall_conv (moveq_conv o snd) ctxt)) |
26582 | 92 |
else_conv (movea_conv ctxt) |
93 |
||
57948 | 94 |
fun ms_conv ctxt ct = |
59582 | 95 |
if is_forall_thesis (Thm.term_of ct) |
26582 | 96 |
then moveq_conv ctxt ct |
97 |
else (implies_concl_conv (ms_conv ctxt) |
|
98 |
else_conv |
|
27571 | 99 |
(forall_conv (ms_conv o snd) ctxt)) |
26582 | 100 |
ct |
101 |
in |
|
57948 | 102 |
ms_conv ctxt |
26582 | 103 |
end |
104 |
||
27571 | 105 |
val full_atomize_elim_conv = thesis_miniscope_conv atomize_elim_conv |
26582 | 106 |
|
107 |
end |
|
108 |
||
109 |
||
27571 | 110 |
fun atomize_elim_tac ctxt = SUBGOAL (fn (subg, i) => |
26582 | 111 |
let |
42361 | 112 |
val thy = Proof_Context.theory_of ctxt |
27571 | 113 |
val _ $ thesis = Logic.strip_assums_concl subg |
57948 | 114 |
|
26582 | 115 |
(* Introduce a quantifier first if the thesis is not bound *) |
57948 | 116 |
val quantify_thesis = |
26582 | 117 |
if is_Bound thesis then all_tac |
118 |
else let |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59586
diff
changeset
|
119 |
val cthesis = Thm.global_cterm_of thy thesis |
60801 | 120 |
val rule = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cthesis)] [NONE, SOME cthesis] |
26582 | 121 |
@{thm meta_spec} |
122 |
in |
|
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
57949
diff
changeset
|
123 |
compose_tac ctxt (false, rule, 1) i |
26582 | 124 |
end |
125 |
in |
|
126 |
quantify_thesis |
|
27571 | 127 |
THEN (CONVERSION (full_atomize_elim_conv ctxt) i) |
26582 | 128 |
end) |
129 |
||
57948 | 130 |
val _ = |
131 |
Theory.setup |
|
132 |
(Method.setup @{binding atomize_elim} (Scan.succeed (SIMPLE_METHOD' o atomize_elim_tac)) |
|
133 |
"convert obtains statement to atomic object logic goal") |
|
26582 | 134 |
|
135 |
end |