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