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;
     1 (*  Author:     Andreas Lochbihler *)
     2 
     3 section \<open>Predicates modelled as FinFuns\<close>
     4 
     5 theory FinFunPred
     6 imports "~~/src/HOL/Library/FinFun"
     7 begin
     8 
     9 unbundle finfun_syntax
    10 
    11 text \<open>Instantiate FinFun predicates just like predicates\<close>
    12 
    13 type_synonym 'a pred\<^sub>f = "'a \<Rightarrow>f bool"
    14 
    15 instantiation "finfun" :: (type, ord) ord
    16 begin
    17 
    18 definition le_finfun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f $ x \<le> g $ x)"
    19 
    20 definition [code del]: "(f::'a \<Rightarrow>f 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> g \<le> f"
    21 
    22 instance ..
    23 
    24 lemma le_finfun_code [code]:
    25   "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ ($f, g$))"
    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 
    36 instantiation "finfun" :: (type, order_bot) order_bot begin
    37 definition "bot = finfun_const bot"
    38 instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
    39 end
    40 
    41 lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
    42 by(auto simp add: bot_finfun_def)
    43 
    44 instantiation "finfun" :: (type, order_top) order_top begin
    45 definition "top = finfun_const top"
    46 instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
    47 end
    48 
    49 lemma top_finfun_apply [simp]: "op $ top = (\<lambda>_. top)"
    50 by(auto simp add: top_finfun_def)
    51 
    52 instantiation "finfun" :: (type, inf) inf begin
    53 definition [code]: "inf f g = (\<lambda>(x, y). inf x y) \<circ>$ ($f, g$)"
    54 instance ..
    55 end
    56 
    57 lemma inf_finfun_apply [simp]: "op $ (inf f g) = inf (op $ f) (op $ g)"
    58 by(auto simp add: inf_finfun_def o_def inf_fun_def)
    59 
    60 instantiation "finfun" :: (type, sup) sup begin
    61 definition [code]: "sup f g = (\<lambda>(x, y). sup x y) \<circ>$ ($f, g$)"
    62 instance ..
    63 end
    64 
    65 lemma sup_finfun_apply [simp]: "op $ (sup f g) = sup (op $ f) (op $ g)"
    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
    83 definition "f - g = case_prod (op -) \<circ>$ ($f, g$)"
    84 instance ..
    85 end
    86 
    87 lemma minus_finfun_apply [simp]: "op $ (f - g) = op $ f - op $ g"
    88 by(simp add: minus_finfun_def o_def fun_diff_def)
    89 
    90 instantiation "finfun" :: (type, uminus) uminus begin
    91 definition "- A = uminus \<circ>$ A"
    92 instance ..
    93 end
    94 
    95 lemma uminus_finfun_apply [simp]: "op $ (- g) = - op $ g"
    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 
   102 text \<open>
   103   Replicate predicate operations for FinFuns
   104 \<close>
   105 
   106 abbreviation finfun_empty :: "'a pred\<^sub>f" ("{}\<^sub>f")
   107 where "{}\<^sub>f \<equiv> bot"
   108 
   109 abbreviation finfun_UNIV :: "'a pred\<^sub>f" 
   110 where "finfun_UNIV \<equiv> top"
   111 
   112 definition finfun_single :: "'a \<Rightarrow> 'a pred\<^sub>f"
   113 where [code]: "finfun_single x = finfun_empty(x $:= True)"
   114 
   115 lemma finfun_single_apply [simp]:
   116   "finfun_single x $ y \<longleftrightarrow> x = y"
   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 
   124 lemma finfun_leI [intro!]: "(!!x. A $ x \<Longrightarrow> B $ x) \<Longrightarrow> A \<le> B"
   125 by(simp add: le_finfun_def)
   126 
   127 lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A $ x \<rbrakk> \<Longrightarrow> B $ x"
   128 by(simp add: le_finfun_def)
   129 
   130 text \<open>Bounded quantification.
   131   Warning: \<open>finfun_Ball\<close> and \<open>finfun_Ex\<close> may raise an exception, they should not be used for quickcheck
   132 \<close>
   133 
   134 definition finfun_Ball_except :: "'a list \<Rightarrow> 'a pred\<^sub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   135 where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A $ a \<longrightarrow> a \<in> set xs \<or> P a)"
   136 
   137 lemma finfun_Ball_except_const:
   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)"
   139 by(auto simp add: finfun_Ball_except_def)
   140 
   141 lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
   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)"
   143 by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff)
   144 
   145 lemma finfun_Ball_except_update:
   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)"
   147 by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: if_split_asm)
   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 
   154 definition finfun_Ball :: "'a pred\<^sub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   155 where [code del]: "finfun_Ball A P = Ball {x. A $ x} P"
   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 
   161 definition finfun_Bex_except :: "'a list \<Rightarrow> 'a pred\<^sub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   162 where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A $ a \<and> a \<notin> set xs \<and> P a)"
   163 
   164 lemma finfun_Bex_except_const:
   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)"
   166 by(auto simp add: finfun_Bex_except_def)
   167 
   168 lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
   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)"
   170 by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff)
   171 
   172 lemma finfun_Bex_except_update: 
   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"
   174 by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: if_split_asm)
   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 
   181 definition finfun_Bex :: "'a pred\<^sub>f \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   182 where [code del]: "finfun_Bex A P = Bex {x. A $ x} P"
   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 
   188 text \<open>Automatically replace predicate operations by finfun predicate operations where possible\<close>
   189 
   190 lemma iso_finfun_le [code_unfold]:
   191   "op $ A \<le> op $ B \<longleftrightarrow> A \<le> B"
   192 by (metis le_finfun_def le_funD le_funI)
   193 
   194 lemma iso_finfun_less [code_unfold]:
   195   "op $ A < op $ B \<longleftrightarrow> A < B"
   196 by (metis iso_finfun_le less_finfun_def less_fun_def)
   197 
   198 lemma iso_finfun_eq [code_unfold]:
   199   "op $ A = op $ B \<longleftrightarrow> A = B"
   200 by(simp only: expand_finfun_eq)
   201 
   202 lemma iso_finfun_sup [code_unfold]:
   203   "sup (op $ A) (op $ B) = op $ (sup A B)"
   204 by(simp)
   205 
   206 lemma iso_finfun_disj [code_unfold]:
   207   "A $ x \<or> B $ x \<longleftrightarrow> sup A B $ x"
   208 by(simp add: sup_fun_def)
   209 
   210 lemma iso_finfun_inf [code_unfold]:
   211   "inf (op $ A) (op $ B) = op $ (inf A B)"
   212 by(simp)
   213 
   214 lemma iso_finfun_conj [code_unfold]:
   215   "A $ x \<and> B $ x \<longleftrightarrow> inf A B $ x"
   216 by(simp add: inf_fun_def)
   217 
   218 lemma iso_finfun_empty_conv [code_unfold]:
   219   "(\<lambda>_. False) = op $ {}\<^sub>f"
   220 by simp
   221 
   222 lemma iso_finfun_UNIV_conv [code_unfold]:
   223   "(\<lambda>_. True) = op $ finfun_UNIV"
   224 by simp
   225 
   226 lemma iso_finfun_upd [code_unfold]:
   227   fixes A :: "'a pred\<^sub>f"
   228   shows "(op $ A)(x := b) = op $ (A(x $:= b))"
   229 by(simp add: fun_eq_iff)
   230 
   231 lemma iso_finfun_uminus [code_unfold]:
   232   fixes A :: "'a pred\<^sub>f"
   233   shows "- op $ A = op $ (- A)"
   234 by(simp)
   235 
   236 lemma iso_finfun_minus [code_unfold]:
   237   fixes A :: "'a pred\<^sub>f"
   238   shows "op $ A - op $ B = op $ (A - B)"
   239 by(simp)
   240 
   241 text \<open>
   242   Do not declare the following two theorems as \<open>[code_unfold]\<close>,
   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.
   245 \<close>
   246 
   247 lemma iso_finfun_Ball_Ball:
   248   "(\<forall>x. A $ x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
   249 by(simp add: finfun_Ball_def)
   250 
   251 lemma iso_finfun_Bex_Bex:
   252   "(\<exists>x. A $ x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
   253 by(simp add: finfun_Bex_def)
   254 
   255 text \<open>Test code setup\<close>
   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 
   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 
   270 end