src/HOLCF/One.thy
author huffman
Thu Jul 07 20:41:12 2005 +0200 (2005-07-07)
changeset 16747 934b6b36d794
parent 16070 4a83dd540b88
child 17838 3032e90c4975
permissions -rw-r--r--
cleaned up
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
nipkow@243
    48
end