Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Heap.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/HOLCF/Ssum.thy
    Author:     Franz Regensburger
    Author:     Brian Huffman
*)

section \<open>The type of strict sums\<close>

theory Ssum
  imports Tr
begin

default_sort pcpo

subsection \<open>Definition of strict sum type\<close>

definition "ssum =
  {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
    (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
    (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"

pcpodef ('a, 'b) ssum  ("(_ \/ _)" [21, 20] 20) = "ssum :: (tr \ 'a \ 'b) set"
  by (simp_all add: ssum_def)

instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
  by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])

type_notation (ASCII)
  ssum  (infixr "++" 10)

subsection \<open>Definitions of constructors\<close>

definition sinl :: "'a \ ('a ++ 'b)"
  where "sinl = (\ a. Abs_ssum (seq\a\TT, a, \))"

definition sinr :: "'b \ ('a ++ 'b)"
  where "sinr = (\ b. Abs_ssum (seq\b\FF, \, b))"

lemma sinl_ssum: "(seq\a\TT, a, \) \ ssum"
  by (simp add: ssum_def seq_conv_if)

lemma sinr_ssum: "(seq\b\FF, \, b) \ ssum"
  by (simp add: ssum_def seq_conv_if)

lemma Rep_ssum_sinl: "Rep_ssum (sinl\a) = (seq\a\TT, a, \)"
  by (simp add: sinl_def cont_Abs_ssum Abs_ssum_inverse sinl_ssum)

lemma Rep_ssum_sinr: "Rep_ssum (sinr\b) = (seq\b\FF, \, b)"
  by (simp add: sinr_def cont_Abs_ssum Abs_ssum_inverse sinr_ssum)

lemmas Rep_ssum_simps =
  Rep_ssum_inject [symmetric] below_ssum_def
  prod_eq_iff below_prod_def
  Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr

subsection \<open>Properties of \emph{sinl} and \emph{sinr}\<close>

text \<open>Ordering\<close>

lemma sinl_below [simp]: "sinl\x \ sinl\y \ x \ y"
  by (simp add: Rep_ssum_simps seq_conv_if)

lemma sinr_below [simp]: "sinr\x \ sinr\y \ x \ y"
  by (simp add: Rep_ssum_simps seq_conv_if)

lemma sinl_below_sinr [simp]: "sinl\x \ sinr\y \ x = \"
  by (simp add: Rep_ssum_simps seq_conv_if)

lemma sinr_below_sinl [simp]: "sinr\x \ sinl\y \ x = \"
  by (simp add: Rep_ssum_simps seq_conv_if)

text \<open>Equality\<close>

lemma sinl_eq [simp]: "sinl\x = sinl\y \ x = y"
  by (simp add: po_eq_conv)

lemma sinr_eq [simp]: "sinr\x = sinr\y \ x = y"
  by (simp add: po_eq_conv)

lemma sinl_eq_sinr [simp]: "sinl\x = sinr\y \ x = \ \ y = \"
  by (subst po_eq_conv) simp

lemma sinr_eq_sinl [simp]: "sinr\x = sinl\y \ x = \ \ y = \"
  by (subst po_eq_conv) simp

lemma sinl_inject: "sinl\x = sinl\y \ x = y"
  by (rule sinl_eq [THEN iffD1])

lemma sinr_inject: "sinr\x = sinr\y \ x = y"
  by (rule sinr_eq [THEN iffD1])

text \<open>Strictness\<close>

lemma sinl_strict [simp]: "sinl\\ = \"
  by (simp add: Rep_ssum_simps)

lemma sinr_strict [simp]: "sinr\\ = \"
  by (simp add: Rep_ssum_simps)

lemma sinl_bottom_iff [simp]: "sinl\x = \ \ x = \"
  using sinl_eq [of "x" "\"] by simp

lemma sinr_bottom_iff [simp]: "sinr\x = \ \ x = \"
  using sinr_eq [of "x" "\"] by simp

lemma sinl_defined: "x \ \ \ sinl\x \ \"
  by simp

lemma sinr_defined: "x \ \ \ sinr\x \ \"
  by simp

text \<open>Compactness\<close>

lemma compact_sinl: "compact x \ compact (sinl\x)"
  by (rule compact_ssum) (simp add: Rep_ssum_sinl)

lemma compact_sinr: "compact x \ compact (sinr\x)"
  by (rule compact_ssum) (simp add: Rep_ssum_sinr)

lemma compact_sinlD: "compact (sinl\x) \ compact x"
  unfolding compact_def
  by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)

lemma compact_sinrD: "compact (sinr\x) \ compact x"
  unfolding compact_def
  by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)

lemma compact_sinl_iff [simp]: "compact (sinl\x) = compact x"
  by (safe elim!: compact_sinl compact_sinlD)

lemma compact_sinr_iff [simp]: "compact (sinr\x) = compact x"
  by (safe elim!: compact_sinr compact_sinrD)

subsection \<open>Case analysis\<close>

lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
  obtains "p = \"
  | x where "p = sinl\x" and "x \ \"
  | y where "p = sinr\y" and "y \ \"
  using Rep_ssum [of p] by (auto simp add: ssum_def Rep_ssum_simps)

lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
  "\P \;
   \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
   \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
  by (cases x) simp_all

lemma ssumE2 [case_names sinl sinr]:
  "\\x. p = sinl\x \ Q; \y. p = sinr\y \ Q\ \ Q"
  by (cases p, simp only: sinl_strict [symmetric], simp, simp)

lemma below_sinlD: "p \ sinl\x \ \y. p = sinl\y \ y \ x"
  by (cases p, rule_tac x="\" in exI, simp_all)

lemma below_sinrD: "p \ sinr\x \ \y. p = sinr\y \ y \ x"
  by (cases p, rule_tac x="\" in exI, simp_all)

subsection \<open>Case analysis combinator\<close>

definition sscase :: "('a \ 'c) \ ('b \ 'c) \ ('a ++ 'b) \ 'c"
  where "sscase = (\ f g s. (\(t, x, y). If t then f\x else g\y) (Rep_ssum s))"

translations
  "case s of XCONST sinl\x \ t1 | XCONST sinr\y \ t2" \ "CONST sscase\(\ x. t1)\(\ y. t2)\s"
  "case s of (XCONST sinl :: 'a)\x \ t1 | XCONST sinr\y \ t2" \ "CONST sscase\(\ x. t1)\(\ y. t2)\s"

translations
  "\(XCONST sinl\x). t" \ "CONST sscase\(\ x. t)\\"
  "\(XCONST sinr\y). t" \ "CONST sscase\\\(\ y. t)"

lemma beta_sscase: "sscase\f\g\s = (\(t, x, y). If t then f\x else g\y) (Rep_ssum s)"
  by (simp add: sscase_def cont_Rep_ssum)

lemma sscase1 [simp]: "sscase\f\g\\ = \"
  by (simp add: beta_sscase Rep_ssum_strict)

lemma sscase2 [simp]: "x \ \ \ sscase\f\g\(sinl\x) = f\x"
  by (simp add: beta_sscase Rep_ssum_sinl)

lemma sscase3 [simp]: "y \ \ \ sscase\f\g\(sinr\y) = g\y"
  by (simp add: beta_sscase Rep_ssum_sinr)

lemma sscase4 [simp]: "sscase\sinl\sinr\z = z"
  by (cases z) simp_all

subsection \<open>Strict sum preserves flatness\<close>

instance ssum :: (flat, flat) flat
  apply (intro_classes, clarify)
  apply (case_tac x, simp)
   apply (case_tac y, simp_all add: flat_below_iff)
  apply (case_tac y, simp_all add: flat_below_iff)
  done

end

¤ Dauer der Verarbeitung: 0.22 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.