# Theory Partial_Function

Up to index of Isabelle/HOL-Proofs

theory Partial_Function
imports Complete_Partial_Order Option
`(* Title:    HOL/Partial_Function.thy   Author:   Alexander Krauss, TU Muenchen*)header {* Partial Function Definitions *}theory Partial_Functionimports Complete_Partial_Order Optionkeywords "partial_function" :: thy_declbeginML_file "Tools/Function/function_lib.ML"ML_file "Tools/Function/partial_function.ML"setup Partial_Function.setupsubsection {* Axiomatic setup *}text {* This techical locale constains the requirements for function  definitions with ccpo fixed points. *}definition "fun_ord ord f g <-> (∀x. ord (f x) (g x))"definition "fun_lub L A = (λx. L {y. ∃f∈A. y = f x})"definition "img_ord f ord = (λx y. ord (f x) (f y))"definition "img_lub f g Lub = (λA. g (Lub (f ` A)))"lemma chain_fun:   assumes A: "chain (fun_ord ord) A"  shows "chain ord {y. ∃f∈A. y = f a}" (is "chain ord ?C")proof (rule chainI)  fix x y assume "x ∈ ?C" "y ∈ ?C"  then obtain f g where fg: "f ∈ A" "g ∈ A"     and [simp]: "x = f a" "y = g a" by blast  from chainD[OF A fg]  show "ord x y ∨ ord y x" unfolding fun_ord_def by autoqedlemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (λf. f t)"by (rule monotoneI) (auto simp: fun_ord_def)lemma let_mono[partial_function_mono]:  "(!!x. monotone orda ordb (λf. b f x))  ==> monotone orda ordb (λf. Let t (b f))"by (simp add: Let_def)lemma if_mono[partial_function_mono]: "monotone orda ordb F ==> monotone orda ordb G==> monotone orda ordb (λf. if c then F f else G f)"unfolding monotone_def by simpdefinition "mk_less R = (λx y. R x y ∧ ¬ R y x)"locale partial_function_definitions =   fixes leq :: "'a => 'a => bool"  fixes lub :: "'a set => 'a"  assumes leq_refl: "leq x x"  assumes leq_trans: "leq x y ==> leq y z ==> leq x z"  assumes leq_antisym: "leq x y ==> leq y x ==> x = y"  assumes lub_upper: "chain leq A ==> x ∈ A ==> leq x (lub A)"  assumes lub_least: "chain leq A ==> (!!x. x ∈ A ==> leq x z) ==> leq (lub A) z"lemma partial_function_lift:  assumes "partial_function_definitions ord lb"  shows "partial_function_definitions (fun_ord ord) (fun_lub lb)" (is "partial_function_definitions ?ordf ?lubf")proof -  interpret partial_function_definitions ord lb by fact  show ?thesis  proof    fix x show "?ordf x x"      unfolding fun_ord_def by (auto simp: leq_refl)  next    fix x y z assume "?ordf x y" "?ordf y z"    thus "?ordf x z" unfolding fun_ord_def       by (force dest: leq_trans)  next    fix x y assume "?ordf x y" "?ordf y x"    thus "x = y" unfolding fun_ord_def      by (force intro!: dest: leq_antisym)  next    fix A f assume f: "f ∈ A" and A: "chain ?ordf A"    thus "?ordf f (?lubf A)"      unfolding fun_lub_def fun_ord_def      by (blast intro: lub_upper chain_fun[OF A] f)  next    fix A :: "('b => 'a) set" and g :: "'b => 'a"    assume A: "chain ?ordf A" and g: "!!f. f ∈ A ==> ?ordf f g"    show "?ordf (?lubf A) g" unfolding fun_lub_def fun_ord_def      by (blast intro: lub_least chain_fun[OF A] dest: g[unfolded fun_ord_def])   qedqedlemma ccpo: assumes "partial_function_definitions ord lb"  shows "class.ccpo lb ord (mk_less ord)"using assms unfolding partial_function_definitions_def mk_less_defby unfold_locales blast+lemma partial_function_image:  assumes "partial_function_definitions ord Lub"  assumes inj: "!!x y. f x = f y ==> x = y"  assumes inv: "!!x. f (g x) = x"  shows "partial_function_definitions (img_ord f ord) (img_lub f g Lub)"proof -  let ?iord = "img_ord f ord"  let ?ilub = "img_lub f g Lub"  interpret partial_function_definitions ord Lub by fact  show ?thesis  proof    fix A x assume "chain ?iord A" "x ∈ A"    then have "chain ord (f ` A)" "f x ∈ f ` A"      by (auto simp: img_ord_def intro: chainI dest: chainD)    thus "?iord x (?ilub A)"      unfolding inv img_lub_def img_ord_def by (rule lub_upper)  next    fix A x assume "chain ?iord A"      and 1: "!!z. z ∈ A ==> ?iord z x"    then have "chain ord (f ` A)"      by (auto simp: img_ord_def intro: chainI dest: chainD)    thus "?iord (?ilub A) x"      unfolding inv img_lub_def img_ord_def      by (rule lub_least) (auto dest: 1[unfolded img_ord_def])  qed (auto simp: img_ord_def intro: leq_refl dest: leq_trans leq_antisym inj)qedcontext partial_function_definitionsbeginabbreviation "le_fun ≡ fun_ord leq"abbreviation "lub_fun ≡ fun_lub lub"abbreviation "fixp_fun ≡ ccpo.fixp lub_fun le_fun"abbreviation "mono_body ≡ monotone le_fun leq"abbreviation "admissible ≡ ccpo.admissible lub_fun le_fun"text {* Interpret manually, to avoid flooding everything with facts about  orders *}lemma ccpo: "class.ccpo lub_fun le_fun (mk_less le_fun)"apply (rule ccpo)apply (rule partial_function_lift)apply (rule partial_function_definitions_axioms)donetext {* The crucial fixed-point theorem *}lemma mono_body_fixp:   "(!!x. mono_body (λf. F f x)) ==> fixp_fun F = F (fixp_fun F)"by (rule ccpo.fixp_unfold[OF ccpo]) (auto simp: monotone_def fun_ord_def)text {* Version with curry/uncurry combinators, to be used by package *}lemma fixp_rule_uc:  fixes F :: "'c => 'c" and    U :: "'c => 'b => 'a" and    C :: "('b => 'a) => 'c"  assumes mono: "!!x. mono_body (λf. U (F (C f)) x)"  assumes eq: "f ≡ C (fixp_fun (λf. U (F (C f))))"  assumes inverse: "!!f. C (U f) = f"  shows "f = F f"proof -  have "f = C (fixp_fun (λf. U (F (C f))))" by (simp add: eq)  also have "... = C (U (F (C (fixp_fun (λf. U (F (C f)))))))"    by (subst mono_body_fixp[of "%f. U (F (C f))", OF mono]) (rule refl)  also have "... = F (C (fixp_fun (λf. U (F (C f)))))" by (rule inverse)  also have "... = F f" by (simp add: eq)  finally show "f = F f" .qedtext {* Fixpoint induction rule *}lemma fixp_induct_uc:  fixes F :: "'c => 'c" and    U :: "'c => 'b => 'a" and    C :: "('b => 'a) => 'c" and    P :: "('b => 'a) => bool"  assumes mono: "!!x. mono_body (λf. U (F (C f)) x)"  assumes eq: "f ≡ C (fixp_fun (λf. U (F (C f))))"  assumes inverse: "!!f. U (C f) = f"  assumes adm: "ccpo.admissible lub_fun le_fun P"  assumes step: "!!f. P (U f) ==> P (U (F f))"  shows "P (U f)"unfolding eq inverseapply (rule ccpo.fixp_induct[OF ccpo adm])apply (insert mono, auto simp: monotone_def fun_ord_def)[1]by (rule_tac f="C x" in step, simp add: inverse)text {* Rules for @{term mono_body}: *}lemma const_mono[partial_function_mono]: "monotone ord leq (λf. c)"by (rule monotoneI) (rule leq_refl)endsubsection {* Flat interpretation: tailrec and option *}definition   "flat_ord b x y <-> x = b ∨ x = y"definition   "flat_lub b A = (if A ⊆ {b} then b else (THE x. x ∈ A - {b}))"lemma flat_interpretation:  "partial_function_definitions (flat_ord b) (flat_lub b)"proof  fix A x assume 1: "chain (flat_ord b) A" "x ∈ A"  show "flat_ord b x (flat_lub b A)"  proof cases    assume "x = b"    thus ?thesis by (simp add: flat_ord_def)  next    assume "x ≠ b"    with 1 have "A - {b} = {x}"      by (auto elim: chainE simp: flat_ord_def)    then have "flat_lub b A = x"      by (auto simp: flat_lub_def)    thus ?thesis by (auto simp: flat_ord_def)  qednext  fix A z assume A: "chain (flat_ord b) A"    and z: "!!x. x ∈ A ==> flat_ord b x z"  show "flat_ord b (flat_lub b A) z"  proof cases    assume "A ⊆ {b}"    thus ?thesis      by (auto simp: flat_lub_def flat_ord_def)  next    assume nb: "¬ A ⊆ {b}"    then obtain y where y: "y ∈ A" "y ≠ b" by auto    with A have "A - {b} = {y}"      by (auto elim: chainE simp: flat_ord_def)    with nb have "flat_lub b A = y"      by (auto simp: flat_lub_def)    with z y show ?thesis by auto      qedqed (auto simp: flat_ord_def)interpretation tailrec!:  partial_function_definitions "flat_ord undefined" "flat_lub undefined"by (rule flat_interpretation)interpretation option!:  partial_function_definitions "flat_ord None" "flat_lub None"by (rule flat_interpretation)abbreviation "option_ord ≡ flat_ord None"abbreviation "mono_option ≡ monotone (fun_ord option_ord) option_ord"lemma bind_mono[partial_function_mono]:assumes mf: "mono_option B" and mg: "!!y. mono_option (λf. C y f)"shows "mono_option (λf. Option.bind (B f) (λy. C y f))"proof (rule monotoneI)  fix f g :: "'a => 'b option" assume fg: "fun_ord option_ord f g"  with mf  have "option_ord (B f) (B g)" by (rule monotoneD[of _ _ _ f g])  then have "option_ord (Option.bind (B f) (λy. C y f)) (Option.bind (B g) (λy. C y f))"    unfolding flat_ord_def by auto      also from mg  have "!!y'. option_ord (C y' f) (C y' g)"    by (rule monotoneD) (rule fg)  then have "option_ord (Option.bind (B g) (λy'. C y' f)) (Option.bind (B g) (λy'. C y' g))"    unfolding flat_ord_def by (cases "B g") auto  finally (option.leq_trans)  show "option_ord (Option.bind (B f) (λy. C y f)) (Option.bind (B g) (λy'. C y' g))" .qedlemma flat_lub_in_chain:  assumes ch: "chain (flat_ord b) A "  assumes lub: "flat_lub b A = a"  shows "a = b ∨ a ∈ A"proof (cases "A ⊆ {b}")  case True  then have "flat_lub b A = b" unfolding flat_lub_def by simp  with lub show ?thesis by simpnext  case False  then obtain c where "c ∈ A" and "c ≠ b" by auto  { fix z assume "z ∈ A"    from chainD[OF ch `c ∈ A` this] have "z = c ∨ z = b"      unfolding flat_ord_def using `c ≠ b` by auto }  with False have "A - {b} = {c}" by auto  with False have "flat_lub b A = c" by (auto simp: flat_lub_def)  with `c ∈ A` lub show ?thesis by simpqedlemma option_admissible: "option.admissible (%(f::'a => 'b option).  (∀x y. f x = Some y --> P x y))"proof (rule ccpo.admissibleI[OF option.ccpo])  fix A :: "('a => 'b option) set"  assume ch: "chain option.le_fun A"    and IH: "∀f∈A. ∀x y. f x = Some y --> P x y"  from ch have ch': "!!x. chain option_ord {y. ∃f∈A. y = f x}" by (rule chain_fun)  show "∀x y. option.lub_fun A x = Some y --> P x y"  proof (intro allI impI)    fix x y assume "option.lub_fun A x = Some y"    from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]    have "Some y ∈ {y. ∃f∈A. y = f x}" by simp    then have "∃f∈A. f x = Some y" by auto    with IH show "P x y" by auto  qedqedlemma fixp_induct_option:  fixes F :: "'c => 'c" and    U :: "'c => 'b => 'a option" and    C :: "('b => 'a option) => 'c" and    P :: "'b => 'a => bool"  assumes mono: "!!x. mono_option (λf. U (F (C f)) x)"  assumes eq: "f ≡ C (ccpo.fixp (fun_lub (flat_lub None)) (fun_ord option_ord) (λf. U (F (C f))))"  assumes inverse2: "!!f. U (C f) = f"  assumes step: "!!f x y. (!!x y. U f x = Some y ==> P x y) ==> U (F f) x = Some y ==> P x y"  assumes defined: "U f x = Some y"  shows "P x y"  using step defined option.fixp_induct_uc[of U F C, OF mono eq inverse2 option_admissible]  by blastdeclaration {* Partial_Function.init "tailrec" @{term tailrec.fixp_fun}  @{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} NONE *}declaration {* Partial_Function.init "option" @{term option.fixp_fun}  @{term option.mono_body} @{thm option.fixp_rule_uc}   (SOME @{thm fixp_induct_option}) *}hide_const (open) chainend`