author  haftmann 
Wed, 08 Dec 2010 14:52:23 +0100  
changeset 41080  294956ff285b 
parent 41075  4bed56dc95fb 
child 41082  9ff94e7cc3b3 
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 

41080  19 
syntax (xsymbols) 
20 
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 

21 
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 

22 
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 

23 
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 

24 

30328  25 

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

27 

34065
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

28 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

29 
text {* 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

30 
Handy introduction and elimination rules for @{text "\<le>"} 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

31 
on unary and binary predicates 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

32 
*} 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

33 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

34 
lemma predicate1I: 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

35 
assumes PQ: "\<And>x. P x \<Longrightarrow> Q x" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

36 
shows "P \<le> Q" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

37 
apply (rule le_funI) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

38 
apply (rule le_boolI) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

39 
apply (rule PQ) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

40 
apply assumption 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

41 
done 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

42 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

43 
lemma predicate1D [Pure.dest?, dest?]: 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

44 
"P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

45 
apply (erule le_funE) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

46 
apply (erule le_boolE) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

47 
apply assumption+ 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

48 
done 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

49 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

50 
lemma rev_predicate1D: 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

51 
"P x ==> P <= Q ==> Q x" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

52 
by (rule predicate1D) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

53 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

54 
lemma predicate2I [Pure.intro!, intro!]: 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

55 
assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

56 
shows "P \<le> Q" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

57 
apply (rule le_funI)+ 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

58 
apply (rule le_boolI) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

59 
apply (rule PQ) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

60 
apply assumption 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

61 
done 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

62 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

63 
lemma predicate2D [Pure.dest, dest]: 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

64 
"P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

65 
apply (erule le_funE)+ 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

66 
apply (erule le_boolE) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

67 
apply assumption+ 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

68 
done 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

69 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

70 
lemma rev_predicate2D: 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

71 
"P x y ==> P <= Q ==> Q x y" 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

72 
by (rule predicate2D) 
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

73 

6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
34007
diff
changeset

74 

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

76 

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

77 
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

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

79 

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

80 
lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

82 

32779  83 

84 
subsubsection {* Order relation *} 

85 

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

86 
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

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

88 

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

89 
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

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

91 

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

92 

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

94 

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

95 
lemma top1I [intro!]: "top x" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

97 

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

98 
lemma top2I [intro!]: "top x y" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

99 
by (simp add: top_fun_def top_bool_def) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

100 

38651
8aadda8e1338
"no_atp" fact that leads to unsound Sledgehammer proofs
blanchet
parents:
37767
diff
changeset

101 
lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

102 
by (simp add: bot_fun_def bot_bool_def) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

103 

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

104 
lemma bot2E [elim!]: "bot x y \<Longrightarrow> P" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

106 

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

107 
lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

109 

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

110 
lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

112 

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

113 

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

115 

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

116 
lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

118 

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

119 
lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

120 
by (simp add: sup_fun_def sup_bool_def) 
32883
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 sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

124 

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

125 
lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

127 

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

128 
lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

129 
by (simp add: sup_fun_def sup_bool_def) iprover 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

130 

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

131 
lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

132 
by (simp add: sup_fun_def sup_bool_def) iprover 
22259
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 
text {* 
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

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

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

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

138 

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

139 
lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

141 

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

142 
lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

144 

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

145 
lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

147 

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

148 
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)" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

149 
by (simp add: sup_fun_def sup_bool_def mem_def) 
22259
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 

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

153 

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

154 
lemma inf1I [intro!]: "A x ==> B x ==> inf A B x" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

155 
by (simp add: inf_fun_def inf_bool_def) 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

156 

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

157 
lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

158 
by (simp add: inf_fun_def inf_bool_def) 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

159 

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

160 
lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

162 

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

163 
lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

164 
by (simp add: inf_fun_def inf_bool_def) 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

165 

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

166 
lemma inf1D1: "inf A B x ==> A x" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

167 
by (simp add: inf_fun_def inf_bool_def) 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

168 

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

169 
lemma inf2D1: "inf A B x y ==> A x y" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

170 
by (simp add: inf_fun_def inf_bool_def) 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

171 

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

172 
lemma inf1D2: "inf A B x ==> B x" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

173 
by (simp add: inf_fun_def inf_bool_def) 
32883
7cbd93dacef3
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
haftmann
parents:
32782
diff
changeset

174 

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

175 
lemma inf2D2: "inf A B x y ==> B x y" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

177 

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

178 
lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

179 
by (simp add: inf_fun_def inf_bool_def mem_def) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

180 

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

181 
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)" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

182 
by (simp add: inf_fun_def inf_bool_def mem_def) 
22259
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 

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

186 

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

187 
lemma SUP1_iff: "(SUP x:A. B x) b = (EX x:A. B x b)" 
41080  188 
by (simp add: SUPR_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

189 

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

190 
lemma SUP2_iff: "(SUP x:A. B x) b c = (EX x:A. B x b c)" 
41080  191 
by (simp add: SUPR_apply) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

192 

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

193 
lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b" 
41080  194 
by (auto simp add: SUPR_apply) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

195 

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

196 
lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c" 
41080  197 
by (auto simp add: SUPR_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

198 

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

199 
lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R" 
41080  200 
by (auto simp add: SUPR_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

201 

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

202 
lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R" 
41080  203 
by (auto simp add: SUPR_apply) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

204 

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

205 
lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))" 
41080  206 
by (simp add: SUPR_apply fun_eq_iff) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

207 

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

208 
lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))" 
41080  209 
by (simp add: SUPR_apply fun_eq_iff) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

210 

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

211 

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

213 

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

214 
lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)" 
41080  215 
by (simp add: INFI_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

216 

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

217 
lemma INF2_iff: "(INF x:A. B x) b c = (ALL x:A. B x b c)" 
41080  218 
by (simp add: INFI_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

219 

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

220 
lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b" 
41080  221 
by (auto simp add: INFI_apply) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

222 

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

223 
lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c" 
41080  224 
by (auto simp add: INFI_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

225 

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

226 
lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b" 
41080  227 
by (auto simp add: INFI_apply) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

228 

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

229 
lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c" 
41080  230 
by (auto simp add: INFI_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

231 

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

232 
lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R" 
41080  233 
by (auto simp add: INFI_apply) 
22430
6a56bf1b3a64
Generalized version of SUP and INF (with index set).
berghofe
parents:
22422
diff
changeset

234 

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

235 
lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R" 
41080  236 
by (auto simp add: INFI_apply) 
22259
476604be7d88
New theory for converting between predicates and sets.
berghofe
parents:
diff
changeset

237 

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

238 
lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))" 
41080  239 
by (simp add: INFI_apply fun_eq_iff) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

240 

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

241 
lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))" 
41080  242 
by (simp add: INFI_apply fun_eq_iff) 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

243 

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

244 

30328  245 
subsection {* Predicates as relations *} 
246 

247 
subsubsection {* Composition *} 

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

248 

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

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

250 
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

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

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

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

254 
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

255 

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

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

257 

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

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

259 
"((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

261 

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

262 

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

264 

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

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

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

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

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

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

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

271 

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

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

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

274 

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

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

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

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

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

279 

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

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

281 
by (iprover intro: conversepI dest: conversepD) 
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 
lemma conversep_converse_eq [pred_set_conv]: 
23741
1801a921df13
 Moved infrastructure for converting between sets and predicates
berghofe
parents:
23708
diff
changeset

284 
"(\<lambda>x y. (x, y) \<in> r)^1 = (\<lambda>x y. (x, y) \<in> r^1)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

286 

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

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

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

289 

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

290 
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

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

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

293 

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

294 
lemma converse_meet: "(inf r s)^1 = inf r^1 s^1" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

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

297 

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

298 
lemma converse_join: "(sup r s)^1 = sup r^1 s^1" 
41075
4bed56dc95fb
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann
parents:
40813
diff
changeset

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

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

301 

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

302 
lemma conversep_noteq [simp]: "(op ~=)^1 = op ~=" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

304 

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

305 
lemma conversep_eq [simp]: "(op =)^1 = op =" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

307 

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

308 

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

310 

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

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

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

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

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

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

316 

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

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

318 

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

319 
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

320 
by (blast intro!: Orderings.order_antisym predicate1I) 
22259
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 

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

324 

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

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

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

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

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

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

330 

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

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

332 

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

333 
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

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

335 

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

336 

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

338 

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

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

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

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

342 

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

343 
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

344 
by (simp add: inv_image_def inv_imagep_def) 
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 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

347 
by (simp add: inv_imagep_def) 
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 

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

351 

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

352 
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

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

354 

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

355 
lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

357 

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

358 
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

359 

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

360 

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

362 

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

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

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

365 

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

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

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

368 

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

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

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

371 

40813
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

372 
(*FIXME inconsistencies: abbreviations vs. definitions, suffix `P` vs. suffix `p`*) 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

373 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

374 
definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

375 
"reflp r \<longleftrightarrow> refl {(x, y). r x y}" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

376 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

377 
definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

378 
"symp r \<longleftrightarrow> sym {(x, y). r x y}" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

379 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

380 
definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

381 
"transp r \<longleftrightarrow> trans {(x, y). r x y}" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

382 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

383 
lemma reflpI: 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

384 
"(\<And>x. r x x) \<Longrightarrow> reflp r" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

385 
by (auto intro: refl_onI simp add: reflp_def) 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

386 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

387 
lemma reflpE: 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

388 
assumes "reflp r" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

389 
obtains "r x x" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

390 
using assms by (auto dest: refl_onD simp add: reflp_def) 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

391 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

392 
lemma sympI: 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

393 
"(\<And>x y. r x y \<Longrightarrow> r y x) \<Longrightarrow> symp r" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

394 
by (auto intro: symI simp add: symp_def) 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

395 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

396 
lemma sympE: 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

397 
assumes "symp r" and "r x y" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

398 
obtains "r y x" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

399 
using assms by (auto dest: symD simp add: symp_def) 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

400 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

401 
lemma transpI: 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

402 
"(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

403 
by (auto intro: transI simp add: transp_def) 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

404 

f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

405 
lemma transpE: 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

406 
assumes "transp r" and "r x y" and "r y z" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

407 
obtains "r x z" 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

408 
using assms by (auto dest: transD simp add: transp_def) 
f1fc2a1547eb
moved generic definitions about relations from Quotient.thy to Predicate;
haftmann
parents:
40674
diff
changeset

409 

30328  410 

411 
subsection {* Predicates as enumerations *} 

412 

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

414 

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

416 

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

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

419 

420 
lemma Pred_eval [simp]: 

421 
"Pred (eval x) = x" 

422 
by (cases x) simp 

423 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

424 
lemma pred_eqI: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

425 
"(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

426 
by (cases P, cases Q) (auto simp add: fun_eq_iff) 
30328  427 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

428 
lemma eval_mem [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

429 
"x \<in> eval P \<longleftrightarrow> eval P x" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

430 
by (simp add: mem_def) 
30328  431 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

432 
lemma eq_mem [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

433 
"x \<in> (op =) y \<longleftrightarrow> x = y" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

434 
by (auto simp add: mem_def) 
30328  435 

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

436 
instantiation pred :: (type) "{complete_lattice, boolean_algebra}" 
30328  437 
begin 
438 

439 
definition 

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

441 

442 
definition 

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

444 

445 
definition 

446 
"\<bottom> = Pred \<bottom>" 

447 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

448 
lemma eval_bot [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

449 
"eval \<bottom> = \<bottom>" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

450 
by (simp add: bot_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

451 

30328  452 
definition 
453 
"\<top> = Pred \<top>" 

454 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

455 
lemma eval_top [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

456 
"eval \<top> = \<top>" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

457 
by (simp add: top_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

458 

30328  459 
definition 
460 
"P \<sqinter> Q = Pred (eval P \<sqinter> eval Q)" 

461 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

462 
lemma eval_inf [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

463 
"eval (P \<sqinter> Q) = eval P \<sqinter> eval Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

464 
by (simp add: inf_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

465 

30328  466 
definition 
467 
"P \<squnion> Q = Pred (eval P \<squnion> eval Q)" 

468 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

469 
lemma eval_sup [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

470 
"eval (P \<squnion> Q) = eval P \<squnion> eval Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

471 
by (simp add: sup_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

472 

30328  473 
definition 
37767  474 
"\<Sqinter>A = Pred (INFI A eval)" 
30328  475 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

476 
lemma eval_Inf [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

477 
"eval (\<Sqinter>A) = INFI A eval" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

478 
by (simp add: Inf_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

479 

30328  480 
definition 
37767  481 
"\<Squnion>A = Pred (SUPR A eval)" 
30328  482 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

483 
lemma eval_Sup [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

484 
"eval (\<Squnion>A) = SUPR A eval" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

485 
by (simp add: Sup_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

486 

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

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

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

489 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

490 
lemma eval_compl [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

491 
"eval ( P) =  eval P" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

492 
by (simp add: uminus_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

493 

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

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

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

496 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

497 
lemma eval_minus [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

498 
"eval (P  Q) = eval P  eval Q" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

499 
by (simp add: minus_pred_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

500 

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

501 
instance proof 
41080  502 
qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def uminus_apply minus_apply) 
30328  503 

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

504 
end 
30328  505 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

506 
lemma eval_INFI [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

507 
"eval (INFI A f) = INFI A (eval \<circ> f)" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

508 
by (unfold INFI_def) simp 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

509 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

510 
lemma eval_SUPR [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

511 
"eval (SUPR A f) = SUPR A (eval \<circ> f)" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

512 
by (unfold SUPR_def) simp 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

513 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

514 
definition single :: "'a \<Rightarrow> 'a pred" where 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

515 
"single x = Pred ((op =) x)" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

516 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

517 
lemma eval_single [simp]: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

518 
"eval (single x) = (op =) x" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

519 
by (simp add: single_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

520 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

521 
definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where 
41080  522 
"P \<guillemotright>= f = (SUPR {x. eval P x} f)" 
40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

523 

c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

524 
lemma eval_bind [simp]: 
41080  525 
"eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)" 
40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

526 
by (simp add: bind_def) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

527 

30328  528 
lemma bind_bind: 
529 
"(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)" 

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

530 
by (rule pred_eqI) auto 
30328  531 

532 
lemma bind_single: 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

534 
by (rule pred_eqI) auto 
30328  535 

536 
lemma single_bind: 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

538 
by (rule pred_eqI) auto 
30328  539 

540 
lemma bottom_bind: 

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

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

542 
by (rule pred_eqI) auto 
30328  543 

544 
lemma sup_bind: 

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

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

546 
by (rule pred_eqI) auto 
30328  547 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

548 
lemma Sup_bind: 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

549 
"(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)" 
40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

550 
by (rule pred_eqI) auto 
30328  551 

552 
lemma pred_iffI: 

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

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

555 
shows "A = B" 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

556 
using assms by (auto intro: pred_eqI) 
30328  557 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

559 
by simp 
30328  560 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

562 
by simp 
30328  563 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

565 
by simp 
30328  566 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

568 
by simp 
30328  569 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

571 
by auto 
30328  572 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

574 
by auto 
30328  575 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

577 
by auto 
30328  578 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

580 
by auto 
30328  581 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

583 
by auto 
30328  584 

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

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

586 
by auto 
30328  587 

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

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

589 
"single x \<noteq> \<bottom>" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

591 

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

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

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

594 
obtains x where "eval A x" 
40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

595 
using assms by (cases A) 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

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

597 

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

598 

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

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

600 

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

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

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

603 

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

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

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

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

607 

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

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

609 
"\<not> is_empty (single x)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

611 

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

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

613 
"is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B" 
36008  614 
by (auto simp add: is_empty_def) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

615 

40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

616 
definition singleton :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where 
33111  617 
"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

618 

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

619 
lemma singleton_eqI: 
33110  620 
"\<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

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

622 

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

623 
lemma eval_singletonI: 
33110  624 
"\<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

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

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

627 
then obtain x where "eval A x" .. 
33110  628 
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

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

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

631 

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

632 
lemma single_singleton: 
33110  633 
"\<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

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

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

637 
by (rule eval_singletonI) 
33110  638 
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

639 
by (rule singleton_eqI) 
33110  640 
ultimately have "eval (single (singleton dfault A)) = eval A" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

641 
by (simp (no_asm_use) add: single_def fun_eq_iff) blast 
40616
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

642 
then have "\<And>x. eval (single (singleton dfault A)) x = eval A x" 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

643 
by simp 
c5ee1e06d795
eval simp rules for predicate type, simplify primitive proofs
haftmann
parents:
39302
diff
changeset

644 
then show ?thesis by (rule pred_eqI) 
32578
22117a76f943
added emptiness check predicate and singleton projection
haftmann
parents:
32372
diff
changeset

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

646 

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

647 
lemma singleton_undefinedI: 
33111  648 
"\<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

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

650 

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

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

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

654 

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

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

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

658 

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

659 
lemma singleton_sup_single_single: 
33111  660 
"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

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

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

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

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

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

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

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

668 
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

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

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

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

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

674 

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

675 
lemma singleton_sup_aux: 
33110  676 
"singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B 
677 
else if B = \<bottom> then singleton dfault A 

678 
else singleton dfault 

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

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

680 
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

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

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

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

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

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

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

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

691 
"\<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

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

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

694 
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

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

696 
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

697 
by (auto simp add: sup_pred_def bot_pred_def) 
33111  698 
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

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

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

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

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

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

704 

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

705 
lemma singleton_sup: 
33110  706 
"singleton dfault (A \<squnion> B) = (if A = \<bottom> then singleton dfault B 
707 
else if B = \<bottom> then singleton dfault A 

33111  708 
else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())" 
33110  709 
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

710 

30328  711 

712 
subsubsection {* Derived operations *} 

713 

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

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

716 

33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

717 
definition holds :: "unit pred \<Rightarrow> bool" where 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

718 
holds_eq: "holds P = eval P ()" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

719 

30328  720 
definition not_pred :: "unit pred \<Rightarrow> unit pred" where 
721 
not_pred_eq: "not_pred P = (if eval P () then \<bottom> else single ())" 

722 

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

724 
unfolding if_pred_eq by (auto intro: singleI) 

725 

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

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

728 

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

730 
unfolding not_pred_eq eval_pred by (auto intro: singleI) 

731 

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

733 
unfolding not_pred_eq by (auto intro: singleI) 

734 

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

736 
unfolding not_pred_eq 

737 
by (auto split: split_if_asm elim: botE) 

738 

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

740 
unfolding not_pred_eq 

741 
by (auto split: split_if_asm elim: botE) 

33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

742 
lemma "f () = False \<or> f () = True" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

743 
by simp 
30328  744 

37549  745 
lemma closure_of_bool_cases [no_atp]: 
33754
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

746 
assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

747 
assumes "f = (%u. True) \<Longrightarrow> P f" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

748 
shows "P f" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

749 
proof  
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

750 
have "f = (%u. False) \<or> f = (%u. True)" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

751 
apply (cases "f ()") 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

752 
apply (rule disjI2) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

753 
apply (rule ext) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

754 
apply (simp add: unit_eq) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

755 
apply (rule disjI1) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

756 
apply (rule ext) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

757 
apply (simp add: unit_eq) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

758 
done 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

759 
from this prems show ?thesis by blast 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

760 
qed 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

761 

f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

762 
lemma unit_pred_cases: 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

763 
assumes "P \<bottom>" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

764 
assumes "P (single ())" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

765 
shows "P Q" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

766 
using assms 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

767 
unfolding bot_pred_def Collect_def empty_def single_def 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

768 
apply (cases Q) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

769 
apply simp 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

770 
apply (rule_tac f="fun" in closure_of_bool_cases) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

771 
apply auto 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

772 
apply (subgoal_tac "(%x. () = x) = (%x. True)") 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

773 
apply auto 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

774 
done 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

775 

f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

776 
lemma holds_if_pred: 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

777 
"holds (if_pred b) = b" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

778 
unfolding if_pred_eq holds_eq 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

779 
by (cases b) (auto intro: singleI elim: botE) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

780 

f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

781 
lemma if_pred_holds: 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

782 
"if_pred (holds P) = P" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

783 
unfolding if_pred_eq holds_eq 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

784 
by (rule unit_pred_cases) (auto intro: singleI elim: botE) 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

785 

f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

786 
lemma is_empty_holds: 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

787 
"is_empty P \<longleftrightarrow> \<not> holds P" 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

788 
unfolding is_empty_def holds_eq 
f2957bd46faf
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
bulwahn
parents:
33622
diff
changeset

789 
by (rule unit_pred_cases) (auto elim: botE intro: singleI) 
30328  790 

791 
subsubsection {* Implementation *} 

792 

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

794 

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

796 
"pred_of_seq Empty = \<bottom>" 

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

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

799 

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

801 
"Seq f = pred_of_seq (f ())" 

802 

803 
code_datatype Seq 

804 

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

806 
"member Empty x \<longleftrightarrow> False" 

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

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

809 

810 
lemma eval_member: 

811 
"member xq = eval (pred_of_seq xq)" 

812 
proof (induct xq) 

813 
case Empty show ?case 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

814 
by (auto simp add: fun_eq_iff elim: botE) 
30328  815 
next 
816 
case Insert show ?case 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

817 
by (auto simp add: fun_eq_iff elim: supE singleE intro: supI1 supI2 singleI) 
30328  818 
next 
819 
case Join then show ?case 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

820 
by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2) 
30328  821 
qed 
822 

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

824 
unfolding Seq_def by (rule sym, rule eval_member) 

825 

826 
lemma single_code [code]: 

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

828 
unfolding Seq_def by simp 

829 

41080  830 
primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where 
30328  831 
"apply f Empty = Empty" 
832 
 "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)" 

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

834 

835 
lemma apply_bind: 

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

837 
proof (induct xq) 

838 
case Empty show ?case 

839 
by (simp add: bottom_bind) 

840 
next 

841 
case Insert show ?case 

842 
by (simp add: single_bind sup_bind) 

843 
next 

844 
case Join then show ?case 

845 
by (simp add: sup_bind) 

846 
qed 

847 

848 
lemma bind_code [code]: 

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

850 
unfolding Seq_def by (rule sym, rule apply_bind) 

851 

852 
lemma bot_set_code [code]: 

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

854 
unfolding Seq_def by simp 

855 

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

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

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

860 

861 
lemma adjunct_sup: 

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

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

864 

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

867 
of Empty \<Rightarrow> g () 

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

30376  869 
 Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))" 
30328  870 
proof (cases "f ()") 
871 
case Empty 

872 
thus ?thesis 

34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33988
diff
changeset

873 
unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]) 
30328  874 
next 
875 
case Insert 

876 
thus ?thesis 

877 
unfolding Seq_def by (simp add: sup_assoc) 

878 
next 

879 
case Join 

880 
thus ?thesis 

30376  881 
unfolding Seq_def 
882 
by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) 

30328  883 
qed 
884 

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

885 
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

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

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

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

889 

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

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

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

892 
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

893 

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

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

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

896 
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

897 

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

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

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

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

901 
 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

902 
 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

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

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

905 

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

906 
lemma eq_pred_code [code]: 
31133  907 
fixes P Q :: "'a pred" 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

908 
shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

909 
by (auto simp add: equal) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

910 

97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

911 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

912 
"HOL.equal (x :: 'a pred) x \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38651
diff
changeset

913 
by (fact equal_refl) 
30430
42ea5d85edcc
explicit code equations for some rarely used pred operations
haftmann
parents:
30378
diff
changeset

914 

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

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

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

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

918 

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

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

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

921 
by (cases P) simp 
30328  922 

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

923 
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

924 

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

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

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

930 

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

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

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

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

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

935 

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

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

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

938 
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

939 

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

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

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

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

943 

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

946 
 "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  947 
 "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P 
948 
else let x = singleton dfault P; y = the_only dfault xq in 

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

950 

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

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

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

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

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

956 

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

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

960 
 Insert x P \<Rightarrow> if is_empty P then x 
33110  961 
else let y = singleton dfault P in 
33111  962 
if x = y then x else dfault () 
33110  963 
 Join P xq \<Rightarrow> if is_empty P then the_only dfault xq 
964 
else if null xq then singleton dfault P 

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

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

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

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

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

970 

33110  971 
definition not_unique :: "'a pred => 'a" 
972 
where 

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

33111  975 
definition the :: "'a pred => 'a" 
976 
where 

37767  977 
"the A = (THE x. eval A x)" 
33111  978 

40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

979 
lemma the_eqI: 
41080  980 
"(THE x. eval P x) = x \<Longrightarrow> the P = x" 
40674
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

981 
by (simp add: the_def) 
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

982 

54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

983 
lemma the_eq [code]: "the A = singleton (\<lambda>x. not_unique A) A" 
54dbe6a1c349
adhere established Collect/mem convention more closely
haftmann
parents:
40616
diff
changeset

984 
by (rule the_eqI) (simp add: singleton_def not_unique_def) 
33110  985 

33988  986 
code_abort not_unique 
987 

36531
19f6e3b0d9b6
code_reflect: specify module name directly after keyword
haftmann
parents:
36513
diff
changeset

988 
code_reflect Predicate 
36513  989 
datatypes pred = Seq and seq = Empty  Insert  Join 
990 
functions map 

991 

30948  992 
ML {* 
993 
signature PREDICATE = 

994 
sig 

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

996 
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

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

998 
val yieldn: int > 'a pred > 'a list * 'a pred 
31222  999 
val map: ('a > 'b) > 'a pred > 'b pred 
30948  1000 
end; 
1001 

1002 
structure Predicate : PREDICATE = 

1003 
struct 

1004 

36513  1005 
datatype pred = datatype Predicate.pred 
1006 
datatype seq = datatype Predicate.seq 

1007 

1008 
fun map f = Predicate.map f; 

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

1009 

36513  1010 
fun yield (Seq f) = next (f ()) 
1011 
and next Empty = NONE 

1012 
 next (Insert (x, P)) = SOME (x, P) 

1013 
 next (Join (P, xq)) = (case yield P 

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

1014 
of NONE => next xq 
36513  1015 
 SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq)))); 
30959
458e55fd0a33
fixed compilation of predicate types in ML environment
haftmann
parents:
30948
diff
changeset

1016 

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

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

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

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

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

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

1023 

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

1024 
fun yieldn P = anamorph yield P; 
30948  1025 

1026 
end; 

1027 
*} 

1028 

30328  1029 
no_notation 
1030 
inf (infixl "\<sqinter>" 70) and 

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

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

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

1034 
top ("\<top>") and 

1035 
bot ("\<bottom>") and 

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

1037 

41080  1038 
no_syntax (xsymbols) 
1039 
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) 

1040 
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) 

1041 
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) 

1042 
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) 

1043 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36008
diff
changeset

1044 
hide_type (open) pred seq 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36008
diff
changeset

1045 
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds 
33111  1046 
Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the 
30328  1047 

1048 
end 