author  bulwahn 
Thu, 12 Nov 2009 09:10:37 +0100  
changeset 33622  24a91a380ee3 
parent 33607  9b3c4e95380e 
child 33754  f2957bd46faf 
permissions  rwrr 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Predicate.thy 
30328  2 
Author: Stefan Berghofer and Lukas Bulwahn and Florian Haftmann, TU Muenchen 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

4 

30328  5 
header {* Predicates as relations and enumerations *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

6 

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

7 
theory Predicate 
23708  8 
imports Inductive Relation 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

10 

30328  11 
notation 
12 
inf (infixl "\<sqinter>" 70) and 

13 
sup (infixl "\<squnion>" 65) and 

14 
Inf ("\<Sqinter>_" [900] 900) and 

15 
Sup ("\<Squnion>_" [900] 900) and 

16 
top ("\<top>") and 

17 
bot ("\<bottom>") 

18 

19 

20 
subsection {* Predicates as (complete) lattices *} 

21 

32779  22 
subsubsection {* Equality *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

23 

26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

24 
lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)" 
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

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

26 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

27 
lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)" 
26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

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

29 

32779  30 

31 
subsubsection {* Order relation *} 

32 

26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

33 
lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)" 
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

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

35 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

36 
lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

38 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

39 

30328  40 
subsubsection {* Top and bottom elements *} 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

41 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

42 
lemma top1I [intro!]: "top x" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

43 
by (simp add: top_fun_eq top_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

44 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

45 
lemma top2I [intro!]: "top x y" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

46 
by (simp add: top_fun_eq top_bool_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

47 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

48 
lemma bot1E [elim!]: "bot x \<Longrightarrow> P" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

49 
by (simp add: bot_fun_eq bot_bool_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

50 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

51 
lemma bot2E [elim!]: "bot x y \<Longrightarrow> P" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

52 
by (simp add: bot_fun_eq bot_bool_eq) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

53 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

54 
lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

56 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

57 
lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

59 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

60 

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

62 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

63 
lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x" 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

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

65 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

66 
lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

67 
by (simp add: sup_fun_eq sup_bool_eq) 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

68 

7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

69 
lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x" 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

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

71 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

72 
lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

74 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

75 
lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

77 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

78 
lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

80 

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

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

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

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

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

85 

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

86 
lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x" 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

88 

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

89 
lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y" 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

91 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

92 
lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

94 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

95 
lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

97 

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

98 

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

100 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

101 
lemma inf1I [intro!]: "A x ==> B x ==> inf A B x" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

102 
by (simp add: inf_fun_eq inf_bool_eq) 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

103 

7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

104 
lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

105 
by (simp add: inf_fun_eq inf_bool_eq) 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

106 

7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

107 
lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P" 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

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

109 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

110 
lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

111 
by (simp add: inf_fun_eq inf_bool_eq) 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

112 

7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

113 
lemma inf1D1: "inf A B x ==> A x" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

114 
by (simp add: inf_fun_eq inf_bool_eq) 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

115 

7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

116 
lemma inf2D1: "inf A B x y ==> A x y" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

117 
by (simp add: inf_fun_eq inf_bool_eq) 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

118 

7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

119 
lemma inf1D2: "inf A B x ==> B x" 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

120 
by (simp add: inf_fun_eq inf_bool_eq) 
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

121 

7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

122 
lemma inf2D2: "inf A B x y ==> B x y" 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22259
diff
changeset

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

124 

32703
7f9e05b3d0fb
removed potentially dangerous rules from pred_set_conv
haftmann
parents:
32601
diff
changeset

125 
lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

126 
by (simp add: inf_fun_eq inf_bool_eq mem_def) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

127 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

128 
lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

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

130 

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

131 

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

133 

32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

134 
lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)" 
24345  135 
by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

136 

32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

137 
lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)" 
24345  138 
by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

139 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

140 
lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

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

142 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

143 
lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

144 
by (auto simp add: SUP2_iff) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

145 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

146 
lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

147 
by (auto simp add: SUP1_iff) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

148 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

149 
lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

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

151 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

152 
lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

153 
by (simp add: SUP1_iff expand_fun_eq) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

154 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

155 
lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

156 
by (simp add: SUP2_iff expand_fun_eq) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

157 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

158 

30328  159 
subsubsection {* Intersections of families *} 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

160 

32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

161 
lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)" 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

162 
by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

163 

32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

164 
lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)" 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

165 
by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast 
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

166 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

167 
lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

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

169 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

170 
lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

171 
by (auto simp add: INF2_iff) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

172 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

173 
lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

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

175 

22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

176 
lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

177 
by (auto simp add: INF2_iff) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

178 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

179 
lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

180 
by (auto simp add: INF1_iff) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

181 

6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

182 
lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

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

184 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

185 
lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

186 
by (simp add: INF1_iff expand_fun_eq) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

187 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

188 
lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))" 
32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

189 
by (simp add: INF2_iff expand_fun_eq) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

190 

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

191 

30328  192 
subsection {* Predicates as relations *} 
193 

194 
subsubsection {* Composition *} 

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

195 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

196 
inductive 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31932
diff
changeset

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

198 
(infixr "OO" 75) 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31932
diff
changeset

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

200 
where 
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
31932
diff
changeset

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

202 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

204 

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

205 
lemma pred_comp_rel_comp_eq [pred_set_conv]: 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

206 
"((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

208 

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

209 

30328  210 
subsubsection {* Converse *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

211 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

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

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

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

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

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

218 

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

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

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

221 

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

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

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

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

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

226 

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

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

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

229 

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

230 
lemma conversep_converse_eq [pred_set_conv]: 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

231 
"(\<lambda>x y. (x, y) \<in> r)^1 = (\<lambda>x y. (x, y) \<in> r^1)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

233 

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

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

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

236 

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

237 
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

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

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

240 

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

241 
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

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

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

244 

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

245 
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

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

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

248 

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

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

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

251 

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

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

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

254 

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

255 

30328  256 
subsubsection {* Domain *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

257 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

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

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

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

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

263 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

265 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

266 
lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)" 
26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

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

268 

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

269 

30328  270 
subsubsection {* Range *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

271 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

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

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

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

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

277 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

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

279 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

280 
lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)" 
26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

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

282 

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

283 

30328  284 
subsubsection {* Inverse image *} 
22259
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 
definition 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

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

289 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

290 
lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

292 

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

293 
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

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

295 

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

296 

30328  297 
subsubsection {* Powerset *} 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

298 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

299 
definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

300 
"Powp A == \<lambda>B. \<forall>x \<in> B. A x" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

301 

1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

302 
lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

303 
by (auto simp add: Powp_def expand_fun_eq) 
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

304 

26797
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

305 
lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq] 
a6cb51c314f2
 Added mem_def and predicate1I in some of the proofs
berghofe
parents:
24345
diff
changeset

306 

23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

307 

30328  308 
subsubsection {* Properties of relations *} 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

309 

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

310 
abbreviation antisymP :: "('a => 'a => bool) => bool" where 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

311 
"antisymP r == antisym {(x, y). r x y}" 
22259
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 
abbreviation transP :: "('a => 'a => bool) => bool" where 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

314 
"transP r == trans {(x, y). r x y}" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

315 

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

316 
abbreviation single_valuedP :: "('a => 'b => bool) => bool" where 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

317 
"single_valuedP r == single_valued {(x, y). r x y}" 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

318 

30328  319 

320 
subsection {* Predicates as enumerations *} 

321 

322 
subsubsection {* The type of predicate enumerations (a monad) *} 

323 

324 
datatype 'a pred = Pred "'a \<Rightarrow> bool" 

325 

326 
primrec eval :: "'a pred \<Rightarrow> 'a \<Rightarrow> bool" where 

327 
eval_pred: "eval (Pred f) = f" 

328 

329 
lemma Pred_eval [simp]: 

330 
"Pred (eval x) = x" 

331 
by (cases x) simp 

332 

333 
lemma eval_inject: "eval x = eval y \<longleftrightarrow> x = y" 

334 
by (cases x) auto 

335 

336 
definition single :: "'a \<Rightarrow> 'a pred" where 

337 
"single x = Pred ((op =) x)" 

338 

339 
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where 

340 
"P \<guillemotright>= f = Pred (\<lambda>x. (\<exists>y. eval P y \<and> eval (f y) x))" 

341 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

342 
instantiation pred :: (type) "{complete_lattice, boolean_algebra}" 
30328  343 
begin 
344 

345 
definition 

346 
"P \<le> Q \<longleftrightarrow> eval P \<le> eval Q" 

347 

348 
definition 

349 
"P < Q \<longleftrightarrow> eval P < eval Q" 

350 

351 
definition 

352 
"\<bottom> = Pred \<bottom>" 

353 

354 
definition 

355 
"\<top> = Pred \<top>" 

356 

357 
definition 

358 
"P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)" 

359 

360 
definition 

361 
"P \<squnion> Q = Pred (eval P \<squnion> eval Q)" 

362 

363 
definition 

31932  364 
[code del]: "\<Sqinter>A = Pred (INFI A eval)" 
30328  365 

366 
definition 

31932  367 
[code del]: "\<Squnion>A = Pred (SUPR A eval)" 
30328  368 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

369 
definition 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

370 
" P = Pred ( eval P)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

371 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

372 
definition 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

373 
"P  Q = Pred (eval P  eval Q)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

374 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

375 
instance proof 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

376 
qed (auto simp add: less_eq_pred_def less_pred_def 
30328  377 
inf_pred_def sup_pred_def bot_pred_def top_pred_def 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

378 
Inf_pred_def Sup_pred_def uminus_pred_def minus_pred_def fun_Compl_def bool_Compl_def, 
30328  379 
auto simp add: le_fun_def less_fun_def le_bool_def less_bool_def 
380 
eval_inject mem_def) 

381 

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

382 
end 
30328  383 

384 
lemma bind_bind: 

385 
"(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)" 

386 
by (auto simp add: bind_def expand_fun_eq) 

387 

388 
lemma bind_single: 

389 
"P \<guillemotright>= single = P" 

390 
by (simp add: bind_def single_def) 

391 

392 
lemma single_bind: 

393 
"single x \<guillemotright>= P = P x" 

394 
by (simp add: bind_def single_def) 

395 

396 
lemma bottom_bind: 

397 
"\<bottom> \<guillemotright>= P = \<bottom>" 

398 
by (auto simp add: bot_pred_def bind_def expand_fun_eq) 

399 

400 
lemma sup_bind: 

401 
"(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R" 

402 
by (auto simp add: bind_def sup_pred_def expand_fun_eq) 

403 

404 
lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)" 

32601
47d0c967c64e
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
haftmann
parents:
32582
diff
changeset

405 
by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq) 
30328  406 

407 
lemma pred_iffI: 

408 
assumes "\<And>x. eval A x \<Longrightarrow> eval B x" 

409 
and "\<And>x. eval B x \<Longrightarrow> eval A x" 

410 
shows "A = B" 

411 
proof  

412 
from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast 

413 
then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq) 

414 
qed 

415 

416 
lemma singleI: "eval (single x) x" 

417 
unfolding single_def by simp 

418 

419 
lemma singleI_unit: "eval (single ()) x" 

420 
by simp (rule singleI) 

421 

422 
lemma singleE: "eval (single x) y \<Longrightarrow> (y = x \<Longrightarrow> P) \<Longrightarrow> P" 

423 
unfolding single_def by simp 

424 

425 
lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" 

426 
by (erule singleE) simp 

427 

428 
lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y" 

429 
unfolding bind_def by auto 

430 

431 
lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P" 

432 
unfolding bind_def by auto 

433 

434 
lemma botE: "eval \<bottom> x \<Longrightarrow> P" 

435 
unfolding bot_pred_def by auto 

436 

437 
lemma supI1: "eval A x \<Longrightarrow> eval (A \<squnion> B) x" 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

438 
unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq) 
30328  439 

440 
lemma supI2: "eval B x \<Longrightarrow> eval (A \<squnion> B) x" 

32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

441 
unfolding sup_pred_def by (simp add: sup_fun_eq sup_bool_eq) 
30328  442 

443 
lemma supE: "eval (A \<squnion> B) x \<Longrightarrow> (eval A x \<Longrightarrow> P) \<Longrightarrow> (eval B x \<Longrightarrow> P) \<Longrightarrow> P" 

444 
unfolding sup_pred_def by auto 

445 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

446 
lemma single_not_bot [simp]: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

447 
"single x \<noteq> \<bottom>" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

448 
by (auto simp add: single_def bot_pred_def expand_fun_eq) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

449 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

450 
lemma not_bot: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

451 
assumes "A \<noteq> \<bottom>" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

452 
obtains x where "eval A x" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

453 
using assms by (cases A) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

454 
(auto simp add: bot_pred_def, auto simp add: mem_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

455 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

456 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

457 
subsubsection {* Emptiness check and definite choice *} 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

458 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

459 
definition is_empty :: "'a pred \<Rightarrow> bool" where 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

460 
"is_empty A \<longleftrightarrow> A = \<bottom>" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

461 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

462 
lemma is_empty_bot: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

463 
"is_empty \<bottom>" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

464 
by (simp add: is_empty_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

465 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

466 
lemma not_is_empty_single: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

467 
"\<not> is_empty (single x)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

468 
by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

469 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

470 
lemma is_empty_sup: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

471 
"is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

472 
by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

473 

33111  474 
definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where 
475 
"singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())" 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

476 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

477 
lemma singleton_eqI: 
33110  478 
"\<exists>!x. eval A x \<Longrightarrow> eval A x \<Longrightarrow> singleton dfault A = x" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

479 
by (auto simp add: singleton_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

480 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

481 
lemma eval_singletonI: 
33110  482 
"\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

483 
proof  
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

484 
assume assm: "\<exists>!x. eval A x" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

485 
then obtain x where "eval A x" .. 
33110  486 
moreover with assm have "singleton dfault A = x" by (rule singleton_eqI) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

487 
ultimately show ?thesis by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

488 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

489 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

490 
lemma single_singleton: 
33110  491 
"\<exists>!x. eval A x \<Longrightarrow> single (singleton dfault A) = A" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

492 
proof  
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

493 
assume assm: "\<exists>!x. eval A x" 
33110  494 
then have "eval A (singleton dfault A)" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

495 
by (rule eval_singletonI) 
33110  496 
moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

497 
by (rule singleton_eqI) 
33110  498 
ultimately have "eval (single (singleton dfault A)) = eval A" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

499 
by (simp (no_asm_use) add: single_def expand_fun_eq) blast 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

500 
then show ?thesis by (simp add: eval_inject) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

501 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

502 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

503 
lemma singleton_undefinedI: 
33111  504 
"\<not> (\<exists>!x. eval A x) \<Longrightarrow> singleton dfault A = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

505 
by (simp add: singleton_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

506 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

507 
lemma singleton_bot: 
33111  508 
"singleton dfault \<bottom> = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

509 
by (auto simp add: bot_pred_def intro: singleton_undefinedI) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

510 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

511 
lemma singleton_single: 
33110  512 
"singleton dfault (single x) = x" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

513 
by (auto simp add: intro: singleton_eqI singleI elim: singleE) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

514 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

515 
lemma singleton_sup_single_single: 
33111  516 
"singleton dfault (single x \<squnion> single y) = (if x = y then x else dfault ())" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

517 
proof (cases "x = y") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

518 
case True then show ?thesis by (simp add: singleton_single) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

519 
next 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

520 
case False 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

521 
have "eval (single x \<squnion> single y) x" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

522 
and "eval (single x \<squnion> single y) y" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

523 
by (auto intro: supI1 supI2 singleI) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

524 
with False have "\<not> (\<exists>!z. eval (single x \<squnion> single y) z)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

525 
by blast 
33111  526 
then have "singleton dfault (single x \<squnion> single y) = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

527 
by (rule singleton_undefinedI) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

528 
with False show ?thesis by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

529 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

530 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

531 
lemma singleton_sup_aux: 
33110  532 
"singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B 
533 
else if B = \<bottom> then singleton dfault A 

534 
else singleton dfault 

535 
(single (singleton dfault A) \<squnion> single (singleton dfault B)))" 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

536 
proof (cases "(\<exists>!x. eval A x) \<and> (\<exists>!y. eval B y)") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

537 
case True then show ?thesis by (simp add: single_singleton) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

538 
next 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

539 
case False 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

540 
from False have A_or_B: 
33111  541 
"singleton dfault A = dfault () \<or> singleton dfault B = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

542 
by (auto intro!: singleton_undefinedI) 
33110  543 
then have rhs: "singleton dfault 
33111  544 
(single (singleton dfault A) \<squnion> single (singleton dfault B)) = dfault ()" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

545 
by (auto simp add: singleton_sup_single_single singleton_single) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

546 
from False have not_unique: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

547 
"\<not> (\<exists>!x. eval A x) \<or> \<not> (\<exists>!y. eval B y)" by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

548 
show ?thesis proof (cases "A \<noteq> \<bottom> \<and> B \<noteq> \<bottom>") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

549 
case True 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

550 
then obtain a b where a: "eval A a" and b: "eval B b" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

551 
by (blast elim: not_bot) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

552 
with True not_unique have "\<not> (\<exists>!x. eval (A \<squnion> B) x)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

553 
by (auto simp add: sup_pred_def bot_pred_def) 
33111  554 
then have "singleton dfault (A \<squnion> B) = dfault ()" by (rule singleton_undefinedI) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

555 
with True rhs show ?thesis by simp 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

556 
next 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

557 
case False then show ?thesis by auto 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

558 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

559 
qed 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

560 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

561 
lemma singleton_sup: 
33110  562 
"singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B 
563 
else if B = \<bottom> then singleton dfault A 

33111  564 
else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())" 
33110  565 
using singleton_sup_aux [of dfault A B] by (simp only: singleton_sup_single_single) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

566 

30328  567 

568 
subsubsection {* Derived operations *} 

569 

570 
definition if_pred :: "bool \<Rightarrow> unit pred" where 

571 
if_pred_eq: "if_pred b = (if b then single () else \<bottom>)" 

572 

573 
definition not_pred :: "unit pred \<Rightarrow> unit pred" where 

574 
not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())" 

575 

576 
lemma if_predI: "P \<Longrightarrow> eval (if_pred P) ()" 

577 
unfolding if_pred_eq by (auto intro: singleI) 

578 

579 
lemma if_predE: "eval (if_pred b) x \<Longrightarrow> (b \<Longrightarrow> x = () \<Longrightarrow> P) \<Longrightarrow> P" 

580 
unfolding if_pred_eq by (cases b) (auto elim: botE) 

581 

582 
lemma not_predI: "\<not> P \<Longrightarrow> eval (not_pred (Pred (\<lambda>u. P))) ()" 

583 
unfolding not_pred_eq eval_pred by (auto intro: singleI) 

584 

585 
lemma not_predI': "\<not> eval P () \<Longrightarrow> eval (not_pred P) ()" 

586 
unfolding not_pred_eq by (auto intro: singleI) 

587 

588 
lemma not_predE: "eval (not_pred (Pred (\<lambda>u. P))) x \<Longrightarrow> (\<not> P \<Longrightarrow> thesis) \<Longrightarrow> thesis" 

589 
unfolding not_pred_eq 

590 
by (auto split: split_if_asm elim: botE) 

591 

592 
lemma not_predE': "eval (not_pred P) x \<Longrightarrow> (\<not> eval P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" 

593 
unfolding not_pred_eq 

594 
by (auto split: split_if_asm elim: botE) 

595 

596 

597 
subsubsection {* Implementation *} 

598 

599 
datatype 'a seq = Empty  Insert "'a" "'a pred"  Join "'a pred" "'a seq" 

600 

601 
primrec pred_of_seq :: "'a seq \<Rightarrow> 'a pred" where 

602 
"pred_of_seq Empty = \<bottom>" 

603 
 "pred_of_seq (Insert x P) = single x \<squnion> P" 

604 
 "pred_of_seq (Join P xq) = P \<squnion> pred_of_seq xq" 

605 

606 
definition Seq :: "(unit \<Rightarrow> 'a seq) \<Rightarrow> 'a pred" where 

607 
"Seq f = pred_of_seq (f ())" 

608 

609 
code_datatype Seq 

610 

611 
primrec member :: "'a seq \<Rightarrow> 'a \<Rightarrow> bool" where 

612 
"member Empty x \<longleftrightarrow> False" 

613 
 "member (Insert y P) x \<longleftrightarrow> x = y \<or> eval P x" 

614 
 "member (Join P xq) x \<longleftrightarrow> eval P x \<or> member xq x" 

615 

616 
lemma eval_member: 

617 
"member xq = eval (pred_of_seq xq)" 

618 
proof (induct xq) 

619 
case Empty show ?case 

620 
by (auto simp add: expand_fun_eq elim: botE) 

621 
next 

622 
case Insert show ?case 

623 
by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI) 

624 
next 

625 
case Join then show ?case 

626 
by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2) 

627 
qed 

628 

629 
lemma eval_code [code]: "eval (Seq f) = member (f ())" 

630 
unfolding Seq_def by (rule sym, rule eval_member) 

631 

632 
lemma single_code [code]: 

633 
"single x = Seq (\<lambda>u. Insert x \<bottom>)" 

634 
unfolding Seq_def by simp 

635 

636 
primrec "apply" :: "('a \<Rightarrow> 'b Predicate.pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where 

637 
"apply f Empty = Empty" 

638 
 "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)" 

639 
 "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)" 

640 

641 
lemma apply_bind: 

642 
"pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f" 

643 
proof (induct xq) 

644 
case Empty show ?case 

645 
by (simp add: bottom_bind) 

646 
next 

647 
case Insert show ?case 

648 
by (simp add: single_bind sup_bind) 

649 
next 

650 
case Join then show ?case 

651 
by (simp add: sup_bind) 

652 
qed 

653 

654 
lemma bind_code [code]: 

655 
"Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))" 

656 
unfolding Seq_def by (rule sym, rule apply_bind) 

657 

658 
lemma bot_set_code [code]: 

659 
"\<bottom> = Seq (\<lambda>u. Empty)" 

660 
unfolding Seq_def by simp 

661 

30376  662 
primrec adjunct :: "'a pred \<Rightarrow> 'a seq \<Rightarrow> 'a seq" where 
663 
"adjunct P Empty = Join P Empty" 

664 
 "adjunct P (Insert x Q) = Insert x (Q \<squnion> P)" 

665 
 "adjunct P (Join Q xq) = Join Q (adjunct P xq)" 

666 

667 
lemma adjunct_sup: 

668 
"pred_of_seq (adjunct P xq) = P \<squnion> pred_of_seq xq" 

669 
by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute) 

670 

30328  671 
lemma sup_code [code]: 
672 
"Seq f \<squnion> Seq g = Seq (\<lambda>u. case f () 

673 
of Empty \<Rightarrow> g () 

674 
 Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g) 

30376  675 
 Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))" 
30328  676 
proof (cases "f ()") 
677 
case Empty 

678 
thus ?thesis 

30376  679 
unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"] sup_bot) 
30328  680 
next 
681 
case Insert 

682 
thus ?thesis 

683 
unfolding Seq_def by (simp add: sup_assoc) 

684 
next 

685 
case Join 

686 
thus ?thesis 

30376  687 
unfolding Seq_def 
688 
by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) 

30328  689 
qed 
690 

30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

691 
primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

692 
"contained Empty Q \<longleftrightarrow> True" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

693 
 "contained (Insert x P) Q \<longleftrightarrow> eval Q x \<and> P \<le> Q" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

694 
 "contained (Join P xq) Q \<longleftrightarrow> P \<le> Q \<and> contained xq Q" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

695 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

696 
lemma single_less_eq_eval: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

697 
"single x \<le> P \<longleftrightarrow> eval P x" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

698 
by (auto simp add: single_def less_eq_pred_def mem_def) 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

699 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

700 
lemma contained_less_eq: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

701 
"contained xq Q \<longleftrightarrow> pred_of_seq xq \<le> Q" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

702 
by (induct xq) (simp_all add: single_less_eq_eval) 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

703 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

704 
lemma less_eq_pred_code [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

705 
"Seq f \<le> Q = (case f () 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

706 
of Empty \<Rightarrow> True 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

707 
 Insert x P \<Rightarrow> eval Q x \<and> P \<le> Q 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

708 
 Join P xq \<Rightarrow> P \<le> Q \<and> contained xq Q)" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

709 
by (cases "f ()") 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

710 
(simp_all add: Seq_def single_less_eq_eval contained_less_eq) 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

711 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

712 
lemma eq_pred_code [code]: 
31133  713 
fixes P Q :: "'a pred" 
30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

714 
shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

715 
unfolding eq by auto 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

716 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

717 
lemma [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

718 
"pred_case f P = f (eval P)" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

719 
by (cases P) simp 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

720 

42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

721 
lemma [code]: 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

722 
"pred_rec f P = f (eval P)" 
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

723 
by (cases P) simp 
30328  724 

31105
95f66b234086
added general preprocessing of equality in predicates for code generation
bulwahn
parents:
30430
diff
changeset

725 
inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x" 
95f66b234086
added general preprocessing of equality in predicates for code generation
bulwahn
parents:
30430
diff
changeset

726 

95f66b234086
added general preprocessing of equality in predicates for code generation
bulwahn
parents:
30430
diff
changeset

727 
lemma eq_is_eq: "eq x y \<equiv> (x = y)" 
31108  728 
by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) 
30948  729 

31216  730 
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where 
731 
"map f P = P \<guillemotright>= (single o f)" 

732 

32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

733 
primrec null :: "'a seq \<Rightarrow> bool" where 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

734 
"null Empty \<longleftrightarrow> True" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

735 
 "null (Insert x P) \<longleftrightarrow> False" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

736 
 "null (Join P xq) \<longleftrightarrow> is_empty P \<and> null xq" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

737 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

738 
lemma null_is_empty: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

739 
"null xq \<longleftrightarrow> is_empty (pred_of_seq xq)" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

740 
by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

741 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

742 
lemma is_empty_code [code]: 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

743 
"is_empty (Seq f) \<longleftrightarrow> null (f ())" 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

744 
by (simp add: null_is_empty Seq_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

745 

33111  746 
primrec the_only :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a seq \<Rightarrow> 'a" where 
747 
[code del]: "the_only dfault Empty = dfault ()" 

748 
 "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())" 

33110  749 
 "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P 
750 
else let x = singleton dfault P; y = the_only dfault xq in 

33111  751 
if x = y then x else dfault ())" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

752 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

753 
lemma the_only_singleton: 
33110  754 
"the_only dfault xq = singleton dfault (pred_of_seq xq)" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

755 
by (induct xq) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

756 
(auto simp add: singleton_bot singleton_single is_empty_def 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

757 
null_is_empty Let_def singleton_sup) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

758 

22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

759 
lemma singleton_code [code]: 
33110  760 
"singleton dfault (Seq f) = (case f () 
33111  761 
of Empty \<Rightarrow> dfault () 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

762 
 Insert x P \<Rightarrow> if is_empty P then x 
33110  763 
else let y = singleton dfault P in 
33111  764 
if x = y then x else dfault () 
33110  765 
 Join P xq \<Rightarrow> if is_empty P then the_only dfault xq 
766 
else if null xq then singleton dfault P 

767 
else let x = singleton dfault P; y = the_only dfault xq in 

33111  768 
if x = y then x else dfault ())" 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

769 
by (cases "f ()") 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

770 
(auto simp add: Seq_def the_only_singleton is_empty_def 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

771 
null_is_empty singleton_bot singleton_single singleton_sup Let_def) 
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

772 

33110  773 
definition not_unique :: "'a pred => 'a" 
774 
where 

33111  775 
[code del]: "not_unique A = (THE x. eval A x)" 
33110  776 

33111  777 
definition the :: "'a pred => 'a" 
778 
where 

779 
[code del]: "the A = (THE x. eval A x)" 

780 

781 
lemma the_eq[code]: "the A = singleton (\<lambda>x. not_unique A) A" 

782 
by (auto simp add: the_def singleton_def not_unique_def) 

33110  783 

30948  784 
ML {* 
785 
signature PREDICATE = 

786 
sig 

787 
datatype 'a pred = Seq of (unit > 'a seq) 

788 
and 'a seq = Empty  Insert of 'a * 'a pred  Join of 'a pred * 'a seq 

30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

789 
val yield: 'a pred > ('a * 'a pred) option 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

790 
val yieldn: int > 'a pred > 'a list * 'a pred 
31222  791 
val map: ('a > 'b) > 'a pred > 'b pred 
30948  792 
end; 
793 

794 
structure Predicate : PREDICATE = 

795 
struct 

796 

30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

797 
@{code_datatype pred = Seq}; 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

798 
@{code_datatype seq = Empty  Insert  Join}; 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

799 

32372  800 
fun yield (@{code Seq} f) = next (f ()) 
30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

801 
and next @{code Empty} = NONE 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

802 
 next (@{code Insert} (x, P)) = SOME (x, P) 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

803 
 next (@{code Join} (P, xq)) = (case yield P 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

804 
of NONE => next xq 
33607  805 
 SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq)))); 
30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

806 

458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

807 
fun anamorph f k x = (if k = 0 then ([], x) 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

808 
else case f x 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

809 
of NONE => ([], x) 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

810 
 SOME (v, y) => let 
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

811 
val (vs, z) = anamorph f (k  1) y 
33607  812 
in (v :: vs, z) end); 
30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

813 

458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

814 
fun yieldn P = anamorph yield P; 
30948  815 

31222  816 
fun map f = @{code map} f; 
817 

30948  818 
end; 
819 
*} 

820 

821 
code_reserved Eval Predicate 

822 

823 
code_type pred and seq 

824 
(Eval "_/ Predicate.pred" and "_/ Predicate.seq") 

825 

826 
code_const Seq and Empty and Insert and Join 

827 
(Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)") 

828 

33110  829 
code_abort not_unique 
830 

30328  831 
no_notation 
832 
inf (infixl "\<sqinter>" 70) and 

833 
sup (infixl "\<squnion>" 65) and 

834 
Inf ("\<Sqinter>_" [900] 900) and 

835 
Sup ("\<Squnion>_" [900] 900) and 

836 
top ("\<top>") and 

837 
bot ("\<bottom>") and 

838 
bind (infixl "\<guillemotright>=" 70) 

839 

840 
hide (open) type pred seq 

32582  841 
hide (open) const Pred eval single bind is_empty singleton if_pred not_pred 
33111  842 
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the 
30328  843 

844 
end 