author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 48059 | f6ce99d3719b |
child 52729 | 412c9e0381a1 |
permissions | -rw-r--r-- |
48028 | 1 |
(* Author: Andreas Lochbihler *) |
2 |
||
3 |
header {* |
|
4 |
Predicates modelled as FinFuns |
|
5 |
*} |
|
6 |
||
48041
d60f6b41bf2d
remove pretty syntax for FinFuns at the end and provide separate syntax theory
Andreas Lochbihler
parents:
48038
diff
changeset
|
7 |
theory FinFunPred imports "~~/src/HOL/Library/FinFun_Syntax" begin |
48028 | 8 |
|
9 |
text {* Instantiate FinFun predicates just like predicates *} |
|
10 |
||
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48029
diff
changeset
|
11 |
type_synonym 'a pred\<^isub>f = "'a \<Rightarrow>f bool" |
48028 | 12 |
|
13 |
instantiation "finfun" :: (type, ord) ord |
|
14 |
begin |
|
15 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
16 |
definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)" |
48028 | 17 |
|
48034
1c5171abe5cc
removed subscripts from FinFun type syntax
Andreas Lochbihler
parents:
48029
diff
changeset
|
18 |
definition [code del]: "(f\<Colon>'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> f \<ge> g" |
48028 | 19 |
|
20 |
instance .. |
|
21 |
||
22 |
lemma le_finfun_code [code]: |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
23 |
"f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ ($f, g$))" |
48028 | 24 |
by(simp add: le_finfun_def finfun_All_All o_def) |
25 |
||
26 |
end |
|
27 |
||
28 |
instance "finfun" :: (type, preorder) preorder |
|
29 |
by(intro_classes)(auto simp add: less_finfun_def le_finfun_def intro: order_trans) |
|
30 |
||
31 |
instance "finfun" :: (type, order) order |
|
32 |
by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext) |
|
33 |
||
34 |
instantiation "finfun" :: (type, bot) bot begin |
|
35 |
definition "bot = finfun_const bot" |
|
36 |
instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def) |
|
37 |
end |
|
38 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
39 |
lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)" |
48028 | 40 |
by(auto simp add: bot_finfun_def) |
41 |
||
42 |
instantiation "finfun" :: (type, top) top begin |
|
43 |
definition "top = finfun_const top" |
|
44 |
instance by(intro_classes)(simp add: top_finfun_def le_finfun_def) |
|
45 |
end |
|
46 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
47 |
lemma top_finfun_apply [simp]: "op $ top = (\<lambda>_. top)" |
48028 | 48 |
by(auto simp add: top_finfun_def) |
49 |
||
50 |
instantiation "finfun" :: (type, inf) inf begin |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
51 |
definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ ($f, g$)" |
48028 | 52 |
instance .. |
53 |
end |
|
54 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
55 |
lemma inf_finfun_apply [simp]: "op $ (inf f g) = inf (op $ f) (op $ g)" |
48028 | 56 |
by(auto simp add: inf_finfun_def o_def inf_fun_def) |
57 |
||
58 |
instantiation "finfun" :: (type, sup) sup begin |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
59 |
definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ ($f, g$)" |
48028 | 60 |
instance .. |
61 |
end |
|
62 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
63 |
lemma sup_finfun_apply [simp]: "op $ (sup f g) = sup (op $ f) (op $ g)" |
48028 | 64 |
by(auto simp add: sup_finfun_def o_def sup_fun_def) |
65 |
||
66 |
instance "finfun" :: (type, semilattice_inf) semilattice_inf |
|
67 |
by(intro_classes)(simp_all add: inf_finfun_def le_finfun_def) |
|
68 |
||
69 |
instance "finfun" :: (type, semilattice_sup) semilattice_sup |
|
70 |
by(intro_classes)(simp_all add: sup_finfun_def le_finfun_def) |
|
71 |
||
72 |
instance "finfun" :: (type, lattice) lattice .. |
|
73 |
||
74 |
instance "finfun" :: (type, bounded_lattice) bounded_lattice |
|
75 |
by(intro_classes) |
|
76 |
||
77 |
instance "finfun" :: (type, distrib_lattice) distrib_lattice |
|
78 |
by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1) |
|
79 |
||
80 |
instantiation "finfun" :: (type, minus) minus begin |
|
48038
72a8506dd59b
eliminated remaining sub- and superscripts in FinFun syntax
Andreas Lochbihler
parents:
48037
diff
changeset
|
81 |
definition "f - g = split (op -) \<circ>$ ($f, g$)" |
48028 | 82 |
instance .. |
83 |
end |
|
84 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
85 |
lemma minus_finfun_apply [simp]: "op $ (f - g) = op $ f - op $ g" |
48028 | 86 |
by(simp add: minus_finfun_def o_def fun_diff_def) |
87 |
||
88 |
instantiation "finfun" :: (type, uminus) uminus begin |
|
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
89 |
definition "- A = uminus \<circ>$ A" |
48028 | 90 |
instance .. |
91 |
end |
|
92 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
93 |
lemma uminus_finfun_apply [simp]: "op $ (- g) = - op $ g" |
48028 | 94 |
by(simp add: uminus_finfun_def o_def fun_Compl_def) |
95 |
||
96 |
instance "finfun" :: (type, boolean_algebra) boolean_algebra |
|
97 |
by(intro_classes) |
|
98 |
(simp_all add: uminus_finfun_def inf_finfun_def expand_finfun_eq sup_fun_def inf_fun_def fun_Compl_def o_def inf_compl_bot sup_compl_top diff_eq) |
|
99 |
||
100 |
text {* |
|
101 |
Replicate predicate operations for FinFuns |
|
102 |
*} |
|
103 |
||
104 |
abbreviation finfun_empty :: "'a pred\<^isub>f" ("{}\<^isub>f") |
|
105 |
where "{}\<^isub>f \<equiv> bot" |
|
106 |
||
107 |
abbreviation finfun_UNIV :: "'a pred\<^isub>f" |
|
108 |
where "finfun_UNIV \<equiv> top" |
|
109 |
||
110 |
definition finfun_single :: "'a \<Rightarrow> 'a pred\<^isub>f" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
111 |
where [code]: "finfun_single x = finfun_empty(x $:= True)" |
48028 | 112 |
|
113 |
lemma finfun_single_apply [simp]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
114 |
"finfun_single x $ y \<longleftrightarrow> x = y" |
48028 | 115 |
by(simp add: finfun_single_def finfun_upd_apply) |
116 |
||
117 |
lemma [iff]: |
|
118 |
shows finfun_single_neq_bot: "finfun_single x \<noteq> bot" |
|
119 |
and bot_neq_finfun_single: "bot \<noteq> finfun_single x" |
|
120 |
by(simp_all add: expand_finfun_eq fun_eq_iff) |
|
121 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
122 |
lemma finfun_leI [intro!]: "(!!x. A $ x \<Longrightarrow> B $ x) \<Longrightarrow> A \<le> B" |
48028 | 123 |
by(simp add: le_finfun_def) |
124 |
||
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
125 |
lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A $ x \<rbrakk> \<Longrightarrow> B $ x" |
48028 | 126 |
by(simp add: le_finfun_def) |
127 |
||
128 |
text {* Bounded quantification. |
|
129 |
Warning: @{text "finfun_Ball"} and @{text "finfun_Ex"} may raise an exception, they should not be used for quickcheck |
|
130 |
*} |
|
131 |
||
132 |
definition finfun_Ball_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
133 |
where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A $ a \<longrightarrow> a \<in> set xs \<or> P a)" |
48028 | 134 |
|
135 |
lemma finfun_Ball_except_const: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
136 |
"finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)" |
48028 | 137 |
by(auto simp add: finfun_Ball_except_def) |
138 |
||
139 |
lemma finfun_Ball_except_const_finfun_UNIV_code [code]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
140 |
"finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)" |
48028 | 141 |
by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff) |
142 |
||
143 |
lemma finfun_Ball_except_update: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
144 |
"finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)" |
48028 | 145 |
by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: split_if_asm) |
146 |
||
147 |
lemma finfun_Ball_except_update_code [code]: |
|
148 |
fixes a :: "'a :: card_UNIV" |
|
149 |
shows "finfun_Ball_except xs (finfun_update_code f a b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) f P)" |
|
150 |
by(simp add: finfun_Ball_except_update) |
|
151 |
||
152 |
definition finfun_Ball :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
153 |
where [code del]: "finfun_Ball A P = Ball {x. A $ x} P" |
48028 | 154 |
|
155 |
lemma finfun_Ball_code [code]: "finfun_Ball = finfun_Ball_except []" |
|
156 |
by(auto intro!: ext simp add: finfun_Ball_except_def finfun_Ball_def) |
|
157 |
||
158 |
||
159 |
definition finfun_Bex_except :: "'a list \<Rightarrow> 'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
160 |
where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A $ a \<and> a \<notin> set xs \<and> P a)" |
48028 | 161 |
|
162 |
lemma finfun_Bex_except_const: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
163 |
"finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)" |
48028 | 164 |
by(auto simp add: finfun_Bex_except_def) |
165 |
||
166 |
lemma finfun_Bex_except_const_finfun_UNIV_code [code]: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
167 |
"finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)" |
48028 | 168 |
by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff) |
169 |
||
170 |
lemma finfun_Bex_except_update: |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
171 |
"finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P" |
48028 | 172 |
by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: split_if_asm) |
173 |
||
174 |
lemma finfun_Bex_except_update_code [code]: |
|
175 |
fixes a :: "'a :: card_UNIV" |
|
176 |
shows "finfun_Bex_except xs (finfun_update_code f a b) P \<longleftrightarrow> ((a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) f P)" |
|
177 |
by(simp add: finfun_Bex_except_update) |
|
178 |
||
179 |
definition finfun_Bex :: "'a pred\<^isub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
180 |
where [code del]: "finfun_Bex A P = Bex {x. A $ x} P" |
48028 | 181 |
|
182 |
lemma finfun_Bex_code [code]: "finfun_Bex = finfun_Bex_except []" |
|
183 |
by(auto intro!: ext simp add: finfun_Bex_except_def finfun_Bex_def) |
|
184 |
||
185 |
||
186 |
text {* Automatically replace predicate operations by finfun predicate operations where possible *} |
|
187 |
||
188 |
lemma iso_finfun_le [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
189 |
"op $ A \<le> op $ B \<longleftrightarrow> A \<le> B" |
48028 | 190 |
by (metis le_finfun_def le_funD le_funI) |
191 |
||
192 |
lemma iso_finfun_less [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
193 |
"op $ A < op $ B \<longleftrightarrow> A < B" |
48028 | 194 |
by (metis iso_finfun_le less_finfun_def less_fun_def) |
195 |
||
196 |
lemma iso_finfun_eq [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
197 |
"op $ A = op $ B \<longleftrightarrow> A = B" |
48029 | 198 |
by(simp only: expand_finfun_eq) |
48028 | 199 |
|
200 |
lemma iso_finfun_sup [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
201 |
"sup (op $ A) (op $ B) = op $ (sup A B)" |
48028 | 202 |
by(simp) |
203 |
||
204 |
lemma iso_finfun_disj [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
205 |
"A $ x \<or> B $ x \<longleftrightarrow> sup A B $ x" |
48028 | 206 |
by(simp add: sup_fun_def) |
207 |
||
208 |
lemma iso_finfun_inf [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
209 |
"inf (op $ A) (op $ B) = op $ (inf A B)" |
48028 | 210 |
by(simp) |
211 |
||
212 |
lemma iso_finfun_conj [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
213 |
"A $ x \<and> B $ x \<longleftrightarrow> inf A B $ x" |
48028 | 214 |
by(simp add: inf_fun_def) |
215 |
||
216 |
lemma iso_finfun_empty_conv [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
217 |
"(\<lambda>_. False) = op $ {}\<^isub>f" |
48028 | 218 |
by simp |
219 |
||
220 |
lemma iso_finfun_UNIV_conv [code_unfold]: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
221 |
"(\<lambda>_. True) = op $ finfun_UNIV" |
48028 | 222 |
by simp |
223 |
||
224 |
lemma iso_finfun_upd [code_unfold]: |
|
225 |
fixes A :: "'a pred\<^isub>f" |
|
48036
1edcd5f73505
FinFun pseudo-constructor syntax without superscripts
Andreas Lochbihler
parents:
48035
diff
changeset
|
226 |
shows "(op $ A)(x := b) = op $ (A(x $:= b))" |
48028 | 227 |
by(simp add: fun_eq_iff) |
228 |
||
229 |
lemma iso_finfun_uminus [code_unfold]: |
|
230 |
fixes A :: "'a pred\<^isub>f" |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
231 |
shows "- op $ A = op $ (- A)" |
48028 | 232 |
by(simp) |
233 |
||
234 |
lemma iso_finfun_minus [code_unfold]: |
|
235 |
fixes A :: "'a pred\<^isub>f" |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
236 |
shows "op $ A - op $ B = op $ (A - B)" |
48028 | 237 |
by(simp) |
238 |
||
239 |
text {* |
|
240 |
Do not declare the following two theorems as @{text "[code_unfold]"}, |
|
241 |
because this causes quickcheck to fail frequently when bounded quantification is used which raises an exception. |
|
242 |
For code generation, the same problems occur, but then, no randomly generated FinFun is usually around. |
|
243 |
*} |
|
244 |
||
245 |
lemma iso_finfun_Ball_Ball: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
246 |
"(\<forall>x. A $ x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P" |
48028 | 247 |
by(simp add: finfun_Ball_def) |
248 |
||
249 |
lemma iso_finfun_Bex_Bex: |
|
48035
2f9584581cf2
replace FinFun application syntax with $
Andreas Lochbihler
parents:
48034
diff
changeset
|
250 |
"(\<exists>x. A $ x \<and> P x) \<longleftrightarrow> finfun_Bex A P" |
48028 | 251 |
by(simp add: finfun_Bex_def) |
252 |
||
48037
6c4b3e78f03e
syntax for FinFun composition without subscripts
Andreas Lochbihler
parents:
48036
diff
changeset
|
253 |
text {* Test code setup *} |
48028 | 254 |
|
255 |
notepad begin |
|
256 |
have "inf ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) ((\<lambda>_. True)(3 := False)) \<le> |
|
257 |
sup ((\<lambda>_. False)(1 := True, 5 := True)) (- ((\<lambda>_. True)(2 := False, 3 := False)))" |
|
258 |
by eval |
|
259 |
end |
|
260 |
||
48059 | 261 |
declare iso_finfun_Ball_Ball[code_unfold] |
262 |
notepad begin |
|
263 |
have "(\<forall>x. ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) x \<longrightarrow> x < 3)" |
|
264 |
by eval |
|
265 |
end |
|
266 |
declare iso_finfun_Ball_Ball[code_unfold del] |
|
267 |
||
48028 | 268 |
end |