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