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