src/HOL/HOLCF/One.thy
author wenzelm
Mon Jan 01 23:07:24 2018 +0100 (2018-01-01)
changeset 67312 0d25e02759b7
parent 62175 8ffc4d0e652d
child 69597 ff784d5a5bfb
permissions -rw-r--r--
misc tuning and modernization;
     1 (*  Title:      HOL/HOLCF/One.thy
     2     Author:     Oscar Slotosch
     3 *)
     4 
     5 section \<open>The unit domain\<close>
     6 
     7 theory One
     8   imports Lift
     9 begin
    10 
    11 type_synonym one = "unit lift"
    12 
    13 translations
    14   (type) "one" \<leftharpoondown> (type) "unit lift"
    15 
    16 definition ONE :: "one"
    17   where "ONE \<equiv> Def ()"
    18 
    19 text \<open>Exhaustion and Elimination for type @{typ one}\<close>
    20 
    21 lemma Exh_one: "t = \<bottom> \<or> t = ONE"
    22   by (induct t) (simp_all add: ONE_def)
    23 
    24 lemma oneE [case_names bottom ONE]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    25   by (induct p) (simp_all add: ONE_def)
    26 
    27 lemma one_induct [case_names bottom ONE]: "P \<bottom> \<Longrightarrow> P ONE \<Longrightarrow> P x"
    28   by (cases x rule: oneE) simp_all
    29 
    30 lemma dist_below_one [simp]: "ONE \<notsqsubseteq> \<bottom>"
    31   by (simp add: ONE_def)
    32 
    33 lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
    34   by (induct x rule: one_induct) simp_all
    35 
    36 lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
    37   by (induct x rule: one_induct) simp_all
    38 
    39 lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
    40   by (simp add: ONE_def)
    41 
    42 lemma one_neq_iffs [simp]:
    43   "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
    44   "ONE \<noteq> x \<longleftrightarrow> x = \<bottom>"
    45   "x \<noteq> \<bottom> \<longleftrightarrow> x = ONE"
    46   "\<bottom> \<noteq> x \<longleftrightarrow> x = ONE"
    47   by (induct x rule: one_induct) simp_all
    48 
    49 lemma compact_ONE: "compact ONE"
    50   by (rule compact_chfin)
    51 
    52 text \<open>Case analysis function for type @{typ one}\<close>
    53 
    54 definition one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a"
    55   where "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
    56 
    57 translations
    58   "case x of XCONST ONE \<Rightarrow> t" \<rightleftharpoons> "CONST one_case\<cdot>t\<cdot>x"
    59   "case x of XCONST ONE :: 'a \<Rightarrow> t" \<rightharpoonup> "CONST one_case\<cdot>t\<cdot>x"
    60   "\<Lambda> (XCONST ONE). t" \<rightleftharpoons> "CONST one_case\<cdot>t"
    61 
    62 lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
    63   by (simp add: one_case_def)
    64 
    65 lemma one_case2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
    66   by (simp add: one_case_def)
    67 
    68 lemma one_case3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
    69   by (induct x rule: one_induct) simp_all
    70 
    71 end