author | bulwahn |
Thu, 08 Nov 2012 11:59:49 +0100 | |
changeset 50028 | d05f859558a0 |
parent 50026 | d9871e5ea0e1 |
child 50029 | 31c9294eebe6 |
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 |
|
49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
61 |
fun mk_vimage f s = |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
62 |
let |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
63 |
val T as Type (@{type_name fun}, [T1, T2]) = fastype_of f |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
64 |
in |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
65 |
Const (@{const_name vimage}, T --> HOLogic.mk_setT T2 --> HOLogic.mk_setT T1) $ f $ s |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
66 |
end; |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
67 |
|
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset
|
68 |
fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (x, T, t)) = ((x, T), t) |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
69 |
| 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
|
70 |
|
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
71 |
(* Copied from predicate_compile_aux.ML *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
72 |
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
|
73 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
74 |
val (xTs, t') = strip_ex t |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
75 |
in |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
76 |
((x, T) :: xTs, t') |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
77 |
end |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
78 |
| strip_ex t = ([], t) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
79 |
|
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
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
|
49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
87 |
fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
88 |
| mk_split_abs vs (Const ("Product_Type.Pair", _) $ u $ v) t = |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
89 |
HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t)) |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
90 |
| mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]); |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
91 |
|
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
92 |
(* a variant of HOLogic.strip_psplits *) |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
93 |
val strip_psplits = |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
94 |
let |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
95 |
fun strip [] qs vs t = (t, rev vs, qs) |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
96 |
| strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) = |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
97 |
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
98 |
| strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t |
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
99 |
| strip (_ :: ps) qs vs t = strip ps qs |
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
100 |
((Name.uu_, hd (binder_types (fastype_of1 (map snd vs, t)))) :: vs) |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
101 |
(incr_boundvars 1 t $ Bound 0) |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
102 |
in strip [[]] [] [] end; |
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
|
103 |
|
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 |
(* 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
|
105 |
|
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
106 |
datatype pattern = Pattern of int list |
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
|
107 |
|
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
108 |
fun dest_Pattern (Pattern bs) = bs |
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
|
109 |
|
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
110 |
fun dest_bound (Bound i) = i |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
111 |
| dest_bound t = raise TERM("dest_bound", [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
|
112 |
|
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
113 |
fun mk_pattern t = case try ((map dest_bound) o HOLogic.strip_tuple) t of |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
114 |
SOME p => Pattern p |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
115 |
| NONE => raise TERM ("mk_pattern: only tuples of bound variables supported", [t]); |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
116 |
|
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
117 |
fun type_of_pattern Ts (Pattern bs) = HOLogic.mk_tupleT (map (nth Ts) bs) |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
118 |
|
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
119 |
fun term_of_pattern Ts (Pattern bs) = |
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
|
120 |
let |
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
121 |
fun mk [b] = Bound b |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
122 |
| mk (b :: bs) = HOLogic.pair_const (nth Ts b) (type_of_pattern Ts (Pattern bs)) |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
123 |
$ Bound b $ mk bs |
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
124 |
in mk bs end; |
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
|
125 |
|
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 |
(* 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
|
127 |
|
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 |
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
|
129 |
|
49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
130 |
fun map_atom f (Atom a) = Atom (f a) |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
131 |
| map_atom _ x = x |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
132 |
|
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
133 |
fun is_collect_atom (Atom (_, Const(@{const_name Collect}, _) $ _)) = true |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
134 |
| is_collect_atom (Atom (_, Const (@{const_name "Groups.uminus_class.uminus"}, _) $ (Const(@{const_name Collect}, _) $ _))) = true |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
135 |
| is_collect_atom _ = false |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
136 |
|
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
137 |
fun mk_split _ [(x, T)] t = (T, Abs (x, T, t)) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
138 |
| mk_split rT ((x, T) :: vs) t = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
139 |
let |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
140 |
val (T', t') = mk_split rT vs t |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
141 |
val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t')) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
142 |
in (domain_type (fastype_of t''), t'') end |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
143 |
|
49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
144 |
fun mk_atom vs (Const (@{const_name "Set.member"}, _) $ x $ s) = |
49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
145 |
if not (null (loose_bnos s)) then |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
146 |
raise TERM ("mk_atom: bound variables in the set expression", [s]) |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
147 |
else |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
148 |
(case try mk_pattern x of |
49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
149 |
SOME pat => (pat, Atom (pat, s)) |
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
150 |
| NONE => |
49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
151 |
let |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
152 |
val bs = loose_bnos x |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
153 |
val vs' = map (nth (rev vs)) bs |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
154 |
val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
155 |
|> sort (fn (p1, p2) => int_ord (fst p1, fst p2)) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
156 |
|> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst'))))) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
157 |
val x' = subst_bounds (subst, x) |
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
158 |
val tuple = Pattern bs |
49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
159 |
val rT = HOLogic.dest_setT (fastype_of s) |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
160 |
val (_, f) = mk_split rT vs' x' |
49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
161 |
in (tuple, Atom (tuple, mk_vimage f s)) end) |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
162 |
| mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = |
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset
|
163 |
apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t) |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
164 |
| mk_atom vs t = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
165 |
let |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
166 |
val bs = loose_bnos t |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
167 |
val vs' = map (nth (rev vs)) bs |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
168 |
val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
169 |
|> sort (fn (p1, p2) => int_ord (fst p1, fst p2)) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
170 |
|> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst'))))) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
171 |
val t' = subst_bounds (subst, t) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
172 |
val tuple = Pattern bs |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
173 |
val setT = HOLogic.mk_tupleT (map snd vs') |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
174 |
val (_, s) = mk_split @{typ bool} vs' t' |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
175 |
in |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
176 |
(tuple, Atom (tuple, HOLogic.Collect_const setT $ s)) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
177 |
end |
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
|
178 |
|
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
179 |
fun merge' [] (pats1, pats2) = ([], (pats1, pats2)) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
180 |
| merge' pat (pats, []) = (pat, (pats, [])) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
181 |
| merge' pat (pats1, pats) = |
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
|
182 |
let |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
183 |
fun disjoint_to_pat p = null (inter (op =) pat p) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
184 |
val overlap_pats = filter_out disjoint_to_pat pats |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
185 |
val rem_pats = filter disjoint_to_pat pats |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
186 |
val (pat, (pats', pats1')) = merge' (distinct (op =) (flat overlap_pats @ pat)) (rem_pats, pats1) |
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
|
187 |
in |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
188 |
(pat, (pats1', pats')) |
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
|
189 |
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
|
190 |
|
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
191 |
fun merge ([], pats) = pats |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
192 |
| merge (pat :: pats', pats) = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
193 |
let val (pat', (pats1', pats2')) = merge' pat (pats', pats) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
194 |
in pat' :: merge (pats1', pats2') end; |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
195 |
|
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
196 |
fun restricted_merge ([], pats) = pats |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
197 |
| restricted_merge (pat :: pats', pats) = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
198 |
let |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
199 |
fun disjoint_to_pat p = null (inter (op =) pat p) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
200 |
val overlap_pats = filter_out disjoint_to_pat pats |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
201 |
val rem_pats = filter disjoint_to_pat pats |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
202 |
in |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
203 |
case overlap_pats of |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
204 |
[] => pat :: restricted_merge (pats', rem_pats) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
205 |
| [pat'] => if subset (op =) (pat, pat') then |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
206 |
pat' :: restricted_merge (pats', rem_pats) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
207 |
else if subset (op =) (pat', pat) then |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
208 |
pat :: restricted_merge (pats', rem_pats) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
209 |
else error "restricted merge: two patterns require relational join" |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
210 |
| _ => error "restricted merge: multiple patterns overlap" |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
211 |
end; |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
212 |
|
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
213 |
fun map_atoms f (Atom a) = Atom (f a) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
214 |
| map_atoms f (Un (fm1, fm2)) = Un (pairself (map_atoms f) (fm1, fm2)) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
215 |
| map_atoms f (Int (fm1, fm2)) = Int (pairself (map_atoms f) (fm1, fm2)) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
216 |
|
50028
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
217 |
fun extend Ts bs t = foldr1 mk_sigma (t :: map (fn b => HOLogic.mk_UNIV (nth Ts b)) bs) |
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
|
218 |
|
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
219 |
fun rearrange vs (pat, pat') t = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
220 |
let |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
221 |
val subst = map_index (fn (i, b) => (b, i)) (rev pat) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
222 |
val vs' = map (nth (rev vs)) pat |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
223 |
val Ts' = map snd (rev vs') |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
224 |
val bs = map (fn b => the (AList.lookup (op =) subst b)) pat' |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
225 |
val rt = term_of_pattern Ts' (Pattern bs) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
226 |
val rT = type_of_pattern Ts' (Pattern bs) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
227 |
val (_, f) = mk_split rT vs' rt |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
228 |
in |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
229 |
mk_image f t |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
230 |
end; |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
231 |
|
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
232 |
fun adjust vs pats (Pattern pat, t) = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
233 |
let |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
234 |
val SOME p = find_first (fn p => not (null (inter (op =) pat p))) pats |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
235 |
val missing = subtract (op =) pat p |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
236 |
val Ts = rev (map snd vs) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
237 |
val t' = extend Ts missing t |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
238 |
in (Pattern p, rearrange vs (pat @ missing, p) t') end |
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
|
239 |
|
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
240 |
fun adjust_atoms vs pats fm = map_atoms (adjust vs pats) fm |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
241 |
|
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
242 |
fun merge_inter vs (pats1, fm1) (pats2, fm2) = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
243 |
let |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
244 |
val pats = restricted_merge (map dest_Pattern pats1, map dest_Pattern pats2) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
245 |
val (fm1', fm2') = pairself (adjust_atoms vs pats) (fm1, fm2) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
246 |
in |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
247 |
(map Pattern pats, Int (fm1', fm2')) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
248 |
end; |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
249 |
|
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
250 |
fun merge_union vs (pats1, fm1) (pats2, fm2) = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
251 |
let |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
252 |
val pats = merge (map dest_Pattern pats1, map dest_Pattern pats2) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
253 |
val (fm1', fm2') = pairself (adjust_atoms vs pats) (fm1, fm2) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
254 |
in |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
255 |
(map Pattern pats, Un (fm1', fm2')) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
256 |
end; |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
257 |
|
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
258 |
fun mk_formula vs (@{const HOL.conj} $ t1 $ t2) = merge_inter vs (mk_formula vs t1) (mk_formula vs t2) |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
259 |
| mk_formula vs (@{const HOL.disj} $ t1 $ t2) = merge_union vs (mk_formula vs t1) (mk_formula vs t2) |
49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset
|
260 |
| mk_formula vs t = apfst single (mk_atom vs 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
|
261 |
|
49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset
|
262 |
fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2) |
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset
|
263 |
| strip_Int fm = [fm] |
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 |
(* 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
|
266 |
|
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
|
267 |
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
|
268 |
let |
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset
|
269 |
val bounds = maps dest_Pattern pats |
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
|
270 |
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
|
271 |
|> 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
|
272 |
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
|
273 |
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
|
274 |
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
|
275 |
|
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
276 |
fun is_reordering t = |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
277 |
let val (t', _, _) = HOLogic.strip_psplits t |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
278 |
in forall (fn Bound _ => true) (HOLogic.strip_tuple t') end |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
279 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
280 |
fun mk_pointfree_expr t = |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
281 |
let |
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset
|
282 |
val ((x, T), (vs, t'')) = apsnd 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
|
283 |
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
|
284 |
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
|
285 |
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
|
286 |
val conjs = HOLogic.dest_conj t'' |
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset
|
287 |
val refl = HOLogic.eq_const T $ Bound (length vs) $ Bound (length vs) |
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
|
288 |
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
|
289 |
the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs))) |
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset
|
290 |
val eq = the_default refl (find_first is_the_eq conjs) |
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
|
291 |
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
|
292 |
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
|
293 |
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
|
294 |
(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
|
295 |
val (pats, fm) = |
49943
6a26fed71755
passing names and types of all bounds around in the simproc
bulwahn
parents:
49942
diff
changeset
|
296 |
mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds)) |
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
|
297 |
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
|
298 |
| 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
|
299 |
| 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
|
300 |
val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats) |
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset
|
301 |
val t = mk_split_abs (rev ((x, T) :: vs)) pat (reorder_bounds pats f) |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
302 |
in |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
303 |
if the_default false (try is_reordering t) andalso is_collect_atom fm then |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
304 |
error "mk_pointfree_expr: trivial case" |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
305 |
else (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
|
306 |
end; |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
307 |
|
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
308 |
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
|
309 |
|
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
|
310 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
311 |
(* proof tactic *) |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
312 |
|
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
|
313 |
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
|
314 |
|
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
|
315 |
(* 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
|
316 |
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
|
317 |
(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
|
318 |
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
|
319 |
| _ => 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
|
320 |
|
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
|
321 |
(* 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
|
322 |
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
|
323 |
(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
|
324 |
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
|
325 |
| _ => 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
|
326 |
|
49944
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset
|
327 |
val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp} |
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset
|
328 |
val vimageE' = |
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset
|
329 |
@{lemma "a \<notin> f -` B ==> (\<And> x. f a = x ==> x \<notin> B ==> P) ==> P" by simp} |
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset
|
330 |
|
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
331 |
val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto} |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
332 |
val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto} |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
333 |
|
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
|
334 |
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
|
335 |
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE})) |
49946 | 336 |
THEN' REPEAT_DETERM o etac @{thm conjE} |
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset
|
337 |
THEN' TRY o hyp_subst_tac; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
338 |
|
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
|
339 |
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
|
340 |
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
|
341 |
(rtac @{thm refl} |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
342 |
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
|
343 |
@{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
|
344 |
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
|
345 |
(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
|
346 |
|
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
|
347 |
val elim_image_tac = etac @{thm imageE} |
50028
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
348 |
THEN' REPEAT_DETERM o CHANGED o |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
349 |
(TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps @{thms split_paired_all prod.cases}) |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
350 |
THEN' REPEAT_DETERM o etac @{thm Pair_inject} |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
351 |
THEN' TRY o hyp_subst_tac) |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
352 |
|
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
|
353 |
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
|
354 |
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
|
355 |
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
|
356 |
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
|
357 |
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
|
358 |
| 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
|
359 |
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
|
360 |
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
|
361 |
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
|
362 |
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
|
363 |
| tac1_of_formula (Atom _) = |
50028
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
364 |
REPEAT_DETERM1 o (atac |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
365 |
ORELSE' rtac @{thm SigmaI} |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
366 |
ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN' TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])) |
49944
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset
|
367 |
ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN' |
49875
0adcb5cd4eba
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49874
diff
changeset
|
368 |
TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])) |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
369 |
ORELSE' (rtac @{thm image_eqI} THEN' |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
370 |
(REPEAT_DETERM o |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
371 |
(rtac @{thm refl} |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
372 |
ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.cases, THEN iffD2]}))) |
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
|
373 |
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
|
374 |
ORELSE' rtac @{thm iffD2[OF Compl_iff]} |
49875
0adcb5cd4eba
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49874
diff
changeset
|
375 |
ORELSE' atac) |
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
|
376 |
|
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
|
377 |
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
|
378 |
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
|
379 |
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
|
380 |
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
|
381 |
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
|
382 |
| 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
|
383 |
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
|
384 |
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
|
385 |
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
|
386 |
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
|
387 |
| tac2_of_formula (Atom _) = |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
388 |
REPEAT_DETERM o |
50028
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
389 |
(atac |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
390 |
ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]} |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
391 |
ORELSE' etac @{thm conjE} |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
392 |
ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN' |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
393 |
TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}]) THEN' |
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
394 |
REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl}) |
50028
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
395 |
ORELSE' (etac @{thm imageE} |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
396 |
THEN' (REPEAT_DETERM o CHANGED o |
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
397 |
(TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps @{thms split_paired_all prod.cases}) |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
398 |
THEN' REPEAT_DETERM o etac @{thm Pair_inject} |
50028
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
399 |
THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl}))) |
49944
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset
|
400 |
ORELSE' etac @{thm ComplE} |
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset
|
401 |
ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE') |
49875
0adcb5cd4eba
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49874
diff
changeset
|
402 |
THEN' TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}]) |
50028
d05f859558a0
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones
bulwahn
parents:
50026
diff
changeset
|
403 |
THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl})) |
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
|
404 |
|
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
|
405 |
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
|
406 |
let |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
407 |
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
|
408 |
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
|
409 |
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
|
410 |
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
|
411 |
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
|
412 |
THEN' elim_image_tac |
49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset
|
413 |
THEN' rtac @{thm iffD2[OF mem_Collect_eq]} |
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset
|
414 |
THEN' REPEAT_DETERM o resolve_tac @{thms exI} |
49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset
|
415 |
THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI})) |
50025
19965e6a705e
handling arbitrary terms in the set comprehension and more general merging of patterns possible in the set_comprehension_pointfree simproc
bulwahn
parents:
50024
diff
changeset
|
416 |
THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl})))) |
49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset
|
417 |
THEN' (fn i => EVERY (rev (map_index (fn (j, f) => |
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset
|
418 |
REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula f (i + j)) (strip_Int fm)))) |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
419 |
in |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
420 |
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
|
421 |
end; |
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
422 |
|
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
|
423 |
|
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
424 |
(* preprocessing conversion: |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
425 |
rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} *) |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
426 |
|
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
427 |
fun comprehension_conv ss ct = |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
428 |
let |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
429 |
val ctxt = Simplifier.the_context ss |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
430 |
fun dest_Collect (Const (@{const_name Collect}, T) $ t) = (HOLogic.dest_setT (body_type T), t) |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
431 |
| dest_Collect t = raise TERM ("dest_Collect", [t]) |
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
432 |
fun list_ex vs t = fold_rev (fn (x, T) => fn t => HOLogic.exists_const T $ Abs (x, T, t)) vs t |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
433 |
fun mk_term t = |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
434 |
let |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
435 |
val (T, t') = dest_Collect t |
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
436 |
val (t'', vs, fp) = case strip_psplits t' of |
49898
dd2ae15ac74f
refined conversion to only react on proper set comprehensions; tuned
bulwahn
parents:
49896
diff
changeset
|
437 |
(_, [_], _) => raise TERM("mk_term", [t']) |
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
438 |
| (t'', vs, fp) => (t'', vs, fp) |
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
439 |
val Ts = map snd vs |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
440 |
val eq = HOLogic.eq_const T $ Bound (length Ts) $ |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
441 |
(HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts))) |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
442 |
in |
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset
|
443 |
HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t''))) |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
444 |
end; |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
445 |
val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases} |
49958 | 446 |
fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th)) |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
447 |
fun tac ctxt = |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
448 |
rtac @{thm set_eqI} |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
449 |
THEN' Simplifier.simp_tac |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
450 |
(Simplifier.inherit_context ss (HOL_basic_ss addsimps unfold_thms)) |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
451 |
THEN' rtac @{thm iffI} |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
452 |
THEN' REPEAT_DETERM o rtac @{thm exI} |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
453 |
THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
454 |
THEN' REPEAT_DETERM o etac @{thm exE} |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
455 |
THEN' etac @{thm conjE} |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
456 |
THEN' REPEAT_DETERM o etac @{thm Pair_inject} |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
457 |
THEN' Subgoal.FOCUS (fn {prems, ...} => |
49958 | 458 |
Simplifier.simp_tac |
459 |
(Simplifier.inherit_context ss (HOL_basic_ss addsimps (filter is_eq prems))) 1) ctxt |
|
49959
0058298658d9
another refinement in the comprehension conversion
bulwahn
parents:
49958
diff
changeset
|
460 |
THEN' TRY o atac |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
461 |
in |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
462 |
case try mk_term (term_of ct) of |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
463 |
NONE => Thm.reflexive ct |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
464 |
| SOME t' => |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
465 |
Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (term_of ct, t'))) |
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
466 |
(fn {context, ...} => tac context 1) |
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
467 |
RS @{thm eq_reflection} |
49896
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
468 |
end |
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
469 |
|
a39deedd5c3f
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc
bulwahn
parents:
49875
diff
changeset
|
470 |
|
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
|
471 |
(* 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
|
472 |
|
49942
50e457bbc5fe
locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree
bulwahn
parents:
49901
diff
changeset
|
473 |
val prep_thms = |
50e457bbc5fe
locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree
bulwahn
parents:
49901
diff
changeset
|
474 |
map mk_meta_eq ([@{thm Bex_def}, @{thm Pow_iff[symmetric]}] @ @{thms ex_simps[symmetric]}) |
49873
4b7c2e4991fc
extending preprocessing of simproc to rewrite subset inequality into membership of powerset
bulwahn
parents:
49857
diff
changeset
|
475 |
|
49850
873fa7156468
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
bulwahn
parents:
49849
diff
changeset
|
476 |
val post_thms = |
873fa7156468
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
bulwahn
parents:
49849
diff
changeset
|
477 |
map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]}, |
873fa7156468
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
bulwahn
parents:
49849
diff
changeset
|
478 |
@{lemma "A \<times> B \<union> A \<times> C = A \<times> (B \<union> C)" by auto}, |
873fa7156468
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
bulwahn
parents:
49849
diff
changeset
|
479 |
@{lemma "(A \<times> B \<inter> C \<times> D) = (A \<inter> C) \<times> (B \<inter> D)" by auto}] |
873fa7156468
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
bulwahn
parents:
49849
diff
changeset
|
480 |
|
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
481 |
fun conv ss t = |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
482 |
let |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
483 |
val ctxt = Simplifier.the_context ss |
50026
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
484 |
val ([t'], ctxt') = Variable.import_terms true [t] (Variable.declare_term t ctxt) |
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
485 |
val ss' = Simplifier.context ctxt' ss |
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
486 |
val ct = cterm_of (Proof_Context.theory_of ctxt') t' |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
487 |
fun unfold_conv thms = |
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
488 |
Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) |
50026
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
489 |
(Raw_Simplifier.inherit_context ss' empty_ss addsimps thms) |
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
490 |
val prep_eq = (comprehension_conv ss' then_conv unfold_conv prep_thms) ct |
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
491 |
val t'' = term_of (Thm.rhs_of prep_eq) |
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
492 |
fun mk_thm (fm, t''') = Goal.prove ctxt' [] [] |
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
493 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t'', t'''))) (fn {context, ...} => tac context fm 1) |
49873
4b7c2e4991fc
extending preprocessing of simproc to rewrite subset inequality into membership of powerset
bulwahn
parents:
49857
diff
changeset
|
494 |
fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans}) |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
495 |
val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms))) |
50026
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
496 |
val export = singleton (Variable.export ctxt' ctxt) |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
497 |
in |
50026
d9871e5ea0e1
importing term with schematic type variables properly before passing it to the tactic in the set_comprehension_pointfree simproc
bulwahn
parents:
50025
diff
changeset
|
498 |
Option.map (export o post o 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
|
499 |
end; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
500 |
|
48128 | 501 |
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
|
502 |
let |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
503 |
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
|
504 |
in |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
505 |
conv ss set_compr |
48122
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
506 |
|> 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
|
507 |
end; |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
508 |
|
49763
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
509 |
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
|
510 |
let |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
511 |
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
|
512 |
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
|
513 |
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
|
514 |
in |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
515 |
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
|
516 |
end; |
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset
|
517 |
|
48124 | 518 |
fun simproc ss redex = |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
519 |
let |
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
520 |
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
|
521 |
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
|
522 |
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
|
523 |
in |
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset
|
524 |
conv ss 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
|
525 |
|> 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
|
526 |
end; |
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
527 |
|
48128 | 528 |
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
|
529 |
let |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
530 |
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
|
531 |
in |
48128 | 532 |
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
|
533 |
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
|
534 |
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
|
535 |
| NONE => NONE |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
536 |
end; |
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset
|
537 |
|
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset
|
538 |
end; |
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset
|
539 |