author  bulwahn 
Thu, 08 Nov 2012 17:06:59 +0100  
changeset 50031  d12b3a270a62 
parent 50030  349f651ec203 
child 50032  a439a9d14ba3 
permissions  rwrr 
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 

d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

18 
(* syntactic operations *) 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

19 

d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

20 
fun mk_inf (t1, t2) = 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

21 
let 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

22 
val T = fastype_of t1 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

23 
in 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

24 
Const (@{const_name Lattices.inf_class.inf}, T > T > T) $ t1 $ t2 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

25 
end 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

26 

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

27 
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

28 
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

29 
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

30 
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

31 
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

32 
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

33 

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 
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

35 
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

36 
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

37 
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

38 
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

39 
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

40 

48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

41 
fun mk_image t1 t2 = 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

42 
let 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

43 
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

44 
in 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

45 
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

46 
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

47 
end; 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

48 

d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

49 
fun mk_sigma (t1, t2) = 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

50 
let 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

51 
val T1 = fastype_of t1 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

52 
val T2 = fastype_of t2 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

53 
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

54 
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

55 
in 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

56 
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

57 
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

58 
end; 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

59 

49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

60 
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

61 
let 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

62 
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

63 
in 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

64 
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

65 
end; 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

66 

49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset

67 
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

68 
 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

69 

d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

70 
(* Copied from predicate_compile_aux.ML *) 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

71 
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

72 
let 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

73 
val (xTs, t') = strip_ex t 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

74 
in 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

75 
((x, T) :: xTs, t') 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

76 
end 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

77 
 strip_ex t = ([], t) 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

78 

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

79 
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

80 
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

81 
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

82 
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

83 
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

84 
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

85 

49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

86 
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

87 
 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

88 
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

89 
 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

90 

49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

91 
(* 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

92 
val strip_psplits = 
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

93 
let 
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

94 
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

95 
 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

96 
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

97 
 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

98 
 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

99 
((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

100 
(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

101 
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

102 

d9822ec4f434
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 
(* 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

104 

50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

105 
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

106 

50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

107 
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

108 

50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

109 
fun dest_bound (Bound i) = i 
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

110 
 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

111 

50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

112 
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

113 

b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

114 
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

115 
let 
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

116 
fun mk [b] = Bound b 
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

117 
 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

118 
$ Bound b $ mk bs 
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

119 
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

120 

d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

121 
(* 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

122 

d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

123 
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

124 

49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

125 
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

126 
 map_atom _ x = x 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

127 

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

128 
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

129 
 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

130 
 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

131 

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

132 
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

133 
 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

134 
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

135 
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

136 
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

137 
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

138 

50030
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

139 
fun mk_term vs t = 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

140 
let 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

141 
val bs = loose_bnos t 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

142 
val vs' = map (nth (rev vs)) bs 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

143 
val subst = map_index (fn (i, j) => (j, Bound i)) (rev bs) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

144 
> sort (fn (p1, p2) => int_ord (fst p1, fst p2)) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

145 
> (fn subst' => map (fn i => the_default (Bound i) (AList.lookup (op =) subst' i)) (0 upto (fst (snd (split_last subst'))))) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

146 
val t' = subst_bounds (subst, t) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

147 
val tuple = Pattern bs 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

148 
in (tuple, (vs', t')) end 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

149 

349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

150 
fun default_atom vs t = 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

151 
let 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

152 
val (tuple, (vs', t')) = mk_term vs t 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

153 
val T = HOLogic.mk_tupleT (map snd vs') 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

154 
val s = HOLogic.Collect_const T $ (snd (mk_split @{typ bool} vs' t')) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

155 
in 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

156 
(tuple, Atom (tuple, s)) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

157 
end 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

158 

49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

159 
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

160 
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

161 
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

162 
else 
50030
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

163 
(case try ((map dest_bound) o HOLogic.strip_tuple) x of 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

164 
SOME pat => (Pattern pat, Atom (Pattern pat, s)) 
49874
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

165 
 NONE => 
49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

166 
let 
50030
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

167 
val (tuple, (vs', x')) = mk_term vs x 
49900
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

168 
val rT = HOLogic.dest_setT (fastype_of s) 
50030
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

169 
val s = mk_vimage (snd (mk_split rT vs' x')) s 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

170 
in (tuple, Atom (tuple, s)) end) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

171 
 mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t) 
349f651ec203
syntactic tuning and restructuring of set_comprehension_pointfree simproc
bulwahn
parents:
50029
diff
changeset

172 
 mk_atom vs t = default_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

173 

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

174 
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

175 
 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

176 
 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

177 
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

178 
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

179 
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

180 
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

181 
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

182 
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

183 
(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

184 
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

185 

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

186 
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

187 
 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

188 
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

189 
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

190 

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 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

192 
 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

193 
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

194 
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

195 
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

196 
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

197 
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

198 
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

199 
[] => 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

200 
 [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

201 
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

202 
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

203 
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

204 
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

205 
 _ => 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

206 
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

207 

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 
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

209 
 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

210 
 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

211 

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

212 
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

213 

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

214 
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

215 
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

216 
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

217 
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

218 
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

219 
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

220 
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

221 
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

222 
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

223 
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

224 
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

225 
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

226 

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 
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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 

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

235 
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

236 

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 
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

238 
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

239 
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

240 
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

241 
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

242 
(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

243 
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

244 

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 
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

246 
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

247 
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

248 
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

249 
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

250 
(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

251 
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

252 

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 
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

254 
 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

255 
 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

256 

49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset

257 
fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2) 
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset

258 
 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

259 

d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

260 
(* 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

261 

d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

262 
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

263 
let 
50024
b7265db3a1dc
simplified structure of patterns in set_comprehension_simproc
bulwahn
parents:
49959
diff
changeset

264 
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

265 
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

266 
> 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

267 
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

268 
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

269 
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

270 

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

271 
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

272 
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

273 
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

274 

48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

275 
fun mk_pointfree_expr t = 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

276 
let 
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset

277 
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

278 
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

279 
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

280 
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

281 
val conjs = HOLogic.dest_conj t'' 
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset

282 
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

283 
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

284 
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

285 
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

286 
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

287 
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

288 
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

289 
(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

290 
val (pats, fm) = 
49943
6a26fed71755
passing names and types of all bounds around in the simproc
bulwahn
parents:
49942
diff
changeset

291 
mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds)) 
50031  292 
fun mk_set (Atom pt) = foldr1 mk_sigma (map (lookup pt) 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

293 
 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

294 
 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

295 
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

296 
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

297 
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

298 
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

299 
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

300 
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

301 
end; 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

302 

48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

303 
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

304 

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

305 

48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

306 
(* proof tactic *) 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

307 

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

308 
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

309 

d9822ec4f434
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 
(* 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

311 
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

312 
(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

313 
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

314 
 _ => 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

315 

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

316 
(* 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

317 
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

318 
(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

319 
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

320 
 _ => 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

321 

49944
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset

322 
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

323 
val vimageE' = 
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset

324 
@{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

325 

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

326 
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

327 
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

328 

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

329 
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

330 
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE})) 
49946  331 
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

332 
THEN' TRY o hyp_subst_tac; 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
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 
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

335 
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

336 
(rtac @{thm refl} 
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

337 
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

338 
@{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

339 
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

340 
(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

341 

50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

342 
fun elim_image_tac ss = 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

343 
THEN' REPEAT_DETERM o CHANGED o 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

344 
(TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps @{thms split_paired_all 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

345 
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

346 
THEN' TRY o hyp_subst_tac) 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

347 

50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

348 
fun tac1_of_formula ss (Int (fm1, fm2)) = 
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

349 
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

350 
THEN' rtac @{thm IntI} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

351 
THEN' (fn i => tac1_of_formula ss fm2 (i + 1)) 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

352 
THEN' tac1_of_formula ss fm1 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

353 
 tac1_of_formula ss (Un (fm1, fm2)) = 
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

354 
etac @{thm disjE} THEN' rtac @{thm UnI1} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

355 
THEN' tac1_of_formula ss fm1 
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

356 
THEN' rtac @{thm UnI2} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

357 
THEN' tac1_of_formula ss fm2 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

358 
 tac1_of_formula ss (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

359 
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

360 
ORELSE' rtac @{thm SigmaI} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

361 
ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN' 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

362 
TRY o Simplifier.simp_tac (Simplifier.inherit_context ss (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

363 
ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN' 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

364 
TRY o Simplifier.simp_tac (Simplifier.inherit_context ss (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

365 
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

366 
(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

367 
(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

368 
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

369 
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

370 
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

371 
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

372 

50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

373 
fun tac2_of_formula ss (Int (fm1, fm2)) = 
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

374 
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

375 
THEN' TRY o rtac @{thm conjI} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

376 
THEN' (fn i => tac2_of_formula ss fm2 (i + 1)) 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

377 
THEN' tac2_of_formula ss fm1 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

378 
 tac2_of_formula ss (Un (fm1, fm2)) = 
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

379 
etac @{thm UnE} THEN' rtac @{thm disjI1} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

380 
THEN' tac2_of_formula ss fm1 
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

381 
THEN' rtac @{thm disjI2} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

382 
THEN' tac2_of_formula ss fm2 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

383 
 tac2_of_formula ss (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

384 
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

385 
(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

386 
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

387 
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

388 
ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN' 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

389 
TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_basic_ss addsimps [@{thm prod.cases}])) THEN' 
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

390 
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

391 
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

392 
THEN' (REPEAT_DETERM o CHANGED o 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

393 
(TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (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

394 
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

395 
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

396 
ORELSE' etac @{thm ComplE} 
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset

397 
ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE') 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

398 
THEN' TRY o Simplifier.full_simp_tac (Simplifier.inherit_context ss (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

399 
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

400 

50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

401 
fun tac ss ctxt fm = 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

402 
let 
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

403 
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

404 
THEN' elim_Collect_tac 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

405 
THEN' intro_image_tac ctxt 
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

406 
THEN' tac1_of_formula ss fm 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

407 
val subset_tac2 = rtac @{thm subsetI} 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

408 
THEN' elim_image_tac ss 
49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset

409 
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

410 
THEN' REPEAT_DETERM o resolve_tac @{thms exI} 
49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset

411 
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

412 
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

413 
THEN' (fn i => EVERY (rev (map_index (fn (j, f) => 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

414 
REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ss 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

415 
in 
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

416 
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

417 
end; 
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

418 

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

419 

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

420 
(* 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

421 
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

422 

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

423 
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

424 
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

425 
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

426 
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

427 
 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

428 
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

429 
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

430 
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

431 
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

432 
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

433 
(_, [_], _) => 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

434 
 (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

435 
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

436 
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

437 
(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

438 
in 
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

439 
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

440 
end; 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

441 
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

442 
val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases} 
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

443 
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

444 
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

445 
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

446 
(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

447 
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

448 
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

449 
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

450 
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

451 
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

452 
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

453 
THEN' Subgoal.FOCUS (fn {prems, ...} => 
49958  454 
Simplifier.simp_tac 
455 
(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

456 
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

457 
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

458 
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

459 
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

460 
 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

461 
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

462 
(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

463 
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

464 
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

465 

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

466 

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

467 
(* 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

468 

49942
50e457bbc5fe
locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree
bulwahn
parents:
49901
diff
changeset

469 
val prep_thms = 
50e457bbc5fe
locally inverting previously applied simplifications with ex_simps in set_comprehension_pointfree
bulwahn
parents:
49901
diff
changeset

470 
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

471 

49850
873fa7156468
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
bulwahn
parents:
49849
diff
changeset

472 
val post_thms = 
873fa7156468
adding postprocessing of computed pointfree expression in set_comprehension_pointfree simproc
bulwahn
parents:
49849
diff
changeset

473 
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

474 
@{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

475 
@{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

476 

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

477 
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

478 
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

479 
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

480 
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

481 
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

482 
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

483 
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

484 
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

485 
(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

486 
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

487 
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

488 
fun mk_thm (fm, t''') = Goal.prove ctxt' [] [] 
50029
31c9294eebe6
using more proper simpset in tactic of set_comprehension_pointfree simproc to avoid renamed bound variable warnings in recursive simplifier calls
bulwahn
parents:
50028
diff
changeset

489 
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t'', t'''))) (fn {context, ...} => tac ss' context fm 1) 
49873
4b7c2e4991fc
extending preprocessing of simproc to rewrite subset inequality into membership of powerset
bulwahn
parents:
49857
diff
changeset

490 
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

491 
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

492 
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

493 
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

494 
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

495 
end; 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

496 

48128  497 
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

498 
let 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

499 
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

500 
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

501 
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

502 
> 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

503 
end; 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

504 

49763
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset

505 
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

506 
let 
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset

507 
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

508 
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

509 
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

510 
in 
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset

511 
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

512 
end; 
bed063d0c526
generalizing set_comprehension_pointfree simproc to work for arbitrary predicates (and not just the finite predicate)
bulwahn
parents:
49761
diff
changeset

513 

48124  514 
fun simproc ss redex = 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

515 
let 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

516 
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

517 
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

518 
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

519 
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

520 
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

521 
> 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

522 
end; 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

523 

48128  524 
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

525 
let 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

526 
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

527 
in 
48128  528 
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

529 
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

530 
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

531 
 NONE => NONE 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

532 
end; 
f479f36ed2ff
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
bulwahn
parents:
48109
diff
changeset

533 

48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

534 
end; 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

535 