1(* Title: HOL/Partial_Function.thy 2 Author: Alexander Krauss, TU Muenchen 3*) 4 5section \<open>Partial Function Definitions\<close> 6 7theory Partial_Function 8 imports Complete_Partial_Order Option 9 keywords "partial_function" :: thy_defn 10begin 11 12named_theorems partial_function_mono "monotonicity rules for partial function definitions" 13ML_file \<open>Tools/Function/partial_function.ML\<close> 14 15lemma (in ccpo) in_chain_finite: 16 assumes "Complete_Partial_Order.chain (\<le>) A" "finite A" "A \<noteq> {}" 17 shows "\<Squnion>A \<in> A" 18using assms(2,1,3) 19proof induction 20 case empty thus ?case by simp 21next 22 case (insert x A) 23 note chain = \<open>Complete_Partial_Order.chain (\<le>) (insert x A)\<close> 24 show ?case 25 proof(cases "A = {}") 26 case True thus ?thesis by simp 27 next 28 case False 29 from chain have chain': "Complete_Partial_Order.chain (\<le>) A" 30 by(rule chain_subset) blast 31 hence "\<Squnion>A \<in> A" using False by(rule insert.IH) 32 show ?thesis 33 proof(cases "x \<le> \<Squnion>A") 34 case True 35 have "\<Squnion>(insert x A) \<le> \<Squnion>A" using chain 36 by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain']) 37 hence "\<Squnion>(insert x A) = \<Squnion>A" 38 by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain']) 39 with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp 40 next 41 case False 42 with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close> 43 have "\<Squnion>(insert x A) = x" 44 by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain]) 45 thus ?thesis by simp 46 qed 47 qed 48qed 49 50lemma (in ccpo) admissible_chfin: 51 "(\<forall>S. Complete_Partial_Order.chain (\<le>) S \<longrightarrow> finite S) 52 \<Longrightarrow> ccpo.admissible Sup (\<le>) P" 53using in_chain_finite by (blast intro: ccpo.admissibleI) 54 55subsection \<open>Axiomatic setup\<close> 56 57text \<open>This techical locale constains the requirements for function 58 definitions with ccpo fixed points.\<close> 59 60definition "fun_ord ord f g \<longleftrightarrow> (\<forall>x. ord (f x) (g x))" 61definition "fun_lub L A = (\<lambda>x. L {y. \<exists>f\<in>A. y = f x})" 62definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))" 63definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))" 64 65lemma chain_fun: 66 assumes A: "chain (fun_ord ord) A" 67 shows "chain ord {y. \<exists>f\<in>A. y = f a}" (is "chain ord ?C") 68proof (rule chainI) 69 fix x y assume "x \<in> ?C" "y \<in> ?C" 70 then obtain f g where fg: "f \<in> A" "g \<in> A" 71 and [simp]: "x = f a" "y = g a" by blast 72 from chainD[OF A fg] 73 show "ord x y \<or> ord y x" unfolding fun_ord_def by auto 74qed 75 76lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)" 77by (rule monotoneI) (auto simp: fun_ord_def) 78 79lemma let_mono[partial_function_mono]: 80 "(\<And>x. monotone orda ordb (\<lambda>f. b f x)) 81 \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))" 82by (simp add: Let_def) 83 84lemma if_mono[partial_function_mono]: "monotone orda ordb F 85\<Longrightarrow> monotone orda ordb G 86\<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)" 87unfolding monotone_def by simp 88 89definition "mk_less R = (\<lambda>x y. R x y \<and> \<not> R y x)" 90 91locale partial_function_definitions = 92 fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 93 fixes lub :: "'a set \<Rightarrow> 'a" 94 assumes leq_refl: "leq x x" 95 assumes leq_trans: "leq x y \<Longrightarrow> leq y z \<Longrightarrow> leq x z" 96 assumes leq_antisym: "leq x y \<Longrightarrow> leq y x \<Longrightarrow> x = y" 97 assumes lub_upper: "chain leq A \<Longrightarrow> x \<in> A \<Longrightarrow> leq x (lub A)" 98 assumes lub_least: "chain leq A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> leq x z) \<Longrightarrow> leq (lub A) z" 99 100lemma partial_function_lift: 101 assumes "partial_function_definitions ord lb" 102 shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf") 103proof - 104 interpret partial_function_definitions ord lb by fact 105 106 show ?thesis 107 proof 108 fix x show "?ordf x x" 109 unfolding fun_ord_def by (auto simp: leq_refl) 110 next 111 fix x y z assume "?ordf x y" "?ordf y z" 112 thus "?ordf x z" unfolding fun_ord_def 113 by (force dest: leq_trans) 114 next 115 fix x y assume "?ordf x y" "?ordf y x" 116 thus "x = y" unfolding fun_ord_def 117 by (force intro!: dest: leq_antisym) 118 next 119 fix A f assume f: "f \<in> A" and A: "chain ?ordf A" 120 thus "?ordf f (?lubf A)" 121 unfolding fun_lub_def fun_ord_def 122 by (blast intro: lub_upper chain_fun[OF A] f) 123 next 124 fix A :: "('b \<Rightarrow> 'a) set" and g :: "'b \<Rightarrow> 'a" 125 assume A: "chain ?ordf A" and g: "\<And>f. f \<in> A \<Longrightarrow> ?ordf f g" 126 show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def 127 by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def]) 128 qed 129qed 130 131lemma ccpo: assumes "partial_function_definitions ord lb" 132 shows "class.ccpo lb ord (mk_less ord)" 133using assms unfolding partial_function_definitions_def mk_less_def 134by unfold_locales blast+ 135 136lemma partial_function_image: 137 assumes "partial_function_definitions ord Lub" 138 assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" 139 assumes inv: "\<And>x. f (g x) = x" 140 shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)" 141proof - 142 let ?iord = "img_ord f ord" 143 let ?ilub = "img_lub f g Lub" 144 145 interpret partial_function_definitions ord Lub by fact 146 show ?thesis 147 proof 148 fix A x assume "chain ?iord A" "x \<in> A" 149 then have "chain ord (f ` A)" "f x \<in> f ` A" 150 by (auto simp: img_ord_def intro: chainI dest: chainD) 151 thus "?iord x (?ilub A)" 152 unfolding inv img_lub_def img_ord_def by (rule lub_upper) 153 next 154 fix A x assume "chain ?iord A" 155 and 1: "\<And>z. z \<in> A \<Longrightarrow> ?iord z x" 156 then have "chain ord (f ` A)" 157 by (auto simp: img_ord_def intro: chainI dest: chainD) 158 thus "?iord (?ilub A) x" 159 unfolding inv img_lub_def img_ord_def 160 by (rule lub_least) (auto dest: 1[unfolded img_ord_def]) 161 qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj) 162qed 163 164context partial_function_definitions 165begin 166 167abbreviation "le_fun \<equiv> fun_ord leq" 168abbreviation "lub_fun \<equiv> fun_lub lub" 169abbreviation "fixp_fun \<equiv> ccpo.fixp lub_fun le_fun" 170abbreviation "mono_body \<equiv> monotone le_fun leq" 171abbreviation "admissible \<equiv> ccpo.admissible lub_fun le_fun" 172 173text \<open>Interpret manually, to avoid flooding everything with facts about 174 orders\<close> 175 176lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)" 177apply (rule ccpo) 178apply (rule partial_function_lift) 179apply (rule partial_function_definitions_axioms) 180done 181 182text \<open>The crucial fixed-point theorem\<close> 183 184lemma mono_body_fixp: 185 "(\<And>x. mono_body (\<lambda>f. F f x)) \<Longrightarrow> fixp_fun F = F (fixp_fun F)" 186by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def) 187 188text \<open>Version with curry/uncurry combinators, to be used by package\<close> 189 190lemma fixp_rule_uc: 191 fixes F :: "'c \<Rightarrow> 'c" and 192 U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and 193 C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" 194 assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" 195 assumes eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" 196 assumes inverse: "\<And>f. C (U f) = f" 197 shows "f = F f" 198proof - 199 have "f = C (fixp_fun (\<lambda>f. U (F (C f))))" by (simp add: eq) 200 also have "... = C (U (F (C (fixp_fun (\<lambda>f. U (F (C f)))))))" 201 by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl) 202 also have "... = F (C (fixp_fun (\<lambda>f. U (F (C f)))))" by (rule inverse) 203 also have "... = F f" by (simp add: eq) 204 finally show "f = F f" . 205qed 206 207text \<open>Fixpoint induction rule\<close> 208 209lemma fixp_induct_uc: 210 fixes F :: "'c \<Rightarrow> 'c" 211 and U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" 212 and C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" 213 and P :: "('b \<Rightarrow> 'a) \<Rightarrow> bool" 214 assumes mono: "\<And>x. mono_body (\<lambda>f. U (F (C f)) x)" 215 and eq: "f \<equiv> C (fixp_fun (\<lambda>f. U (F (C f))))" 216 and inverse: "\<And>f. U (C f) = f" 217 and adm: "ccpo.admissible lub_fun le_fun P" 218 and bot: "P (\<lambda>_. lub {})" 219 and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))" 220 shows "P (U f)" 221unfolding eq inverse 222apply (rule ccpo.fixp_induct[OF ccpo adm]) 223apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2] 224apply (rule_tac f5="C x" in step) 225apply (simp add: inverse) 226done 227 228 229text \<open>Rules for \<^term>\<open>mono_body\<close>:\<close> 230 231lemma const_mono[partial_function_mono]: "monotone ord leq (\<lambda>f. c)" 232by (rule monotoneI) (rule leq_refl) 233 234end 235 236 237subsection \<open>Flat interpretation: tailrec and option\<close> 238 239definition 240 "flat_ord b x y \<longleftrightarrow> x = b \<or> x = y" 241 242definition 243 "flat_lub b A = (if A \<subseteq> {b} then b else (THE x. x \<in> A - {b}))" 244 245lemma flat_interpretation: 246 "partial_function_definitions (flat_ord b) (flat_lub b)" 247proof 248 fix A x assume 1: "chain (flat_ord b) A" "x \<in> A" 249 show "flat_ord b x (flat_lub b A)" 250 proof cases 251 assume "x = b" 252 thus ?thesis by (simp add: flat_ord_def) 253 next 254 assume "x \<noteq> b" 255 with 1 have "A - {b} = {x}" 256 by (auto elim: chainE simp: flat_ord_def) 257 then have "flat_lub b A = x" 258 by (auto simp: flat_lub_def) 259 thus ?thesis by (auto simp: flat_ord_def) 260 qed 261next 262 fix A z assume A: "chain (flat_ord b) A" 263 and z: "\<And>x. x \<in> A \<Longrightarrow> flat_ord b x z" 264 show "flat_ord b (flat_lub b A) z" 265 proof cases 266 assume "A \<subseteq> {b}" 267 thus ?thesis 268 by (auto simp: flat_lub_def flat_ord_def) 269 next 270 assume nb: "\<not> A \<subseteq> {b}" 271 then obtain y where y: "y \<in> A" "y \<noteq> b" by auto 272 with A have "A - {b} = {y}" 273 by (auto elim: chainE simp: flat_ord_def) 274 with nb have "flat_lub b A = y" 275 by (auto simp: flat_lub_def) 276 with z y show ?thesis by auto 277 qed 278qed (auto simp: flat_ord_def) 279 280lemma flat_ordI: "(x \<noteq> a \<Longrightarrow> x = y) \<Longrightarrow> flat_ord a x y" 281by(auto simp add: flat_ord_def) 282 283lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y" 284by(auto simp add: flat_ord_def) 285 286lemma antisymp_flat_ord: "antisymp (flat_ord a)" 287by(rule antisympI)(auto dest: flat_ord_antisym) 288 289interpretation tailrec: 290 partial_function_definitions "flat_ord undefined" "flat_lub undefined" 291 rewrites "flat_lub undefined {} \<equiv> undefined" 292by (rule flat_interpretation)(simp add: flat_lub_def) 293 294interpretation option: 295 partial_function_definitions "flat_ord None" "flat_lub None" 296 rewrites "flat_lub None {} \<equiv> None" 297by (rule flat_interpretation)(simp add: flat_lub_def) 298 299 300abbreviation "tailrec_ord \<equiv> flat_ord undefined" 301abbreviation "mono_tailrec \<equiv> monotone (fun_ord tailrec_ord) tailrec_ord" 302 303lemma tailrec_admissible: 304 "ccpo.admissible (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) 305 (\<lambda>a. \<forall>x. a x \<noteq> c \<longrightarrow> P x (a x))" 306proof(intro ccpo.admissibleI strip) 307 fix A x 308 assume chain: "Complete_Partial_Order.chain (fun_ord (flat_ord c)) A" 309 and P [rule_format]: "\<forall>f\<in>A. \<forall>x. f x \<noteq> c \<longrightarrow> P x (f x)" 310 and defined: "fun_lub (flat_lub c) A x \<noteq> c" 311 from defined obtain f where f: "f \<in> A" "f x \<noteq> c" 312 by(auto simp add: fun_lub_def flat_lub_def split: if_split_asm) 313 hence "P x (f x)" by(rule P) 314 moreover from chain f have "\<forall>f' \<in> A. f' x = c \<or> f' x = f x" 315 by(auto 4 4 simp add: Complete_Partial_Order.chain_def flat_ord_def fun_ord_def) 316 hence "fun_lub (flat_lub c) A x = f x" 317 using f by(auto simp add: fun_lub_def flat_lub_def) 318 ultimately show "P x (fun_lub (flat_lub c) A x)" by simp 319qed 320 321lemma fixp_induct_tailrec: 322 fixes F :: "'c \<Rightarrow> 'c" and 323 U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a" and 324 C :: "('b \<Rightarrow> 'a) \<Rightarrow> 'c" and 325 P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" and 326 x :: "'b" 327 assumes mono: "\<And>x. monotone (fun_ord (flat_ord c)) (flat_ord c) (\<lambda>f. U (F (C f)) x)" 328 assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub c)) (fun_ord (flat_ord c)) (\<lambda>f. U (F (C f))))" 329 assumes inverse2: "\<And>f. U (C f) = f" 330 assumes step: "\<And>f x y. (\<And>x y. U f x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = y \<Longrightarrow> y \<noteq> c \<Longrightarrow> P x y" 331 assumes result: "U f x = y" 332 assumes defined: "y \<noteq> c" 333 shows "P x y" 334proof - 335 have "\<forall>x y. U f x = y \<longrightarrow> y \<noteq> c \<longrightarrow> P x y" 336 by(rule partial_function_definitions.fixp_induct_uc[OF flat_interpretation, of _ U F C, OF mono eq inverse2]) 337 (auto intro: step tailrec_admissible simp add: fun_lub_def flat_lub_def) 338 thus ?thesis using result defined by blast 339qed 340 341lemma admissible_image: 342 assumes pfun: "partial_function_definitions le lub" 343 assumes adm: "ccpo.admissible lub le (P \<circ> g)" 344 assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" 345 assumes inv: "\<And>x. f (g x) = x" 346 shows "ccpo.admissible (img_lub f g lub) (img_ord f le) P" 347proof (rule ccpo.admissibleI) 348 fix A assume "chain (img_ord f le) A" 349 then have ch': "chain le (f ` A)" 350 by (auto simp: img_ord_def intro: chainI dest: chainD) 351 assume "A \<noteq> {}" 352 assume P_A: "\<forall>x\<in>A. P x" 353 have "(P \<circ> g) (lub (f ` A))" using adm ch' 354 proof (rule ccpo.admissibleD) 355 fix x assume "x \<in> f ` A" 356 with P_A show "(P \<circ> g) x" by (auto simp: inj[OF inv]) 357 qed(simp add: \<open>A \<noteq> {}\<close>) 358 thus "P (img_lub f g lub A)" unfolding img_lub_def by simp 359qed 360 361lemma admissible_fun: 362 assumes pfun: "partial_function_definitions le lub" 363 assumes adm: "\<And>x. ccpo.admissible lub le (Q x)" 364 shows "ccpo.admissible (fun_lub lub) (fun_ord le) (\<lambda>f. \<forall>x. Q x (f x))" 365proof (rule ccpo.admissibleI) 366 fix A :: "('b \<Rightarrow> 'a) set" 367 assume Q: "\<forall>f\<in>A. \<forall>x. Q x (f x)" 368 assume ch: "chain (fun_ord le) A" 369 assume "A \<noteq> {}" 370 hence non_empty: "\<And>a. {y. \<exists>f\<in>A. y = f a} \<noteq> {}" by auto 371 show "\<forall>x. Q x (fun_lub lub A x)" 372 unfolding fun_lub_def 373 by (rule allI, rule ccpo.admissibleD[OF adm chain_fun[OF ch] non_empty]) 374 (auto simp: Q) 375qed 376 377 378abbreviation "option_ord \<equiv> flat_ord None" 379abbreviation "mono_option \<equiv> monotone (fun_ord option_ord) option_ord" 380 381lemma bind_mono[partial_function_mono]: 382assumes mf: "mono_option B" and mg: "\<And>y. mono_option (\<lambda>f. C y f)" 383shows "mono_option (\<lambda>f. Option.bind (B f) (\<lambda>y. C y f))" 384proof (rule monotoneI) 385 fix f g :: "'a \<Rightarrow> 'b option" assume fg: "fun_ord option_ord f g" 386 with mf 387 have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g]) 388 then have "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y. C y f))" 389 unfolding flat_ord_def by auto 390 also from mg 391 have "\<And>y'. option_ord (C y' f) (C y' g)" 392 by (rule monotoneD) (rule fg) 393 then have "option_ord (Option.bind (B g) (\<lambda>y'. C y' f)) (Option.bind (B g) (\<lambda>y'. C y' g))" 394 unfolding flat_ord_def by (cases "B g") auto 395 finally (option.leq_trans) 396 show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" . 397qed 398 399lemma flat_lub_in_chain: 400 assumes ch: "chain (flat_ord b) A " 401 assumes lub: "flat_lub b A = a" 402 shows "a = b \<or> a \<in> A" 403proof (cases "A \<subseteq> {b}") 404 case True 405 then have "flat_lub b A = b" unfolding flat_lub_def by simp 406 with lub show ?thesis by simp 407next 408 case False 409 then obtain c where "c \<in> A" and "c \<noteq> b" by auto 410 { fix z assume "z \<in> A" 411 from chainD[OF ch \<open>c \<in> A\<close> this] have "z = c \<or> z = b" 412 unfolding flat_ord_def using \<open>c \<noteq> b\<close> by auto } 413 with False have "A - {b} = {c}" by auto 414 with False have "flat_lub b A = c" by (auto simp: flat_lub_def) 415 with \<open>c \<in> A\<close> lub show ?thesis by simp 416qed 417 418lemma option_admissible: "option.admissible (%(f::'a \<Rightarrow> 'b option). 419 (\<forall>x y. f x = Some y \<longrightarrow> P x y))" 420proof (rule ccpo.admissibleI) 421 fix A :: "('a \<Rightarrow> 'b option) set" 422 assume ch: "chain option.le_fun A" 423 and IH: "\<forall>f\<in>A. \<forall>x y. f x = Some y \<longrightarrow> P x y" 424 from ch have ch': "\<And>x. chain option_ord {y. \<exists>f\<in>A. y = f x}" by (rule chain_fun) 425 show "\<forall>x y. option.lub_fun A x = Some y \<longrightarrow> P x y" 426 proof (intro allI impI) 427 fix x y assume "option.lub_fun A x = Some y" 428 from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]] 429 have "Some y \<in> {y. \<exists>f\<in>A. y = f x}" by simp 430 then have "\<exists>f\<in>A. f x = Some y" by auto 431 with IH show "P x y" by auto 432 qed 433qed 434 435lemma fixp_induct_option: 436 fixes F :: "'c \<Rightarrow> 'c" and 437 U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a option" and 438 C :: "('b \<Rightarrow> 'a option) \<Rightarrow> 'c" and 439 P :: "'b \<Rightarrow> 'a \<Rightarrow> bool" 440 assumes mono: "\<And>x. mono_option (\<lambda>f. U (F (C f)) x)" 441 assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (\<lambda>f. U (F (C f))))" 442 assumes inverse2: "\<And>f. U (C f) = f" 443 assumes step: "\<And>f x y. (\<And>x y. U f x = Some y \<Longrightarrow> P x y) \<Longrightarrow> U (F f) x = Some y \<Longrightarrow> P x y" 444 assumes defined: "U f x = Some y" 445 shows "P x y" 446 using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible] 447 unfolding fun_lub_def flat_lub_def by(auto 9 2) 448 449declaration \<open>Partial_Function.init "tailrec" \<^term>\<open>tailrec.fixp_fun\<close> 450 \<^term>\<open>tailrec.mono_body\<close> @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc} 451 (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close> 452 453declaration \<open>Partial_Function.init "option" \<^term>\<open>option.fixp_fun\<close> 454 \<^term>\<open>option.mono_body\<close> @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc} 455 (SOME @{thm fixp_induct_option})\<close> 456 457hide_const (open) chain 458 459end 460