src/HOLCF/One.thy
author wenzelm
Sun Oct 21 14:21:48 2007 +0200 (2007-10-21)
changeset 25131 2c8caac48ade
parent 18111 2b56f74fd605
child 27293 de9a2fd0eab4
permissions -rw-r--r--
modernized specifications ('definition', 'abbreviation', 'notation');
slotosch@2640
     1
(*  Title:      HOLCF/One.thy
nipkow@243
     2
    ID:         $Id$
slotosch@2640
     3
    Author:     Oscar Slotosch
wenzelm@16070
     4
wenzelm@16070
     5
The unit domain.
nipkow@243
     6
*)
nipkow@243
     7
huffman@15577
     8
header {* The unit domain *}
huffman@15577
     9
huffman@15577
    10
theory One
huffman@15577
    11
imports Lift
huffman@15577
    12
begin
nipkow@243
    13
huffman@15576
    14
types one = "unit lift"
wenzelm@25131
    15
translations
wenzelm@25131
    16
  "one" <= (type) "unit lift" 
nipkow@243
    17
wenzelm@3717
    18
constdefs
wenzelm@3717
    19
  ONE :: "one"
wenzelm@25131
    20
  "ONE == Def ()"
nipkow@243
    21
huffman@16747
    22
text {* Exhaustion and Elimination for type @{typ one} *}
huffman@15576
    23
huffman@16747
    24
lemma Exh_one: "t = \<bottom> \<or> t = ONE"
huffman@15576
    25
apply (unfold ONE_def)
huffman@15576
    26
apply (induct t)
huffman@15576
    27
apply simp
huffman@15576
    28
apply simp
huffman@15576
    29
done
huffman@15576
    30
huffman@16747
    31
lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@15576
    32
apply (rule Exh_one [THEN disjE])
huffman@15576
    33
apply fast
huffman@15576
    34
apply fast
huffman@15576
    35
done
huffman@15576
    36
huffman@16747
    37
lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
huffman@15576
    38
apply (unfold ONE_def)
huffman@16747
    39
apply simp
huffman@15576
    40
done
huffman@15576
    41
huffman@16747
    42
lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
huffman@15576
    43
apply (unfold ONE_def)
huffman@16747
    44
apply simp_all
huffman@15576
    45
done
huffman@15576
    46
huffman@17838
    47
lemma compact_ONE [simp]: "compact ONE"
huffman@17838
    48
by (rule compact_chfin)
huffman@17838
    49
huffman@18080
    50
text {* Case analysis function for type @{typ one} *}
huffman@18080
    51
wenzelm@25131
    52
definition
wenzelm@25131
    53
  one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
wenzelm@25131
    54
  "one_when = (\<Lambda> a. strictify\<cdot>(\<Lambda> _. a))"
huffman@18080
    55
huffman@18080
    56
translations
wenzelm@25131
    57
  "case x of CONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
wenzelm@25131
    58
  "\<Lambda> (CONST ONE). t" == "CONST one_when\<cdot>t"
huffman@18080
    59
huffman@18111
    60
lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
huffman@18080
    61
by (simp add: one_when_def)
huffman@18080
    62
huffman@18111
    63
lemma one_when2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
huffman@18080
    64
by (simp add: one_when_def)
huffman@18080
    65
huffman@18111
    66
lemma one_when3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
huffman@18080
    67
by (rule_tac p=x in oneE, simp_all)
huffman@18080
    68
nipkow@243
    69
end