Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: MultipleJRE.sh Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Library/Option_ord.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section \<open>Canonical order on option type\<close>

theory Option_ord
imports Main
begin

notation
  bot ("\") and
  top ("\") and
  inf  (infixl "\" 70) and
  sup  (infixl "\" 65) and
  Inf  ("\ _" [900] 900) and
  Sup  ("\ _" [900] 900)

syntax
  "_INF1"     :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
  "_INF"      :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
  "_SUP1"     :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
  "_SUP"      :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)

instantiation option :: (preorder) preorder
begin

definition less_eq_option where
  "x \ y \ (case x of None \ True | Some x \ (case y of None \ False | Some y \ x \ y))"

definition less_option where
  "x < y \ (case y of None \ False | Some y \ (case x of None \ True | Some x \ x < y))"

lemma less_eq_option_None [simp]: "None \ x"
  by (simp add: less_eq_option_def)

lemma less_eq_option_None_code [code]: "None \ x \ True"
  by simp

lemma less_eq_option_None_is_None: "x \ None \ x = None"
  by (cases x) (simp_all add: less_eq_option_def)

lemma less_eq_option_Some_None [simp, code]: "Some x \ None \ False"
  by (simp add: less_eq_option_def)

lemma less_eq_option_Some [simp, code]: "Some x \ Some y \ x \ y"
  by (simp add: less_eq_option_def)

lemma less_option_None [simp, code]: "x < None \ False"
  by (simp add: less_option_def)

lemma less_option_None_is_Some: "None < x \ \z. x = Some z"
  by (cases x) (simp_all add: less_option_def)

lemma less_option_None_Some [simp]: "None < Some x"
  by (simp add: less_option_def)

lemma less_option_None_Some_code [code]: "None < Some x \ True"
  by simp

lemma less_option_Some [simp, code]: "Some x < Some y \ x < y"
  by (simp add: less_option_def)

instance
  by standard
    (auto simp add: less_eq_option_def less_option_def less_le_not_le
      elim: order_trans split: option.splits)

end

instance option :: (order) order
  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)

instance option :: (linorder) linorder
  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)

instantiation option :: (order) order_bot
begin

definition bot_option where "\ = None"

instance
  by standard (simp add: bot_option_def)

end

instantiation option :: (order_top) order_top
begin

definition top_option where "\ = Some \"

instance
  by standard (simp add: top_option_def less_eq_option_def split: option.split)

end

instance option :: (wellorder) wellorder
proof
  fix P :: "'a option \ bool"
  fix z :: "'a option"
  assume H: "\x. (\y. y < x \ P y) \ P x"
  have "P None" by (rule H) simp
  then have P_Some [case_names Some]: "P z" if "\x. z = Some x \ (P \ Some) x" for z
    using \<open>P None\<close> that by (cases z) simp_all
  show "P z"
  proof (cases z rule: P_Some)
    case (Some w)
    show "(P \ Some) w"
    proof (induct rule: less_induct)
      case (less x)
      have "P (Some x)"
      proof (rule H)
        fix y :: "'a option"
        assume "y < Some x"
        show "P y"
        proof (cases y rule: P_Some)
          case (Some v)
          with \<open>y < Some x\<close> have "v < x" by simp
          with less show "(P \ Some) v" .
        qed
      qed
      then show ?case by simp
    qed
  qed
qed

instantiation option :: (inf) inf
begin

definition inf_option where
  "x \ y = (case x of None \ None | Some x \ (case y of None \ None | Some y \ Some (x \ y)))"

lemma inf_None_1 [simp, code]: "None \ y = None"
  by (simp add: inf_option_def)

lemma inf_None_2 [simp, code]: "x \ None = None"
  by (cases x) (simp_all add: inf_option_def)

lemma inf_Some [simp, code]: "Some x \ Some y = Some (x \ y)"
  by (simp add: inf_option_def)

instance ..

end

instantiation option :: (sup) sup
begin

definition sup_option where
  "x \ y = (case x of None \ y | Some x' \ (case y of None \ x | Some y \ Some (x' \ y)))"

lemma sup_None_1 [simp, code]: "None \ y = y"
  by (simp add: sup_option_def)

lemma sup_None_2 [simp, code]: "x \ None = x"
  by (cases x) (simp_all add: sup_option_def)

lemma sup_Some [simp, code]: "Some x \ Some y = Some (x \ y)"
  by (simp add: sup_option_def)

instance ..

end

instance option :: (semilattice_inf) semilattice_inf
proof
  fix x y z :: "'a option"
  show "x \ y \ x"
    by (cases x, simp_all, cases y, simp_all)
  show "x \ y \ y"
    by (cases x, simp_all, cases y, simp_all)
  show "x \ y \ x \ z \ x \ y \ z"
    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
qed

instance option :: (semilattice_sup) semilattice_sup
proof
  fix x y z :: "'a option"
  show "x \ x \ y"
    by (cases x, simp_all, cases y, simp_all)
  show "y \ x \ y"
    by (cases x, simp_all, cases y, simp_all)
  fix x y z :: "'a option"
  show "y \ x \ z \ x \ y \ z \ x"
    by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
qed

instance option :: (lattice) lattice ..

instance option :: (lattice) bounded_lattice_bot ..

instance option :: (bounded_lattice_top) bounded_lattice_top ..

instance option :: (bounded_lattice_top) bounded_lattice ..

instance option :: (distrib_lattice) distrib_lattice
proof
  fix x y z :: "'a option"
  show "x \ y \ z = (x \ y) \ (x \ z)"
    by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
qed

instantiation option :: (complete_lattice) complete_lattice
begin

definition Inf_option :: "'a option set \ 'a option" where
  "\A = (if None \ A then None else Some (\Option.these A))"

lemma None_in_Inf [simp]: "None \ A \ \A = None"
  by (simp add: Inf_option_def)

definition Sup_option :: "'a option set \ 'a option" where
  "\A = (if A = {} \ A = {None} then None else Some (\Option.these A))"

lemma empty_Sup [simp]: "\{} = None"
  by (simp add: Sup_option_def)

lemma singleton_None_Sup [simp]: "\{None} = None"
  by (simp add: Sup_option_def)

instance
proof
  fix x :: "'a option" and A
  assume "x \ A"
  then show "\A \ x"
    by (cases x) (auto simp add: Inf_option_def in_these_eq intro: Inf_lower)
next
  fix z :: "'a option" and A
  assume *: "\x. x \ A \ z \ x"
  show "z \ \A"
  proof (cases z)
    case None then show ?thesis by simp
  next
    case (Some y)
    show ?thesis
      by (auto simp add: Inf_option_def in_these_eq Some intro!: Inf_greatest dest!: *)
  qed
next
  fix x :: "'a option" and A
  assume "x \ A"
  then show "x \ \A"
    by (cases x) (auto simp add: Sup_option_def in_these_eq intro: Sup_upper)
next
  fix z :: "'a option" and A
  assume *: "\x. x \ A \ x \ z"
  show "\A \ z "
  proof (cases z)
    case None
    with * have "\x. x \ A \ x = None" by (auto dest: less_eq_option_None_is_None)
    then have "A = {} \ A = {None}" by blast
    then show ?thesis by (simp add: Sup_option_def)
  next
    case (Some y)
    from * have "\w. Some w \ A \ Some w \ z" .
    with Some have "\w. w \ Option.these A \ w \ y"
      by (simp add: in_these_eq)
    then have "\Option.these A \ y" by (rule Sup_least)
    with Some show ?thesis by (simp add: Sup_option_def)
  qed
next
  show "\{} = (\::'a option)"
    by (auto simp: bot_option_def)
  show "\{} = (\::'a option)"
    by (auto simp: top_option_def Inf_option_def)
qed

end

lemma Some_Inf:
  "Some (\A) = \(Some ` A)"
  by (auto simp add: Inf_option_def)

lemma Some_Sup:
  "A \ {} \ Some (\A) = \(Some ` A)"
  by (auto simp add: Sup_option_def)

lemma Some_INF:
  "Some (\x\A. f x) = (\x\A. Some (f x))"
  by (simp add: Some_Inf image_comp)

lemma Some_SUP:
  "A \ {} \ Some (\x\A. f x) = (\x\A. Some (f x))"
  by (simp add: Some_Sup image_comp)

lemma option_Inf_Sup: "\(Sup ` A) \ \(Inf ` {f ` A |f. \Y\A. f Y \ Y})"
  for A :: "('a::complete_distrib_lattice option) set set"
proof (cases "{} \ A")
  case True
  then show ?thesis
    by (rule INF_lower2, simp_all)
next
  case False
  from this have X: "{} \ A"
    by simp
  then show ?thesis
  proof (cases "{None} \ A")
    case True
    then show ?thesis
      by (rule INF_lower2, simp_all)
  next
    case False

    {fix y
      assume A: "y \ A"
      have "Sup (y - {None}) = Sup y"
        by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
      from A and this have "(\z. y - {None} = z - {None} \ z \ A) \ \y = \(y - {None})"
        by auto
    }
    from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\A})"
      by (auto simp add: image_def)

    have [simp]: "\y. y \ A \ \ya. {ya. \x. x \ y \ (\y. x = Some y) \ ya = the x}
          = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
      by (rule exI, auto)

    have [simp]: "\y. y \ A \
         (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x}
          = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
      apply (safe, blast)
      by (rule arg_cong [of _ _ Sup], auto)
    {fix y
      assume [simp]: "y \ A"
      have "\x. (\y. x = {ya. \x\y - {None}. ya = the x} \ y \ A) \ \{ya. \x. x \ y \ (\y. x = Some y) \ ya = the x} = \x"
      and "\x. (\y. x = y - {None} \ y \ A) \ \{ya. \x\y - {None}. ya = the x} = \{y. \xa. xa \ x \ (\y. xa = Some y) \ y = the xa}"
         apply (rule exI [of _ "{ya. \x. x \ y \ (\y. x = Some y) \ ya = the x}"], simp)
        by (rule exI [of _ "y - {None}"], simp)
    }
    from this have C: "(\x. (\Option.these x)) ` {y - {None} |y. y \ A} = (Sup ` {the ` (y - {None}) |y. y \ A})"
      by (simp add: image_def Option.these_def, safe, simp_all)

    have D: "\ f . \Y\A. f Y \ Y \ False"
      by (drule spec [of _ "\ Y . SOME x . x \ Y"], simp add: X some_in_eq)

    define F where "F = (\ Y . SOME x::'a option . x \ (Y - {None}))"

    have G: "\ Y . Y \ A \ \ x . x \ Y - {None}"
      by (metis False X all_not_in_conv insert_Diff_single these_insert_None these_not_empty_eq)

    have F: "\ Y . Y \ A \ F Y \ (Y - {None})"
      by (metis F_def G empty_iff some_in_eq)

    have "Some \ \ Inf (F ` A)"
      by (metis (no_types, lifting) Diff_iff F Inf_option_def bot.extremum image_iff
          less_eq_option_Some singletonI)

    from this have "Inf (F ` A) \ None"
      by (cases "\x\A. F x", simp_all)

    from this have "Inf (F ` A) \ None \ Inf (F ` A) \ Inf ` {f ` A |f. \Y\A. f Y \ Y}"
      using F by auto

    from this have "\ x . x \ None \ x \ Inf ` {f ` A |f. \Y\A. f Y \ Y}"
      by blast

    from this have E:" Inf ` {f ` A |f. \Y\A. f Y \ Y} = {None} \ False"
      by blast

    have [simp]: "((\x\{f ` A |f. \Y\A. f Y \ Y}. \x) = None) = False"
      by (metis (no_types, lifting) E Sup_option_def \<open>\<exists>x. x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}\<close>
          ex_in_conv option.simps(3))

    have B: "Option.these ((\x. Some (\Option.these x)) ` {y - {None} |y. y \ A})
        = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
      by (metis image_image these_image_Some_eq)
    {
      fix f
      assume A: "\ Y . (\y. Y = the ` (y - {None}) \ y \ A) \ f Y \ Y"

      have "\xa. xa \ A \ f {y. \a\xa - {None}. y = the a} = f (the ` (xa - {None}))"
        by  (simp add: image_def)
      from this have [simp]: "\xa. xa \ A \ \x\A. f {y. \a\xa - {None}. y = the a} = f (the ` (x - {None}))"
        by blast
      have "\xa. xa \ A \ f (the ` (xa - {None})) = f {y. \a \ xa - {None}. y = the a} \ xa \ A"
        by (simp add: image_def)
      from this have [simp]: "\xa. xa \ A \ \x. f (the ` (xa - {None})) = f {y. \a\x - {None}. y = the a} \ x \ A"
        by blast

      {
        fix Y
        have "Y \ A \ Some (f (the ` (Y - {None}))) \ Y"
          using A [of "the ` (Y - {None})"] apply (simp add: image_def)
          using option.collapse by fastforce
      }
      from this have [simp]: "\ Y . Y \ A \ Some (f (the ` (Y - {None}))) \ Y"
        by blast
      have [simp]: "(\x\A. Some (f {y. \x\x - {None}. y = the x})) = \{Some (f {y. \a\x - {None}. y = the a}) |x. x \ A}"
        by (simp add: Setcompr_eq_image)

      have [simp]: "\x. (\f. x = {y. \x\A. y = f x} \ (\Y\A. f Y \ Y)) \ \{Some (f {y. \a\x - {None}. y = the a}) |x. x \ A} = \x"
        apply (rule exI [of _ "{Some (f {y. \a\x - {None}. y = the a}) | x . x\ A}"], safe)
        by (rule exI [of _ "(\ Y . Some (f (the ` (Y - {None})))) "], safe, simp_all)

      {
        fix xb
        have "xb \ A \ (\x\{{ya. \x\y - {None}. ya = the x} |y. y \ A}. f x) \ f {y. \x\xb - {None}. y = the x}"
          apply (rule INF_lower2 [of "{y. \x\xb - {None}. y = the x}"])
          by blast+
      }
      from this have [simp]: "(\x\{the ` (y - {None}) |y. y \ A}. f x) \ the (\Y\A. Some (f (the ` (Y - {None}))))"
        apply (simp add: Inf_option_def image_def Option.these_def)
        by (rule Inf_greatest, clarsimp)
      have [simp]: "the (\Y\A. Some (f (the ` (Y - {None})))) \ Option.these (Inf ` {f ` A |f. \Y\A. f Y \ Y})"
        apply (auto simp add: Option.these_def)
        apply (rule imageI)
        apply auto
        using \<open>\<And>Y. Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y\<close> apply blast
        apply (auto simp add: Some_INF [symmetric])
        done
      have "(\x\{the ` (y - {None}) |y. y \ A}. f x) \ \Option.these (Inf ` {f ` A |f. \Y\A. f Y \ Y})"
        by (rule Sup_upper2 [of "the (Inf ((\ Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
    }
    from this have X: "\ f . \Y. (\y. Y = the ` (y - {None}) \ y \ A) \ f Y \ Y \
      (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
      by blast


    have [simp]: "\ x . x\{y - {None} |y. y \ A} \ x \ {} \ x \ {None}"
      using F by fastforce

    have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\A}))"
      by (subst A, simp)

    also have "... = (\x\{y - {None} |y. y \ A}. if x = {} \ x = {None} then None else Some (\Option.these x))"
      by (simp add: Sup_option_def)

    also have "... = (\x\{y - {None} |y. y \ A}. Some (\Option.these x))"
      using G by fastforce

    also have "... = Some (\Option.these ((\x. Some (\Option.these x)) ` {y - {None} |y. y \ A}))"
      by (simp add: Inf_option_def, safe)

    also have "... = Some (\ ((\x. (\Option.these x)) ` {y - {None} |y. y \ A}))"
      by (simp add: B)

    also have "... = Some (Inf (Sup ` {the ` (y - {None}) |y. y \ A}))"
      by (unfold C, simp)
    thm Inf_Sup
    also have "... = Some (\x\{f ` {the ` (y - {None}) |y. y \ A} |f. \Y. (\y. Y = the ` (y - {None}) \ y \ A) \ f Y \ Y}. \x) "
      by (simp add: Inf_Sup)

    also have "... \ \ (Inf ` {f ` A |f. \Y\A. f Y \ Y})"
    proof (cases "\ (Inf ` {f ` A |f. \Y\A. f Y \ Y})")
      case None
      then show ?thesis by (simp add: less_eq_option_def)
    next
      case (Some a)
      then show ?thesis
        apply simp
        apply (rule Sup_least, safe)
        apply (simp add: Sup_option_def)
        apply (cases "(\f. \Y\A. f Y \ Y) \ Inf ` {f ` A |f. \Y\A. f Y \ Y} = {None}", simp_all)
        by (drule X, simp)
    qed
    finally show ?thesis by simp
  qed
qed

instance option :: (complete_distrib_lattice) complete_distrib_lattice
  by (standard, simp add: option_Inf_Sup)

instance option :: (complete_linorder) complete_linorder ..

no_notation
  bot ("\") and
  top ("\") and
  inf  (infixl "\" 70) and
  sup  (infixl "\" 65) and
  Inf  ("\ _" [900] 900) and
  Sup  ("\ _" [900] 900)

no_syntax
  "_INF1"     :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
  "_INF"      :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)
  "_SUP1"     :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10)
  "_SUP"      :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10)

end

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.