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