src/HOL/HOLCF/One.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46125 00cd193a48dc
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41295
diff changeset
     1
(*  Title:      HOL/HOLCF/One.thy
2640
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"
46125
00cd193a48dc improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents: 42151
diff changeset
    61
  "case x of XCONST ONE :: 'a \<Rightarrow> t" => "CONST one_case\<cdot>t\<cdot>x"
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    62
  "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t"
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    63
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    64
lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    65
by (simp add: one_case_def)
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    66
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    67
lemma one_case2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    68
by (simp add: one_case_def)
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    69
40212
20df78048db5 rename constant 'one_when' to 'one_case'
huffman
parents: 40046
diff changeset
    70
lemma one_case3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
27293
de9a2fd0eab4 added some lemmas; tuned proofs
huffman
parents: 25131
diff changeset
    71
by (induct x rule: one_induct) simp_all
18080
c1a7490ee3ff add constant one_when; LAM pattern for ONE
huffman
parents: 17838
diff changeset
    72
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    73
end