1 (* Title: HOL/ex/set_comprehension_pointfree.ML |
|
2 Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen |
|
3 |
|
4 Simproc for rewriting set comprehensions to pointfree expressions. |
|
5 *) |
|
6 |
|
7 signature SET_COMPREHENSION_POINTFREE = |
|
8 sig |
|
9 val simproc : morphism -> simpset -> cterm -> thm option |
|
10 end |
|
11 |
|
12 structure Set_Comprehension_Pointfree : SET_COMPREHENSION_POINTFREE = |
|
13 struct |
|
14 |
|
15 (* syntactic operations *) |
|
16 |
|
17 fun mk_inf (t1, t2) = |
|
18 let |
|
19 val T = fastype_of t1 |
|
20 in |
|
21 Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2 |
|
22 end |
|
23 |
|
24 fun mk_image t1 t2 = |
|
25 let |
|
26 val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1 |
|
27 in |
|
28 Const (@{const_name image}, T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2 |
|
29 end; |
|
30 |
|
31 fun mk_sigma (t1, t2) = |
|
32 let |
|
33 val T1 = fastype_of t1 |
|
34 val T2 = fastype_of t2 |
|
35 val setT = HOLogic.dest_setT T1 |
|
36 val resultT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2)) |
|
37 in |
|
38 Const (@{const_name Sigma}, T1 --> (setT --> T2) --> resultT) $ t1 $ absdummy setT t2 |
|
39 end; |
|
40 |
|
41 fun dest_Bound (Bound x) = x |
|
42 | dest_Bound t = raise TERM("dest_Bound", [t]); |
|
43 |
|
44 fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (_, _, t)) = t |
|
45 | dest_Collect t = raise TERM ("dest_Collect", [t]) |
|
46 |
|
47 (* Copied from predicate_compile_aux.ML *) |
|
48 fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = |
|
49 let |
|
50 val (xTs, t') = strip_ex t |
|
51 in |
|
52 ((x, T) :: xTs, t') |
|
53 end |
|
54 | strip_ex t = ([], t) |
|
55 |
|
56 fun list_tupled_abs [] f = f |
|
57 | list_tupled_abs [(n, T)] f = (Abs (n, T, f)) |
|
58 | list_tupled_abs ((n, T)::v::vs) f = HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f)) |
|
59 |
|
60 fun mk_pointfree_expr t = |
|
61 let |
|
62 val (vs, t'') = strip_ex (dest_Collect t) |
|
63 val (eq::conjs) = HOLogic.dest_conj t'' |
|
64 val f = if fst (HOLogic.dest_eq eq) = Bound (length vs) |
|
65 then snd (HOLogic.dest_eq eq) |
|
66 else raise TERM("mk_pointfree_expr", [t]); |
|
67 val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs |
|
68 val grouped_mems = AList.group (op =) mems |
|
69 fun mk_grouped_unions (i, T) = |
|
70 case AList.lookup (op =) grouped_mems i of |
|
71 SOME ts => foldr1 mk_inf ts |
|
72 | NONE => HOLogic.mk_UNIV T |
|
73 val complete_sets = map mk_grouped_unions ((length vs - 1) downto 0 ~~ map snd vs) |
|
74 in |
|
75 mk_image (list_tupled_abs vs f) (foldr1 mk_sigma complete_sets) |
|
76 end; |
|
77 |
|
78 (* proof tactic *) |
|
79 |
|
80 (* This tactic is terribly incomplete *) |
|
81 |
|
82 val goal1_tac_part2 = REPEAT_ALL_NEW (CHANGED o (atac ORELSE' rtac @{thm SigmaI})) |
|
83 |
|
84 val goal1_tac = etac @{thm CollectE} |
|
85 THEN' REPEAT1 o CHANGED o etac @{thm exE} |
|
86 THEN' REPEAT1 o CHANGED o etac @{thm conjE} |
|
87 THEN' rtac @{thm image_eqI} |
|
88 THEN' RANGE [(REPEAT o CHANGED o stac @{thm split}) THEN' goal1_tac_part2, goal1_tac_part2] |
|
89 |
|
90 val goal2_tac = etac @{thm imageE} |
|
91 THEN' rtac @{thm CollectI} |
|
92 THEN' REPEAT o CHANGED o etac @{thm SigmaE} |
|
93 THEN' REPEAT o CHANGED o rtac @{thm exI} |
|
94 THEN' REPEAT_ALL_NEW (rtac @{thm conjI}) |
|
95 THEN_ALL_NEW |
|
96 (atac ORELSE' |
|
97 (asm_full_simp_tac HOL_basic_ss THEN' stac @{thm split} THEN' rtac @{thm refl})) |
|
98 |
|
99 val tac = |
|
100 rtac @{thm set_eqI} 1 |
|
101 THEN rtac @{thm iffI} 1 |
|
102 THEN goal1_tac 1 |
|
103 THEN goal2_tac 1 |
|
104 |
|
105 (* simproc *) |
|
106 |
|
107 fun simproc _ ss redex = |
|
108 let |
|
109 val ctxt = Simplifier.the_context ss |
|
110 val _ $ set_compr = term_of redex |
|
111 in |
|
112 case try mk_pointfree_expr set_compr of |
|
113 NONE => NONE |
|
114 | SOME pointfree_expr => |
|
115 SOME (Goal.prove ctxt [] [] |
|
116 (HOLogic.mk_Trueprop (HOLogic.mk_eq (set_compr, pointfree_expr))) (K tac) |
|
117 RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection}) |
|
118 end |
|
119 |
|
120 end; |
|