author | wenzelm |
Mon, 25 Jun 2012 15:14:07 +0200 | |
changeset 48124 | 87c831e30f0a |
parent 48109 | 0a58f7eefba2 |
child 48128 | bf172a5929bb |
permissions | -rw-r--r-- |
48124 | 1 |
(* Title: HOL/Tools/set_comprehension_pointfree.ML |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
2 |
Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen |
48124 | 3 |
Author: Rafal Kolanski, NICTA |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
4 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
5 |
Simproc for rewriting set comprehensions to pointfree expressions. |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
6 |
*) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
7 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
8 |
signature SET_COMPREHENSION_POINTFREE = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
9 |
sig |
48124 | 10 |
val simproc : simpset -> cterm -> thm option |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
11 |
val rewrite_term : term -> term option |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
12 |
val conv : Proof.context -> term -> thm option |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
13 |
end |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
14 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
15 |
structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
16 |
struct |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
17 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
18 |
(* syntactic operations *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
19 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
20 |
fun mk_inf (t1, t2) = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
21 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
22 |
val T = fastype_of t1 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
23 |
in |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
24 |
Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
25 |
end |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
26 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
27 |
fun mk_image t1 t2 = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
28 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
29 |
val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
30 |
in |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
31 |
Const (@{const_name image}, |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
32 |
T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2 |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
33 |
end; |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
34 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
35 |
fun mk_sigma (t1, t2) = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
36 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
37 |
val T1 = fastype_of t1 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
38 |
val T2 = fastype_of t2 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
39 |
val setT = HOLogic.dest_setT T1 |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
40 |
val resT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2)) |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
41 |
in |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
42 |
Const (@{const_name Sigma}, |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
43 |
T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2 |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
44 |
end; |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
45 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
46 |
fun dest_Bound (Bound x) = x |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
47 |
| dest_Bound t = raise TERM("dest_Bound", [t]); |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
48 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
49 |
fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
50 |
| dest_Collect t = raise TERM ("dest_Collect", [t]) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
51 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
52 |
(* Copied from predicate_compile_aux.ML *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
53 |
fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
54 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
55 |
val (xTs, t') = strip_ex t |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
56 |
in |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
57 |
((x, T) :: xTs, t') |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
58 |
end |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
59 |
| strip_ex t = ([], t) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
60 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
61 |
fun list_tupled_abs [] f = f |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
62 |
| list_tupled_abs [(n, T)] f = (Abs (n, T, f)) |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
63 |
| list_tupled_abs ((n, T)::v::vs) f = |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
64 |
HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f)) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
65 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
66 |
fun mk_pointfree_expr t = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
67 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
68 |
val (vs, t'') = strip_ex (dest_Collect t) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
69 |
val (eq::conjs) = HOLogic.dest_conj t'' |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
70 |
val f = if fst (HOLogic.dest_eq eq) = Bound (length vs) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
71 |
then snd (HOLogic.dest_eq eq) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
72 |
else raise TERM("mk_pointfree_expr", [t]); |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
73 |
val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
74 |
val grouped_mems = AList.group (op =) mems |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
75 |
fun mk_grouped_unions (i, T) = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
76 |
case AList.lookup (op =) grouped_mems i of |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
77 |
SOME ts => foldr1 mk_inf ts |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
78 |
| NONE => HOLogic.mk_UNIV T |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
79 |
val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
80 |
in |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
81 |
mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
82 |
end; |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
83 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
84 |
val rewrite_term = try mk_pointfree_expr |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
85 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
86 |
(* proof tactic *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
87 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
88 |
(* Tactic works for arbitrary number of m : S conjuncts *) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
89 |
|
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
90 |
val dest_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
91 |
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE conjE})) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
92 |
THEN' hyp_subst_tac; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
93 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
94 |
val intro_image_Sigma_tac = rtac @{thm image_eqI} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
95 |
THEN' (REPEAT_DETERM1 o |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
96 |
(rtac @{thm refl} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
97 |
ORELSE' rtac |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
98 |
@{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]})); |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
99 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
100 |
val dest_image_Sigma_tac = etac @{thm imageE} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
101 |
THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm}) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
102 |
THEN' hyp_subst_tac |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
103 |
THEN' (TRY o REPEAT_DETERM1 o |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
104 |
(etac @{thm conjE} ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]})); |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
105 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
106 |
val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
107 |
THEN' REPEAT_DETERM1 o resolve_tac @{thms exI} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
108 |
THEN' (TRY o (rtac @{thm conjI})) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
109 |
THEN' (TRY o hyp_subst_tac) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
110 |
THEN' rtac @{thm refl}; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
111 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
112 |
val tac = |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
113 |
let |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
114 |
val subset_tac1 = rtac @{thm subsetI} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
115 |
THEN' dest_Collect_tac |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
116 |
THEN' intro_image_Sigma_tac |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
117 |
THEN' (REPEAT_DETERM1 o |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
118 |
(rtac @{thm SigmaI} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
119 |
ORELSE' rtac @{thm UNIV_I} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
120 |
ORELSE' rtac @{thm IntI} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
121 |
ORELSE' atac)); |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
122 |
|
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
123 |
val subset_tac2 = rtac @{thm subsetI} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
124 |
THEN' dest_image_Sigma_tac |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
125 |
THEN' intro_Collect_tac |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
126 |
THEN' REPEAT_DETERM o |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
127 |
(rtac @{thm conjI} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
128 |
ORELSE' eresolve_tac @{thms IntD1 IntD2} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
129 |
ORELSE' atac); |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
130 |
in |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
131 |
rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2 |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
132 |
end; |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
133 |
|
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
134 |
fun conv ctxt t = |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
135 |
let |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
136 |
fun mk_thm t' = Goal.prove ctxt [] [] |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
137 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) (K (tac 1)); |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
138 |
in |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
139 |
Option.map mk_thm (rewrite_term t) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
140 |
end; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
141 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
142 |
(* simproc *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
143 |
|
48124 | 144 |
fun simproc ss redex = |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
145 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
146 |
val ctxt = Simplifier.the_context ss |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
147 |
val _ $ set_compr = term_of redex |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
148 |
in |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
149 |
conv ctxt set_compr |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
150 |
|> Option.map (fn thm => |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
151 |
thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection}) |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
152 |
end; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
153 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
154 |
end; |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
155 |