author | Christian Urban <urbanc@in.tum.de> |
Sun, 25 Apr 2010 09:13:16 +0200 | |
changeset 1947 | 51f411b1197d |
parent 1866 | 6d4e4bf9bce6 |
child 2064 | 2725853f43b9 |
permissions | -rw-r--r-- |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
1 |
(* Title: nominal_permeq.ML |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
2 |
Author: Christian Urban |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
3 |
Author: Brian Huffman |
1037
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 |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
signature NOMINAL_PERMEQ = |
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
sig |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
8 |
val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
9 |
val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic |
1947 | 10 |
|
11 |
val perm_simp_meth: thm list * string list -> Proof.context -> Method.method |
|
12 |
val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method |
|
13 |
val args_parser: (thm list * string list) context_parser |
|
14 |
||
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
|
15 |
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
|
16 |
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
|
17 |
end; |
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
19 |
(* |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
20 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
21 |
- eqvt_tac and eqvt_strict_tac take a list of theorems |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
22 |
which are first tried to simplify permutations |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
23 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
24 |
the string list contains constants that should not be |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
25 |
analysed (for example there is no raw eqvt-lemma for |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
26 |
the constant The; therefore it should not be analysed |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
28 |
- setting [[trace_eqvt = true]] switches on tracing |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
29 |
information |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
30 |
|
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
32 |
TODO: |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
33 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
34 |
- provide a proper parser for the method (see Nominal2_Eqvt) |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
35 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
36 |
- proably the list of bad constant should be a dataslot |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
*) |
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
|
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
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
|
41 |
struct |
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
43 |
open Nominal_ThmDecls; |
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
|
44 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
45 |
(* tracing infrastructure *) |
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
|
46 |
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
|
47 |
|
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 |
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
|
49 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
50 |
fun trace_msg ctxt result = |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
51 |
let |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
52 |
val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
53 |
val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
54 |
in |
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
parents:
1801
diff
changeset
|
55 |
warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
56 |
end |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
57 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
58 |
fun trace_conv ctxt conv ctrm = |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
59 |
let |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
60 |
val result = conv ctrm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
61 |
in |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
62 |
if Thm.is_reflexive result |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
63 |
then result |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
64 |
else (trace_msg ctxt result; result) |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
65 |
end |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
66 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
67 |
(* this conversion always fails, but prints |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
68 |
out the analysed term *) |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
69 |
fun trace_info_conv ctxt ctrm = |
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
|
70 |
let |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
71 |
val trm = term_of ctrm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
72 |
val _ = case (head_of trm) of |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
73 |
@{const "Trueprop"} => () |
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
parents:
1801
diff
changeset
|
74 |
| _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
75 |
in |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
76 |
Conv.no_conv ctrm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
77 |
end |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
78 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
79 |
(* conversion for applications: |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
80 |
only applies the conversion, if the head of the |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
81 |
application is not a "bad head" *) |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
82 |
fun has_bad_head bad_hds trm = |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
83 |
case (head_of trm) of |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
84 |
Const (s, _) => member (op=) bad_hds s |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
85 |
| _ => false |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
86 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
87 |
fun eqvt_apply_conv bad_hds ctrm = |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
88 |
case (term_of ctrm) of |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
89 |
Const (@{const_name "permute"}, _) $ _ $ (trm $ _) => |
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
|
90 |
let |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
91 |
val (perm, t) = Thm.dest_comb ctrm |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
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
|
93 |
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
|
94 |
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
|
95 |
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
|
96 |
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
|
97 |
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
|
98 |
in |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
99 |
if has_bad_head bad_hds trm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
100 |
then Conv.no_conv ctrm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
101 |
else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
end |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
103 |
| _ => Conv.no_conv ctrm |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
|
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
|
105 |
(* conversion for lambdas *) |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
106 |
fun eqvt_lambda_conv ctrm = |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
107 |
case (term_of ctrm) of |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
108 |
Const (@{const_name "permute"}, _) $ _ $ (Abs _) => |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
109 |
Conv.rewr_conv @{thm eqvt_lambda} ctrm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
110 |
| _ => Conv.no_conv ctrm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
111 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
112 |
(* conversion that raises an error or prints a warning message, |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
113 |
if a permutation on a constant or application cannot be analysed *) |
1866
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
114 |
fun progress_info_conv ctxt strict_flag bad_hds ctrm = |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
115 |
let |
1866
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
116 |
fun msg trm = |
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
117 |
let |
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
118 |
val hd = head_of trm |
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
119 |
in |
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
120 |
if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () |
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
121 |
else (if strict_flag then error else warning) |
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
122 |
("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
123 |
end |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
124 |
|
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
125 |
val _ = case (term_of ctrm) of |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
126 |
Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
127 |
| Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
128 |
| _ => () |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
129 |
in |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
130 |
Conv.all_conv ctrm |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
131 |
end |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
|
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
|
133 |
(* main conversion *) |
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
parents:
1801
diff
changeset
|
134 |
fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = |
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
|
135 |
let |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
136 |
val first_conv_wrapper = |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
137 |
if trace_enabled ctxt |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
138 |
then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
139 |
else Conv.first_conv |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
140 |
|
1810
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1803
diff
changeset
|
141 |
val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
parents:
1803
diff
changeset
|
142 |
val post_thms = map safe_mk_equiv @{thms permute_pure} |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
in |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
144 |
first_conv_wrapper |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
145 |
[ More_Conv.rewrs_conv pre_thms, |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
146 |
eqvt_apply_conv bad_hds, |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
147 |
eqvt_lambda_conv, |
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
148 |
More_Conv.rewrs_conv post_thms, |
1866
6d4e4bf9bce6
automatic proofs for equivariance of alphas
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
149 |
progress_info_conv ctxt strict_flag bad_hds |
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
150 |
] ctrm |
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
151 |
end |
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
152 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
153 |
(* raises an error if some permutations cannot be eliminated *) |
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
parents:
1801
diff
changeset
|
154 |
fun eqvt_strict_tac ctxt user_thms bad_hds = |
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
parents:
1801
diff
changeset
|
155 |
CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) 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
|
156 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
157 |
(* prints a warning message if some permutations cannot be eliminated *) |
1803
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
parents:
1801
diff
changeset
|
158 |
fun eqvt_tac ctxt user_thms bad_hds = |
ed46cf122016
used warning instead of tracing (does not seem to produce stable output)
Christian Urban <urbanc@in.tum.de>
parents:
1801
diff
changeset
|
159 |
CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) 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
|
160 |
|
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
parents:
1800
diff
changeset
|
161 |
(* setup of the configuration value *) |
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
|
162 |
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
|
163 |
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
|
164 |
|
1947 | 165 |
|
166 |
(** methods **) |
|
167 |
||
168 |
val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
|
169 |
val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
|
170 |
(Scan.repeat (Args.const true))) [] |
|
171 |
||
172 |
val args_parser = |
|
173 |
add_thms_parser -- exclude_consts_parser || |
|
174 |
exclude_consts_parser -- add_thms_parser >> swap |
|
175 |
||
176 |
fun perm_simp_meth (thms, consts) ctxt = |
|
177 |
SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) |
|
178 |
||
179 |
fun perm_strict_simp_meth (thms, consts) ctxt = |
|
180 |
SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) |
|
181 |
||
1037
2845e736dc1a
added a first eqvt_tac which pushes permutations inside terms
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
182 |
end; (* structure *) |