author  haftmann 
Fri, 09 Mar 2007 08:45:50 +0100  
changeset 22422  ee19cdb07528 
parent 22259  476604be7d88 
child 22430  6a56bf1b3a64 
permissions  rwrr 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Predicate.thy 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

2 
ID: $Id$ 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

3 
Author: Stefan Berghofer, TU Muenchen 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

4 
*) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

5 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

6 
header {* Predicates *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

7 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

8 
theory Predicate 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

9 
imports Inductive 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

10 
begin 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

11 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

12 
subsection {* Converting between predicates and sets *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

13 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

14 
definition 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

15 
member :: "'a set => 'a => bool" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

16 
"member == %S x. x : S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

17 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

18 
lemma memberI[intro!, Pure.intro!]: "x : S ==> member S x" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

19 
by (simp add: member_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

20 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

21 
lemma memberD[dest!, Pure.dest!]: "member S x ==> x : S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

22 
by (simp add: member_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

23 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

24 
lemma member_eq[simp]: "member S x = (x : S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

25 
by (simp add: member_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

26 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

27 
lemma member_Collect_eq[simp]: "member (Collect P) = P" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

28 
by (simp add: member_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

29 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

30 
lemma Collect_member_eq[simp]: "Collect (member S) = S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

31 
by (simp add: member_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

32 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

33 
lemma split_set: "(!!S. PROP P S) == (!!S. PROP P (Collect S))" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

34 
proof 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

35 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

36 
assume "!!S. PROP P S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

37 
show "PROP P (Collect S)" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

38 
next 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

39 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

40 
assume "!!S. PROP P (Collect S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

41 
have "PROP P {x. x : S}" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

42 
thus "PROP P S" by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

43 
qed 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

44 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

45 
lemma split_predicate: "(!!S. PROP P S) == (!!S. PROP P (member S))" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

46 
proof 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

47 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

48 
assume "!!S. PROP P S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

49 
show "PROP P (member S)" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

50 
next 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

51 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

52 
assume "!!S. PROP P (member S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

53 
have "PROP P (member {x. S x})" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

54 
thus "PROP P S" by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

55 
qed 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

56 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

57 
lemma member_right_eq: "(x == member y) == (Collect x == y)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

58 
by (rule equal_intr_rule, simp, drule symmetric, simp) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

59 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

60 
definition 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

61 
member2 :: "('a * 'b) set => 'a => 'b \<Rightarrow> bool" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

62 
"member2 == %S x y. (x, y) : S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

63 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

64 
definition 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

65 
Collect2 :: "('a => 'b => bool) => ('a * 'b) set" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

66 
"Collect2 == %P. {(x, y). P x y}" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

67 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

68 
lemma member2I[intro!, Pure.intro!]: "(x, y) : S ==> member2 S x y" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

69 
by (simp add: member2_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

70 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

71 
lemma member2D[dest!, Pure.dest!]: "member2 S x y ==> (x, y) : S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

72 
by (simp add: member2_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

73 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

74 
lemma member2_eq[simp]: "member2 S x y = ((x, y) : S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

75 
by (simp add: member2_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

76 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

77 
lemma Collect2I: "P x y ==> (x, y) : Collect2 P" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

78 
by (simp add: Collect2_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

79 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

80 
lemma Collect2D: "(x, y) : Collect2 P ==> P x y" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

81 
by (simp add: Collect2_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

82 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

83 
lemma member2_Collect2_eq[simp]: "member2 (Collect2 P) = P" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

84 
by (simp add: member2_def Collect2_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

85 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

86 
lemma Collect2_member2_eq[simp]: "Collect2 (member2 S) = S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

87 
by (auto simp add: member2_def Collect2_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

88 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

89 
lemma mem_Collect2_eq[iff]: "((x, y) : Collect2 P) = P x y" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

90 
by (iprover intro: Collect2I dest: Collect2D) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

91 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

92 
lemma member2_Collect_split_eq [simp]: "member2 (Collect (split P)) = P" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

93 
by (simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

94 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

95 
lemma split_set2: "(!!S. PROP P S) == (!!S. PROP P (Collect2 S))" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

96 
proof 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

97 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

98 
assume "!!S. PROP P S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

99 
show "PROP P (Collect2 S)" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

100 
next 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

101 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

102 
assume "!!S. PROP P (Collect2 S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

103 
have "PROP P (Collect2 (member2 S))" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

104 
thus "PROP P S" by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

105 
qed 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

106 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

107 
lemma split_predicate2: "(!!S. PROP P S) == (!!S. PROP P (member2 S))" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

108 
proof 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

109 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

110 
assume "!!S. PROP P S" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

111 
show "PROP P (member2 S)" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

112 
next 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

113 
fix S 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

114 
assume "!!S. PROP P (member2 S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

115 
have "PROP P (member2 (Collect2 S))" . 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

116 
thus "PROP P S" by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

117 
qed 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

118 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

119 
lemma member2_right_eq: "(x == member2 y) == (Collect2 x == y)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

120 
by (rule equal_intr_rule, simp, drule symmetric, simp) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

121 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

122 
ML_setup {* 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

123 
local 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

124 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

125 
fun vars_of b (v as Var _) = if b then [] else [v] 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

126 
 vars_of b (t $ u) = vars_of true t union vars_of false u 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

127 
 vars_of b (Abs (_, _, t)) = vars_of false t 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

128 
 vars_of _ _ = []; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

129 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

130 
fun rew ths1 ths2 th = Drule.forall_elim_vars 0 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

131 
(rewrite_rule ths2 (rewrite_rule ths1 (Drule.forall_intr_list 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

132 
(map (cterm_of (theory_of_thm th)) (vars_of false (prop_of th))) th))); 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

133 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

134 
val get_eq = Simpdata.mk_eq o thm; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

135 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

136 
val split_predicate = get_eq "split_predicate"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

137 
val split_predicate2 = get_eq "split_predicate2"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

138 
val split_set = get_eq "split_set"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

139 
val split_set2 = get_eq "split_set2"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

140 
val member_eq = get_eq "member_eq"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

141 
val member2_eq = get_eq "member2_eq"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

142 
val member_Collect_eq = get_eq "member_Collect_eq"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

143 
val member2_Collect2_eq = get_eq "member2_Collect2_eq"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

144 
val mem_Collect2_eq = get_eq "mem_Collect2_eq"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

145 
val member_right_eq = thm "member_right_eq"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

146 
val member2_right_eq = thm "member2_right_eq"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

147 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

148 
val rew' = Thm.symmetric o rew [split_set2] [split_set, 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

149 
member_right_eq, member2_right_eq, member_Collect_eq, member2_Collect2_eq]; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

150 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

151 
val rules1 = [split_predicate, split_predicate2, member_eq, member2_eq]; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

152 
val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq]; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

153 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

154 
structure PredSetConvData = GenericDataFun 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

155 
(struct 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

156 
val name = "HOL/pred_set_conv"; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

157 
type T = thm list; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

158 
val empty = []; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

159 
val extend = I; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

160 
fun merge _ = Drule.merge_rules; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

161 
fun print _ _ = () 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

162 
end) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

163 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

164 
fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths => 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

165 
Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

166 
(ths @ PredSetConvData.get ctxt) @ ths2)))); 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

167 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

168 
val pred_set_conv_att = Attrib.no_args (Thm.declaration_attribute 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

169 
(Drule.add_rule #> PredSetConvData.map)); 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

170 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

171 
in 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

172 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

173 
val _ = ML_Context.>> (PredSetConvData.init #> 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

174 
Attrib.add_attributes 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

175 
[("pred_set_conv", pred_set_conv_att, 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

176 
"declare rules for converting between predicate and set notation"), 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

177 
("to_set", mk_attr [] rules1 I, "convert rule to set notation"), 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

178 
("to_pred", mk_attr [split_set2] rules2 rew', 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

179 
"convert rule to predicate notation")]) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

180 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

181 
end; 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

182 
*} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

183 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

184 
lemma member_inject [pred_set_conv]: "(member R = member S) = (R = S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

185 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

186 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

187 
lemma member2_inject [pred_set_conv]: "(member2 R = member2 S) = (R = S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

188 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

189 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

190 
lemma member_mono [pred_set_conv]: "(member R <= member S) = (R <= S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

191 
by fast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

192 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

193 
lemma member2_mono [pred_set_conv]: "(member2 R <= member2 S) = (R <= S)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

194 
by fast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

195 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

196 
lemma member_empty [pred_set_conv]: "(%x. False) = member {}" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

197 
by (simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

198 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

199 
lemma member2_empty [pred_set_conv]: "(%x y. False) = member2 {}" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

200 
by (simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

201 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

202 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

203 
subsubsection {* Binary union *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

204 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

205 
lemma member_Un [pred_set_conv]: "sup (member R) (member S) = member (R Un S)" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

206 
by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

207 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

208 
lemma member2_Un [pred_set_conv]: "sup (member2 R) (member2 S) = member2 (R Un S)" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

209 
by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

210 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

211 
lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x  B x" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

212 
by (simp add: sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

213 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

214 
lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y  B x y" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

215 
by (simp add: sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

216 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

217 
lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

218 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

219 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

220 
lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

221 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

222 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

223 
lemma join1I2 [elim?]: "B x \<Longrightarrow> sup A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

224 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

225 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

226 
lemma sup1I2 [elim?]: "B x y \<Longrightarrow> sup A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

227 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

228 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

229 
text {* 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

230 
\medskip Classical introduction rule: no commitment to @{text A} vs 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

231 
@{text B}. 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

232 
*} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

233 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

234 
lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

235 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

236 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

237 
lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

238 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

239 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

240 
lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

241 
by simp iprover 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

242 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

243 
lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

244 
by simp iprover 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

245 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

246 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

247 
subsubsection {* Binary intersection *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

248 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

249 
lemma member_Int [pred_set_conv]: "inf (member R) (member S) = member (R Int S)" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

250 
by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

251 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

252 
lemma member2_Int [pred_set_conv]: "inf (member2 R) (member2 S) = member2 (R Int S)" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

253 
by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

254 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

255 
lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

256 
by (simp add: inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

257 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

258 
lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

259 
by (simp add: inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

260 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

261 
lemma inf1I [intro!]: "A x ==> B x ==> inf A B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

262 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

263 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

264 
lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

265 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

266 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

267 
lemma inf1D1: "inf A B x ==> A x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

268 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

269 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

270 
lemma inf2D1: "inf A B x y ==> A x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

271 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

272 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

273 
lemma inf1D2: "inf A B x ==> B x" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

274 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

275 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

276 
lemma inf2D2: "inf A B x y ==> B x y" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

277 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

278 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

279 
lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

280 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

281 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

282 
lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

283 
by simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

284 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

285 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

286 
subsubsection {* Unions of families *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

287 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

288 
lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

289 
by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

290 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

291 
lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

292 
by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

293 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

294 
lemma SUP1_iff [simp]: "((SUP x. B x) b) = (EX x. B x b)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

295 
by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

296 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

297 
lemma SUP2_iff [simp]: "((SUP x. B x) b c) = (EX x. B x b c)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

298 
by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

299 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

300 
lemma SUP1_I [intro]: "B a b ==> (SUP x. B x) b" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

301 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

302 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

303 
lemma SUP2_I [intro]: "B a b c ==> (SUP x. B x) b c" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

304 
by auto 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

305 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

306 
lemma SUP1_E [elim!]: "(SUP x. B x) b ==> (!!x. B x b ==> R) ==> R" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

307 
by simp iprover 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

308 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

309 
lemma SUP2_E [elim!]: "(SUP x. B x) b c ==> (!!x. B x b c ==> R) ==> R" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

310 
by simp iprover 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

311 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

312 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

313 
subsection {* Composition of two relations *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

314 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

315 
inductive2 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

316 
pred_comp :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

317 
(infixr "OO" 75) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

318 
for r :: "'b => 'c => bool" and s :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

319 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

320 
pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

321 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

322 
inductive_cases2 pred_compE [elim!]: "(r OO s) a c" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

323 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

324 
lemma pred_comp_rel_comp_eq [pred_set_conv]: 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

325 
"(member2 r OO member2 s) = member2 (r O s)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

326 
by (auto simp add: expand_fun_eq elim: pred_compE) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

327 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

328 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

329 
subsection {* Converse *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

330 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

331 
inductive2 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

332 
conversep :: "('a => 'b => bool) => 'b => 'a => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

333 
("(_^1)" [1000] 1000) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

334 
for r :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

335 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

336 
conversepI: "r a b ==> r^1 b a" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

337 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

338 
notation (xsymbols) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

339 
conversep ("(_\<inverse>\<inverse>)" [1000] 1000) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

340 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

341 
lemma conversepD: 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

342 
assumes ab: "r^1 a b" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

343 
shows "r b a" using ab 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

344 
by cases simp 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

345 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

346 
lemma conversep_iff [iff]: "r^1 a b = r b a" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

347 
by (iprover intro: conversepI dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

348 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

349 
lemma conversep_converse_eq [pred_set_conv]: 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

350 
"(member2 r)^1 = member2 (r^1)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

351 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

352 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

353 
lemma conversep_conversep [simp]: "(r^1)^1 = r" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

354 
by (iprover intro: order_antisym conversepI dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

355 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

356 
lemma converse_pred_comp: "(r OO s)^1 = s^1 OO r^1" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

357 
by (iprover intro: order_antisym conversepI pred_compI 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

358 
elim: pred_compE dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

359 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

360 
lemma converse_meet: "(inf r s)^1 = inf r^1 s^1" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

361 
by (simp add: inf_fun_eq inf_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

362 
(iprover intro: conversepI ext dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

363 

22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

364 
lemma converse_join: "(sup r s)^1 = sup r^1 s^1" 
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

365 
by (simp add: sup_fun_eq sup_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

366 
(iprover intro: conversepI ext dest: conversepD) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

367 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

368 
lemma conversep_noteq [simp]: "(op ~=)^1 = op ~=" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

369 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

370 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

371 
lemma conversep_eq [simp]: "(op =)^1 = op =" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

372 
by (auto simp add: expand_fun_eq) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

373 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

374 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

375 
subsection {* Domain *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

376 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

377 
inductive2 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

378 
DomainP :: "('a => 'b => bool) => 'a => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

379 
for r :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

380 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

381 
DomainPI [intro]: "r a b ==> DomainP r a" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

382 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

383 
inductive_cases2 DomainPE [elim!]: "DomainP r a" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

384 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

385 
lemma member2_DomainP [pred_set_conv]: "DomainP (member2 r) = member (Domain r)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

386 
by (blast intro!: Orderings.order_antisym) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

387 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

388 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

389 
subsection {* Range *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

390 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

391 
inductive2 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

392 
RangeP :: "('a => 'b => bool) => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

393 
for r :: "'a => 'b => bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

394 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

395 
RangePI [intro]: "r a b ==> RangeP r b" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

396 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

397 
inductive_cases2 RangePE [elim!]: "RangeP r b" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

398 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

399 
lemma member2_RangeP [pred_set_conv]: "RangeP (member2 r) = member (Range r)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

400 
by (blast intro!: Orderings.order_antisym) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

401 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

402 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

403 
subsection {* Inverse image *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

404 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

405 
definition 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

406 
inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

407 
"inv_imagep r f == %x y. r (f x) (f y)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

408 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

409 
lemma [pred_set_conv]: "inv_imagep (member2 r) f = member2 (inv_image r f)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

410 
by (simp add: inv_image_def inv_imagep_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

411 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

412 
lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

413 
by (simp add: inv_imagep_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

414 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

415 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

416 
subsection {* Properties of relations  predicate versions *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

417 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

418 
abbreviation antisymP :: "('a => 'a => bool) => bool" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

419 
"antisymP r == antisym (Collect2 r)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

420 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

421 
abbreviation transP :: "('a => 'a => bool) => bool" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

422 
"transP r == trans (Collect2 r)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

423 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

424 
abbreviation single_valuedP :: "('a => 'b => bool) => bool" where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

425 
"single_valuedP r == single_valued (Collect2 r)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

426 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

427 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

428 
subsection {* Bounded quantifiers for predicates *} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

429 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

430 
text {* 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

431 
Bounded existential quantifier for predicates (executable). 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

432 
*} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

433 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

434 
inductive2 bexp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

435 
for P :: "'a \<Rightarrow> bool" and Q :: "'a \<Rightarrow> bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

436 
where 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

437 
bexpI [intro]: "P x \<Longrightarrow> Q x \<Longrightarrow> bexp P Q" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

438 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

439 
lemmas bexpE [elim!] = bexp.cases 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

440 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

441 
syntax 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

442 
Bexp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<triangleright>_./ _)" [0, 0, 10] 10) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

443 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

444 
translations 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

445 
"\<exists>x\<triangleright>P. Q" \<rightleftharpoons> "CONST bexp P (\<lambda>x. Q)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

446 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

447 
constdefs 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

448 
ballp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

449 
"ballp P Q \<equiv> \<forall>x. P x \<longrightarrow> Q x" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

450 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

451 
syntax 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

452 
Ballp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<triangleright>_./ _)" [0, 0, 10] 10) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

453 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

454 
translations 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

455 
"\<forall>x\<triangleright>P. Q" \<rightleftharpoons> "CONST ballp P (\<lambda>x. Q)" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

456 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

457 
(* To avoid etacontraction of body: *) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

458 
print_translation {* 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

459 
let 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

460 
fun btr' syn [A,Abs abs] = 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

461 
let val (x,t) = atomic_abs_tr' abs 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

462 
in Syntax.const syn $ x $ A $ t end 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

463 
in 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

464 
[("ballp", btr' "Ballp"),("bexp", btr' "Bexp")] 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

465 
end 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

466 
*} 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

467 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

468 
lemma ballpI [intro!]: "(\<And>x. A x \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<triangleright>A. P x" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

469 
by (simp add: ballp_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

470 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

471 
lemma bspecp [dest?]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> A x \<Longrightarrow> P x" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

472 
by (simp add: ballp_def) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

473 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

474 
lemma ballpE [elim]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (\<not> A x \<Longrightarrow> Q) \<Longrightarrow> Q" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

475 
by (unfold ballp_def) blast 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

476 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

477 
lemma ballp_not_bexp_eq: "(\<forall>x\<triangleright>P. Q x) = (\<not> (\<exists>x\<triangleright>P. \<not> Q x))" 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

478 
by (blast dest: bspecp) 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

479 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

480 
declare ballp_not_bexp_eq [THEN eq_reflection, code unfold] 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

481 

476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

482 
end 