src/HOL/HOLCF/One.thy
author huffman
Sun, 19 Dec 2010 18:11:20 -0800
changeset 41295 5b5388d4ccc9
parent 41182 717404c7d59a
child 42151 4da4fc77664b
permissions -rw-r--r--
types -> type_synonym
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2275
diff changeset
     1
(*  Title:      HOLCF/One.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2275
diff changeset
     2
    Author:     Oscar Slotosch
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     3
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     5
header {* The unit domain *}
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     6
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     7
theory One
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     8
imports Lift
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     9
begin
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
41295
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    11
type_synonym
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    12
  one = "unit lift"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
41295
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    14
translations
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    15
  (type) "one" <= (type) "unit lift"
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    16
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    17
definition ONE :: "one"
5b5388d4ccc9 types -> type_synonym
huffman
parents: 41182
diff changeset
    18
  where "ONE == Def ()"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
16747
934b6b36d794 cleaned up
huffman
parents: 16070
diff changeset
    20
text {* Exhaustion and Elimination for type @{typ one} *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    21
16747
934b6b36d794 cleaned up
huffman
parents: 16070
diff changeset
    22
lemma Exh_one: "t = \<bottom> \<or> t = ONE"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    23
unfolding ONE_def by (induct t) simp_all
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    24
35783
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35431
diff changeset
    25
lemma oneE [case_names bottom ONE]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    26
unfolding ONE_def by (induct p) simp_all
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    27
35783
38538bfe9ca6 declare case_names for various induction rules
huffman
parents: 35431
diff changeset
    28
lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    29
by (cases x rule: oneE) simp_all
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    30
41182
717404c7d59a add notsqsubseteq syntax
huffman
parents: 40774
diff changeset
    31
lemma dist_below_one [simp]: "ONE \<notsqsubseteq> \<bottom>"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    32
unfolding ONE_def by simp
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    33
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30911
diff changeset
    34
lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    35
by (induct x rule: one_induct) simp_all
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    36
31076
99fe356cbbc2 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents: 30911
diff changeset
    37
lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    38
by (induct x rule: one_induct) simp_all
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    39
30911
7809cbaa1b61 domain package: simplify internal proofs of con_rews
huffman
parents: 29141
diff changeset
    40
lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
7809cbaa1b61 domain package: simplify internal proofs of con_rews
huffman
parents: 29141
diff changeset
    41
unfolding ONE_def by simp
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents: 14981
diff changeset
    42
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    43
lemma one_neq_iffs [simp]:
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    44
  "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    45
  "ONE \<noteq> x \<longleftrightarrow> x = \<bottom>"
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    46
  "x \<noteq> \<bottom> \<longleftrightarrow> x = ONE"
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    47
  "\<bottom> \<noteq> x \<longleftrightarrow> x = ONE"
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    48
by (induct x rule: one_induct) simp_all
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    49
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    50
lemma compact_ONE: "compact ONE"
17838
3032e90c4975 added compactness theorems
huffman
parents: 16747
diff changeset
    51
by (rule compact_chfin)
3032e90c4975 added compactness theorems
huffman
parents: 16747
diff changeset
    52
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    53
text {* Case analysis function for type @{typ one} *}
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    54
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18111
diff changeset
    55
definition
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    56
  one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
40767
a3e505b236e7 rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents: 40212
diff changeset
    57
  "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)"
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    58
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    59
translations
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    60
  "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    61
  "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t"
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    62
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    63
lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    64
by (simp add: one_case_def)
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    65
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    66
lemma one_case2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    67
by (simp add: one_case_def)
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    68
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    69
lemma one_case3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    70
by (induct x rule: one_induct) simp_all
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    71
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    72
end