products/sources/formale Sprachen/Coq/test-suite/ssr/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: telephone.tex   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.4 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff