author  bulwahn 
Sun, 21 Oct 2012 08:39:41 +0200  
changeset 49959  0058298658d9 
parent 49958  46711464de50 
child 50024  b7265db3a1dc 
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 

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

18 

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

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

20 

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

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

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

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

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

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

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

27 

49768
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

28 
fun mk_sup (t1, t2) = 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

29 
let 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

30 
val T = fastype_of t1 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

31 
in 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

32 
Const (@{const_name Lattices.sup_class.sup}, T > T > T) $ t1 $ t2 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

33 
end 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

34 

3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

35 
fun mk_Compl t = 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

36 
let 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

37 
val T = fastype_of t 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

38 
in 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

39 
Const (@{const_name "Groups.uminus_class.uminus"}, T > T) $ t 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

40 
end 
3ecfba7e731d
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc
bulwahn
parents:
49765
diff
changeset

41 

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

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

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

44 
val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

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

46 
Const (@{const_name image}, 
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

47 
T > fastype_of t2 > HOLogic.mk_setT R) $ t1 $ t2 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

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

49 

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

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

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

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

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

54 
val setT = HOLogic.dest_setT T1 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

55 
val resT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2)) 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

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

57 
Const (@{const_name Sigma}, 
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

58 
T1 > (setT > T2) > resT) $ t1 $ absdummy setT t2 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

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

60 

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

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

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

63 
val T as Type (@{type_name fun}, [T1, T2]) = fastype_of f 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

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

65 
Const (@{const_name vimage}, T > HOLogic.mk_setT T2 > HOLogic.mk_setT T1) $ f $ s 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

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

67 

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

68 
fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (x, T, t)) = ((x, T), t) 
48049
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

69 
 dest_Collect t = raise TERM ("dest_Collect", [t]) 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

70 

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

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

72 
fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = 
d862b0d56c49
adding incompleted simproc to rewrite set comprehensions into pointfree expressions on sets
bulwahn
parents:
diff
changeset

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

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

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

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

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

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

79 

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

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

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

82 
val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

84 
HOLogic.pair_const T1 T2 $ t1 $ t2 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

86 

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

87 
fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

88 
 mk_split_abs vs (Const ("Product_Type.Pair", _) $ u $ v) t = 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

89 
HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t)) 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

90 
 mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]); 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

91 

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

92 
(* a variant of HOLogic.strip_psplits *) 
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

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

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

95 
fun strip [] qs vs t = (t, rev vs, qs) 
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

96 
 strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) = 
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

97 
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t 
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset

98 
 strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t 
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset

99 
 strip (_ :: ps) qs vs t = strip ps qs 
49901
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

100 
((Name.uu_, hd (binder_types (fastype_of1 (map snd vs, t)))) :: vs) 
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

101 
(incr_boundvars 1 t $ Bound 0) 
58cac1b3b535
comprehension conversion reuses suggested names for bound variables instead of invented fresh ones; tuned tactic
bulwahn
parents:
49900
diff
changeset

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

103 

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

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

105 

d9822ec4f434
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 
datatype pattern = TBound of int  TPair of pattern * pattern; 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

107 

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

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

109 
 mk_pattern (Const (@{const_name "Product_Type.Pair"}, _) $ l $ r) = 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

111 
 mk_pattern t = raise TERM ("mk_pattern: only bound variable tuples currently supported", [t]); 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

112 

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

113 
fun type_of_pattern Ts (TBound n) = nth Ts n 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

114 
 type_of_pattern Ts (TPair (l, r)) = HOLogic.mk_prodT (type_of_pattern Ts l, type_of_pattern Ts r) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

115 

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

116 
fun term_of_pattern _ (TBound n) = Bound n 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

118 
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

119 
val (lt, rt) = pairself (term_of_pattern Ts) (l, r) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

120 
val (lT, rT) = pairself (curry fastype_of1 Ts) (lt, rt) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

121 
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

122 
HOLogic.pair_const lT rT $ lt $ rt 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

123 
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

124 

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

125 
fun bounds_of_pattern (TBound i) = [i] 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

126 
 bounds_of_pattern (TPair (l, r)) = union (op =) (bounds_of_pattern l) (bounds_of_pattern r) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

127 

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

128 

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

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

130 

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

131 
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

132 

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

133 
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

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

135 

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

136 
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

137 
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

138 
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

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

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

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

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

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

144 
val bs = loose_bnos x 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

145 
val vs' = map (nth (rev vs)) bs 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

146 
val x' = subst_atomic (map_index (fn (i, j) => (Bound j, Bound i)) (rev bs)) x 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

147 
val tuple = foldr1 TPair (map TBound bs) 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

148 
val rT = HOLogic.dest_setT (fastype_of s) 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

149 
fun mk_split [(x, T)] t = (T, Abs (x, T, t)) 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

150 
 mk_split ((x, T) :: vs) t = 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

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

152 
val (T', t') = mk_split vs t 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

153 
val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t')) 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

154 
in (domain_type (fastype_of t''), t'') end 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

155 
val (_, f) = mk_split vs' x' 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

156 
in (tuple, Atom (tuple, mk_vimage f s)) end) 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

157 
 mk_atom vs (Const (@{const_name "HOL.Not"}, _) $ t) = 
89b118c0c070
checking for bound variables in the set expression; handling negation more generally
bulwahn
parents:
49898
diff
changeset

158 
apsnd (map_atom (apsnd mk_Compl)) (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

159 

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

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

161 
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

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

163 
orelse (inter (op =) (bounds_of_pattern pat1) (bounds_of_pattern pat2) = []) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

164 
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

165 
forall (fn pat1 => forall (fn pat2 => check pat1 pat2) pats2) pats1 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

166 
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

167 

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

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

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

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

171 
else raise Fail "merge_patterns: variable groups overlap" 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

172 

d9822ec4f434
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 
fun merge oper (pats1, sp1) (pats2, sp2) = (merge_patterns (pats1, pats2), oper (sp1, sp2)) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

174 

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

175 
fun mk_formula vs (@{const HOL.conj} $ t1 $ t2) = merge Int (mk_formula vs t1) (mk_formula vs t2) 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

176 
 mk_formula vs (@{const HOL.disj} $ t1 $ t2) = merge Un (mk_formula vs t1) (mk_formula vs t2) 
72b6d5fb407f
term construction of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49873
diff
changeset

177 
 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

178 

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

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

180 
 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

181 

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

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

183 

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

185 
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

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

187 
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

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

189 
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

190 
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

191 
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

192 

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

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

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

195 
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

196 
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

197 
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

198 
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

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

200 
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

201 
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

202 
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

203 
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

204 
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

205 
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

206 
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

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

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

209 
mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds)) 
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

210 
fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t'  ts => foldr1 mk_sigma ts) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

211 
 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

212 
 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

213 
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

214 
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

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

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

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

218 

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

219 
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

220 

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

221 

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

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

223 

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

224 
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

225 

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

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

227 
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

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

229 
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

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

231 

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

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

233 
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

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

235 
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

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

237 

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

238 
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

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

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

241 

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

242 
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

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

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

246 

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

247 
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

248 
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

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

250 
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

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

252 
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

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

254 

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

255 
val elim_image_tac = etac @{thm imageE} 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

256 
THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm}) 
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

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

258 

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 
fun tac1_of_formula (Int (fm1, fm2)) = 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

260 
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

261 
THEN' rtac @{thm IntI} 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

262 
THEN' (fn i => tac1_of_formula fm2 (i + 1)) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

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

265 
etac @{thm disjE} THEN' rtac @{thm UnI1} 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

267 
THEN' rtac @{thm UnI2} 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

269 
 tac1_of_formula (Atom _) = 
49875
0adcb5cd4eba
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49874
diff
changeset

270 
REPEAT_DETERM1 o (rtac @{thm SigmaI} 
49944
28cd3c9ca278
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage
bulwahn
parents:
49943
diff
changeset

271 
ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN' 
49875
0adcb5cd4eba
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49874
diff
changeset

272 
TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])) 
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

273 
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

274 
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

275 
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

276 

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

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

278 
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

279 
THEN' TRY o rtac @{thm conjI} 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

280 
THEN' (fn i => tac2_of_formula fm2 (i + 1)) 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

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

283 
etac @{thm UnE} THEN' rtac @{thm disjI1} 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

285 
THEN' rtac @{thm disjI2} 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

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

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

289 
(dtac @{thm iffD1[OF mem_Sigma_iff]} 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

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

292 
ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE') 
49875
0adcb5cd4eba
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49874
diff
changeset

293 
THEN' TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}]) 
0adcb5cd4eba
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage
bulwahn
parents:
49874
diff
changeset

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

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

296 

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

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

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

299 
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

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

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

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

303 
val subset_tac2 = rtac @{thm subsetI} 
49849
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

305 
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

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

307 
THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI})) 
49857
7bf407d77152
setcomprehension_pointfree simproc also works for set comprehension without an equation
bulwahn
parents:
49852
diff
changeset

308 
THEN' (K (TRY (SOMEGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl})))) 
49852
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset

309 
THEN' (fn i => EVERY (rev (map_index (fn (j, f) => 
caaa1956f0da
refined tactic in set_comprehension_pointfree simproc
bulwahn
parents:
49850
diff
changeset

310 
REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula f (i + j)) (strip_Int fm)))) 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

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

312 
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

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

314 

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

315 

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

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

317 
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

318 

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

319 
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

320 
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

321 
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

322 
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

323 
 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

324 
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

325 
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

326 
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

327 
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

328 
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

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

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

331 
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

332 
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

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

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

335 
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

336 
end; 
49957
6250121bfffb
passing around the simpset instead of the context; rewriting tactics to avoid the 'renamed bound variable' warnings in nested simplifier calls
bulwahn
parents:
49946
diff
changeset

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

339 
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

340 
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

341 
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

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

343 
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

344 
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

345 
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

346 
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

347 
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

348 
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

349 
THEN' Subgoal.FOCUS (fn {prems, ...} => 
49958  350 
Simplifier.simp_tac 
351 
(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

352 
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

353 
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

354 
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

355 
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

356 
 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

357 
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

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

359 
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

360 
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

361 

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

362 

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

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

364 

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

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

366 
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

367 

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

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

369 
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

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

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

372 

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

373 
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

374 
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

375 
val ctxt = Simplifier.the_context ss 
49765
b9eb9c2b87c7
unfolding bounded existential quantifiers as first step in the set_comprehension_pointfree simproc
bulwahn
parents:
49763
diff
changeset

376 
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

377 
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

378 
Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) 
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

379 
(Raw_Simplifier.inherit_context ss empty_ss addsimps 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

380 
val prep_eq = (comprehension_conv ss then_conv unfold_conv prep_thms) ct 
49873
4b7c2e4991fc
extending preprocessing of simproc to rewrite subset inequality into membership of powerset
bulwahn
parents:
49857
diff
changeset

381 
val t' = term_of (Thm.rhs_of prep_eq) 
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

382 
fun mk_thm (fm, t'') = Goal.prove ctxt [] [] 
d9822ec4f434
extending the setcomprehension_pointfree simproc to handle nesting disjunctions, conjunctions and negations (with contributions from Rafal Kolanski, NICTA); tuned
bulwahn
parents:
49831
diff
changeset

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

384 
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

385 
val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms))) 
48108
f93433b451b8
Improved tactic for rewriting set comprehensions into pointfree form.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
48055
diff
changeset

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

387 
Option.map (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

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

389 

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

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

392 
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

393 
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

394 
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

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

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

397 

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

398 
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

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

400 
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

401 
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

402 
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

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

404 
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

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

406 

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

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

409 
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

410 
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

411 
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

412 
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

413 
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

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

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

416 

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

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

419 
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

420 
in 
48128  421 
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

422 
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

423 
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

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

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

426 

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

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

428 