author | bulwahn |
Sun, 14 Oct 2012 19:16:32 +0200 | |
changeset 49849 | d9822ec4f434 |
parent 49831 | b28dbb7a45d9 |
child 49850 | 873fa7156468 |
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 |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
10 |
val base_simproc : simpset -> cterm -> thm option |
48128 | 11 |
val code_simproc : simpset -> cterm -> thm option |
48124 | 12 |
val simproc : simpset -> cterm -> 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 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
18 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
19 |
(* syntactic operations *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
20 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
21 |
fun mk_inf (t1, t2) = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
22 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
23 |
val T = fastype_of t1 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
24 |
in |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
25 |
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
|
26 |
end |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
27 |
|
49768
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
28 |
fun mk_sup (t1, t2) = |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
29 |
let |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
30 |
val T = fastype_of t1 |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
31 |
in |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
32 |
Const (@{const_name Lattices.sup_class.sup}, T --> T --> T) $ t1 $ t2 |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
33 |
end |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
34 |
|
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
35 |
fun mk_Compl t = |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
36 |
let |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
37 |
val T = fastype_of t |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
38 |
in |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
39 |
Const (@{const_name "Groups.uminus_class.uminus"}, T --> T) $ t |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
40 |
end |
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset
|
41 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
42 |
fun mk_image t1 t2 = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
43 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
44 |
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
|
45 |
in |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
end; |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
49 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
50 |
fun mk_sigma (t1, t2) = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
51 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
52 |
val T1 = fastype_of t1 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
53 |
val T2 = fastype_of t2 |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
54 |
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
|
55 |
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
|
56 |
in |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
end; |
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 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
|
62 |
| 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
|
63 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
64 |
(* Copied from predicate_compile_aux.ML *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
65 |
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
|
66 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
67 |
val (xTs, t') = strip_ex t |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
68 |
in |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
69 |
((x, T) :: xTs, t') |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
70 |
end |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
71 |
| strip_ex t = ([], t) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
72 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
73 |
fun mk_prod1 Ts (t1, t2) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
74 |
let |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
75 |
val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
76 |
in |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
77 |
HOLogic.pair_const T1 T2 $ t1 $ t2 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
78 |
end; |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
79 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
80 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
81 |
(* patterns *) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
82 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
83 |
datatype pattern = TBound of int | TPair of pattern * pattern; |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
84 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
85 |
fun mk_pattern (Bound n) = TBound n |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
86 |
| mk_pattern (Const (@{const_name "Product_Type.Pair"}, _) $ l $ r) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
87 |
TPair (mk_pattern l, mk_pattern r) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
88 |
| mk_pattern t = raise TERM ("mk_pattern: only bound variable tuples currently supported", [t]); |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
89 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
90 |
fun type_of_pattern Ts (TBound n) = nth Ts n |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
91 |
| type_of_pattern Ts (TPair (l, r)) = HOLogic.mk_prodT (type_of_pattern Ts l, type_of_pattern Ts r) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
92 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
93 |
fun term_of_pattern _ (TBound n) = Bound n |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
94 |
| term_of_pattern Ts (TPair (l, r)) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
95 |
let |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
96 |
val (lt, rt) = pairself (term_of_pattern Ts) (l, r) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
97 |
val (lT, rT) = pairself (curry fastype_of1 Ts) (lt, rt) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
98 |
in |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
99 |
HOLogic.pair_const lT rT $ lt $ rt |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
100 |
end; |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
101 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
102 |
fun bounds_of_pattern (TBound i) = [i] |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
103 |
| bounds_of_pattern (TPair (l, r)) = union (op =) (bounds_of_pattern l) (bounds_of_pattern r) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
104 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
105 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
106 |
(* formulas *) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
107 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
108 |
datatype formula = Atom of (pattern * term) | Int of formula * formula | Un of formula * formula |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
109 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
110 |
fun mk_atom (Const (@{const_name "Set.member"}, _) $ x $ s) = (mk_pattern x, Atom (mk_pattern x, s)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
111 |
| mk_atom (Const (@{const_name "HOL.Not"}, _) $ (Const (@{const_name "Set.member"}, _) $ x $ s)) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
112 |
(mk_pattern x, Atom (mk_pattern x, mk_Compl s)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
113 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
114 |
fun can_merge (pats1, pats2) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
115 |
let |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
116 |
fun check pat1 pat2 = (pat1 = pat2) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
117 |
orelse (inter (op =) (bounds_of_pattern pat1) (bounds_of_pattern pat2) = []) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
118 |
in |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
119 |
forall (fn pat1 => forall (fn pat2 => check pat1 pat2) pats2) pats1 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
120 |
end |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
121 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
122 |
fun merge_patterns (pats1, pats2) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
123 |
if can_merge (pats1, pats2) then |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
124 |
union (op =) pats1 pats2 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
125 |
else raise Fail "merge_patterns: variable groups overlap" |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
126 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
127 |
fun merge oper (pats1, sp1) (pats2, sp2) = (merge_patterns (pats1, pats2), oper (sp1, sp2)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
128 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
129 |
fun mk_formula (@{const HOL.conj} $ t1 $ t2) = merge Int (mk_formula t1) (mk_formula t2) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
130 |
| mk_formula (@{const HOL.disj} $ t1 $ t2) = merge Un (mk_formula t1) (mk_formula t2) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
131 |
| mk_formula t = apfst single (mk_atom t) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
132 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
133 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
134 |
(* term construction *) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
135 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
136 |
fun reorder_bounds pats t = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
137 |
let |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
138 |
val bounds = maps bounds_of_pattern pats |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
139 |
val bperm = bounds ~~ ((length bounds - 1) downto 0) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
140 |
|> sort (fn (i,j) => int_ord (fst i, fst j)) |> map snd |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
141 |
in |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
142 |
subst_bounds (map Bound bperm, t) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
143 |
end; |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
144 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
145 |
fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
146 |
| mk_split_abs vs (Const ("Product_Type.Pair", _) $ u $ v) t = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
147 |
HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
148 |
| mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]); |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
149 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
150 |
fun mk_pointfree_expr t = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
151 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
152 |
val (vs, t'') = strip_ex (dest_Collect t) |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
153 |
val Ts = map snd (rev vs) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
154 |
fun mk_mem_UNIV n = HOLogic.mk_mem (Bound n, HOLogic.mk_UNIV (nth Ts n)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
155 |
fun lookup (pat', t) pat = if pat = pat' then t else HOLogic.mk_UNIV (type_of_pattern Ts pat) |
49761
b7772f3b6c03
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
bulwahn
parents:
48128
diff
changeset
|
156 |
val conjs = HOLogic.dest_conj t'' |
b7772f3b6c03
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
bulwahn
parents:
48128
diff
changeset
|
157 |
val is_the_eq = |
b7772f3b6c03
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
bulwahn
parents:
48128
diff
changeset
|
158 |
the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs))) |
b7772f3b6c03
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
bulwahn
parents:
48128
diff
changeset
|
159 |
val SOME eq = find_first is_the_eq conjs |
b7772f3b6c03
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
bulwahn
parents:
48128
diff
changeset
|
160 |
val f = snd (HOLogic.dest_eq eq) |
b7772f3b6c03
set_comprehension_pointfree also handles terms where the equation is not at the first position, which is a necessary generalisation to eventually handle bounded existentials; tuned
bulwahn
parents:
48128
diff
changeset
|
161 |
val conjs' = filter_out (fn t => eq = t) conjs |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
162 |
val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs')) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
163 |
(0 upto (length vs - 1)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
164 |
val (pats, fm) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
165 |
mk_formula (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
166 |
fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
167 |
| mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
168 |
| mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
169 |
val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
170 |
val t = mk_split_abs (rev vs) pat (reorder_bounds pats f) |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
171 |
in |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
172 |
(fm, mk_image t (mk_set fm)) |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
173 |
end; |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
174 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
175 |
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
|
176 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
177 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
178 |
(* proof tactic *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
179 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
180 |
val prod_case_distrib = @{lemma "(prod_case g x) z = prod_case (% x y. (g x y) z) x" by (simp add: prod_case_beta)} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
181 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
182 |
(* FIXME: one of many clones *) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
183 |
fun Trueprop_conv cv ct = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
184 |
(case Thm.term_of ct of |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
185 |
Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
186 |
| _ => raise CTERM ("Trueprop_conv", [ct])) |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
187 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
188 |
(* FIXME: another clone *) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
189 |
fun eq_conv cv1 cv2 ct = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
190 |
(case Thm.term_of ct of |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
191 |
Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
192 |
| _ => raise CTERM ("eq_conv", [ct])) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
193 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
194 |
val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
195 |
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE})) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
196 |
THEN' TRY o etac @{thm conjE} |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
197 |
THEN' hyp_subst_tac; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
198 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
199 |
fun intro_image_tac ctxt = rtac @{thm image_eqI} |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
200 |
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
|
201 |
(rtac @{thm refl} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
202 |
ORELSE' rtac |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
203 |
@{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
204 |
ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
205 |
(Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt))) |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
206 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
207 |
val elim_image_tac = etac @{thm imageE} |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
208 |
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
|
209 |
THEN' hyp_subst_tac |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
210 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
211 |
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
|
212 |
THEN' REPEAT_DETERM1 o resolve_tac @{thms exI} |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
213 |
THEN' (TRY o (rtac @{thm conjI})) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
214 |
THEN' (TRY o hyp_subst_tac) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
215 |
THEN' rtac @{thm refl}; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
216 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
217 |
fun tac1_of_formula (Int (fm1, fm2)) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
218 |
TRY o etac @{thm conjE} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
219 |
THEN' rtac @{thm IntI} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
220 |
THEN' (fn i => tac1_of_formula fm2 (i + 1)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
221 |
THEN' tac1_of_formula fm1 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
222 |
| tac1_of_formula (Un (fm1, fm2)) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
223 |
etac @{thm disjE} THEN' rtac @{thm UnI1} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
224 |
THEN' tac1_of_formula fm1 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
225 |
THEN' rtac @{thm UnI2} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
226 |
THEN' tac1_of_formula fm2 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
227 |
| tac1_of_formula (Atom _) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
228 |
(REPEAT_DETERM1 o (rtac @{thm SigmaI} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
229 |
ORELSE' rtac @{thm UNIV_I} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
230 |
ORELSE' rtac @{thm iffD2[OF Compl_iff]} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
231 |
ORELSE' atac)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
232 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
233 |
fun tac2_of_formula (Int (fm1, fm2)) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
234 |
TRY o etac @{thm IntE} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
235 |
THEN' TRY o rtac @{thm conjI} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
236 |
THEN' (fn i => tac2_of_formula fm2 (i + 1)) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
237 |
THEN' tac2_of_formula fm1 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
238 |
| tac2_of_formula (Un (fm1, fm2)) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
239 |
etac @{thm UnE} THEN' rtac @{thm disjI1} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
240 |
THEN' tac2_of_formula fm1 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
241 |
THEN' rtac @{thm disjI2} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
242 |
THEN' tac2_of_formula fm2 |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
243 |
| tac2_of_formula (Atom _) = |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
244 |
TRY o REPEAT_DETERM1 o |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
245 |
(dtac @{thm iffD1[OF mem_Sigma_iff]} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
246 |
ORELSE' etac @{thm conjE} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
247 |
ORELSE' etac @{thm ComplE} |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
248 |
ORELSE' atac) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
249 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
250 |
fun tac ctxt fm = |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
251 |
let |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
252 |
val subset_tac1 = rtac @{thm subsetI} |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
253 |
THEN' elim_Collect_tac |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
254 |
THEN' (intro_image_tac ctxt) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
255 |
THEN' (tac1_of_formula fm) |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
256 |
val subset_tac2 = rtac @{thm subsetI} |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
257 |
THEN' elim_image_tac |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
258 |
THEN' intro_Collect_tac |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
259 |
THEN' tac2_of_formula fm |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
260 |
in |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
261 |
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
|
262 |
end; |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
263 |
|
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
264 |
|
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
265 |
(* main simprocs *) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
266 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
267 |
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
|
268 |
let |
49765
b9eb9c2b87c7
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
bulwahn
parents:
49763
diff
changeset
|
269 |
val ct = cterm_of (Proof_Context.theory_of ctxt) t |
b9eb9c2b87c7
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
bulwahn
parents:
49763
diff
changeset
|
270 |
val Bex_def = mk_meta_eq @{thm Bex_def} |
b9eb9c2b87c7
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
bulwahn
parents:
49763
diff
changeset
|
271 |
val unfold_eq = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv Bex_def))) ctxt ct |
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
272 |
val t' = term_of (Thm.rhs_of unfold_eq) |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
273 |
fun mk_thm (fm, t'') = Goal.prove ctxt [] [] |
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset
|
274 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1) |
49765
b9eb9c2b87c7
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
bulwahn
parents:
49763
diff
changeset
|
275 |
fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans}) |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
276 |
in |
49765
b9eb9c2b87c7
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
bulwahn
parents:
49763
diff
changeset
|
277 |
Option.map (unfold o mk_thm) (rewrite_term t') |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
278 |
end; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
279 |
|
48128 | 280 |
fun base_simproc ss redex = |
48122
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
281 |
let |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
282 |
val ctxt = Simplifier.the_context ss |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
283 |
val set_compr = term_of redex |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
284 |
in |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
285 |
conv ctxt set_compr |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
286 |
|> Option.map (fn thm => thm RS @{thm eq_reflection}) |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
287 |
end; |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
288 |
|
49763
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
289 |
fun instantiate_arg_cong ctxt pred = |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
290 |
let |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
291 |
val certify = cterm_of (Proof_Context.theory_of ctxt) |
49831
b28dbb7a45d9
increading indexes to avoid clashes in the set_comprehension_pointfree simproc
bulwahn
parents:
49768
diff
changeset
|
292 |
val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong} |
49763
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
293 |
val f $ _ = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of arg_cong))) |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
294 |
in |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
295 |
cterm_instantiate [(certify f, certify pred)] arg_cong |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
296 |
end; |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
297 |
|
48124 | 298 |
fun simproc ss redex = |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
299 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
300 |
val ctxt = Simplifier.the_context ss |
49763
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
301 |
val pred $ set_compr = term_of redex |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
302 |
val arg_cong' = instantiate_arg_cong ctxt pred |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
303 |
in |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
304 |
conv ctxt set_compr |
49763
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
305 |
|> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection}) |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
306 |
end; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
307 |
|
48128 | 308 |
fun code_simproc ss redex = |
48122
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
309 |
let |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
310 |
val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
311 |
in |
48128 | 312 |
case base_simproc ss (Thm.rhs_of prep_thm) of |
48122
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
313 |
SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm], |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
314 |
Raw_Simplifier.rewrite false @{thms eq_equal} (Thm.rhs_of rewr_thm)]) |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
315 |
| NONE => NONE |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
316 |
end; |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
317 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
318 |
end; |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
319 |