src/HOLCF/One.thy
author huffman
Thu Nov 03 01:44:27 2005 +0100 (2005-11-03)
changeset 18080 c1a7490ee3ff
parent 17838 3032e90c4975
child 18111 2b56f74fd605
permissions -rw-r--r--
add constant one_when; LAM pattern for ONE
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"
nipkow@243
    15
wenzelm@3717
    16
constdefs
wenzelm@3717
    17
  ONE :: "one"
huffman@16747
    18
  "ONE \<equiv> Def ()"
slotosch@2640
    19
slotosch@2640
    20
translations
wenzelm@3717
    21
  "one" <= (type) "unit lift" 
nipkow@243
    22
huffman@16747
    23
text {* Exhaustion and Elimination for type @{typ one} *}
huffman@15576
    24
huffman@16747
    25
lemma Exh_one: "t = \<bottom> \<or> t = ONE"
huffman@15576
    26
apply (unfold ONE_def)
huffman@15576
    27
apply (induct t)
huffman@15576
    28
apply simp
huffman@15576
    29
apply simp
huffman@15576
    30
done
huffman@15576
    31
huffman@16747
    32
lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
huffman@15576
    33
apply (rule Exh_one [THEN disjE])
huffman@15576
    34
apply fast
huffman@15576
    35
apply fast
huffman@15576
    36
done
huffman@15576
    37
huffman@16747
    38
lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
huffman@15576
    39
apply (unfold ONE_def)
huffman@16747
    40
apply simp
huffman@15576
    41
done
huffman@15576
    42
huffman@16747
    43
lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
huffman@15576
    44
apply (unfold ONE_def)
huffman@16747
    45
apply simp_all
huffman@15576
    46
done
huffman@15576
    47
huffman@17838
    48
lemma compact_ONE [simp]: "compact ONE"
huffman@17838
    49
by (rule compact_chfin)
huffman@17838
    50
huffman@18080
    51
text {* Case analysis function for type @{typ one} *}
huffman@18080
    52
huffman@18080
    53
constdefs
huffman@18080
    54
  one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a"
huffman@18080
    55
  "one_when \<equiv> \<Lambda> a. strictify\<cdot>(\<Lambda> _. a)"
huffman@18080
    56
huffman@18080
    57
translations
huffman@18080
    58
  "\<Lambda> ONE. t" == "one_when\<cdot>t"
huffman@18080
    59
huffman@18080
    60
lemma one_when1 [simp]: "(\<Lambda> ONE. t)\<cdot>\<bottom> = \<bottom>"
huffman@18080
    61
by (simp add: one_when_def)
huffman@18080
    62
huffman@18080
    63
lemma one_when2 [simp]: "(\<Lambda> ONE. t)\<cdot>ONE = t"
huffman@18080
    64
by (simp add: one_when_def)
huffman@18080
    65
huffman@18080
    66
lemma one_when3 [simp]: "(\<Lambda> ONE. ONE)\<cdot>x = x"
huffman@18080
    67
by (rule_tac p=x in oneE, simp_all)
huffman@18080
    68
nipkow@243
    69
end