| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 09 Apr 2010 21:51:01 +0200 | |
| changeset 1800 | 78fdc6b36a1c |
| parent 1774 | c34347ec7ab3 |
| child 1801 | 6d2a39db3862 |
| permissions | -rw-r--r-- |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: nominal_thmdecls.ML |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Brian Huffman, Christian Urban |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
*) |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
signature NOMINAL_PERMEQ = |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
sig |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
7 |
val eqvt_tac: Proof.context -> thm list -> int -> tactic |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
8 |
val trace_eqvt: bool Config.T |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
9 |
val setup: theory -> theory |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
end; |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
(* TODO: |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
- provide a method interface with the usual add and del options |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
- print a warning if for a constant no eqvt lemma is stored |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
*) |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
structure Nominal_Permeq: NOMINAL_PERMEQ = |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
struct |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
|
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
24 |
fun is_head_Trueprop trm = |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
25 |
case (head_of trm) of |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
26 |
@{const "Trueprop"} => true
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
27 |
| _ => false |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
28 |
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
29 |
(* debugging infrastructure *) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
30 |
val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
31 |
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
32 |
fun trace_enabled ctxt = Config.get ctxt trace_eqvt |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
34 |
fun trace_conv ctxt conv ct = |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
35 |
let |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
36 |
val result = conv ct |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
37 |
val _ = |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
38 |
if trace_enabled ctxt andalso not (Thm.is_reflexive result) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
39 |
then |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
40 |
let |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
41 |
val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
42 |
val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
43 |
in |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
44 |
warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
45 |
end |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
46 |
else () |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
47 |
in |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
48 |
result |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
49 |
end; |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
50 |
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
51 |
(* conversion for applications *) |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
fun eqvt_apply_conv ctxt ct = |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
case (term_of ct) of |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
(Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
let |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
val (perm, t) = Thm.dest_comb ct |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
val (_, p) = Thm.dest_comb perm |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
val (f, x) = Thm.dest_comb t |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
val a = ctyp_of_term x; |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
val b = ctyp_of_term t; |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
val ty_insts = map SOME [b, a] |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
62 |
val term_insts = map SOME [p, f, x] |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
in |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
end |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
| _ => Conv.no_conv ct |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
|
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
68 |
(* conversion for lambdas *) |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
fun eqvt_lambda_conv ctxt ct = |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
case (term_of ct) of |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
(Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
Conv.rewr_conv @{thm eqvt_lambda} ct
|
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
| _ => Conv.no_conv ct |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
|
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
75 |
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
76 |
(* main conversion *) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
77 |
fun eqvt_conv ctxt thms ctrm = |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
78 |
let |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
79 |
val trm = term_of ctrm |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
80 |
val _ = if trace_enabled ctxt andalso not (is_head_Trueprop trm) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
81 |
then warning ("analysing " ^ Syntax.string_of_term ctxt trm)
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
82 |
else () |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
83 |
val wrapper = if trace_enabled ctxt then trace_conv ctxt else I |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
in |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
85 |
Conv.first_conv (map wrapper |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
86 |
[ More_Conv.rewrs_conv thms, |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
87 |
Conv.rewr_conv @{thm eqvt_bound},
|
|
1066
96651cddeba9
eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts
Christian Urban <urbanc@in.tum.de>
parents:
1059
diff
changeset
|
88 |
More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvts_raw_thms ctxt), |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
89 |
eqvt_apply_conv ctxt, |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
90 |
eqvt_lambda_conv ctxt, |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
91 |
More_Conv.rewrs_conv @{thms permute_pure[THEN eq_reflection]},
|
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
Conv.all_conv |
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
93 |
]) ctrm |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
end |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
|
|
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
96 |
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
97 |
fun eqvt_tac ctxt thms = |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
98 |
CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt thms) ctxt) |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
99 |
|
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
100 |
val setup = |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
101 |
trace_eqvt_setup |
|
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents:
1774
diff
changeset
|
102 |
|
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
end; (* structure *) |