src/HOL/HOLCF/Cprod.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45786 3f07a7a91180
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: 40774
diff changeset
     1
(*  Title:      HOL/HOLCF/Cprod.thy
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     2
    Author:     Franz Regensburger
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     3
*)
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     4
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     5
header {* The cpo of cartesian products *}
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
     6
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     7
theory Cprod
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents: 40002
diff changeset
     8
imports Cfun
15577
e16da3068ad6 fix headers
huffman
parents: 15576
diff changeset
     9
begin
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    10
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35926
diff changeset
    11
default_sort cpo
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    12
35900
aa5dfb03eb1e remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents: 33399
diff changeset
    13
subsection {* Continuous case function for unit type *}
16008
861a255cf1e7 pcpo instance for type unit
huffman
parents: 15609
diff changeset
    14
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18289
diff changeset
    15
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18289
diff changeset
    16
  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18289
diff changeset
    17
  "unit_when = (\<Lambda> a _. a)"
16008
861a255cf1e7 pcpo instance for type unit
huffman
parents: 15609
diff changeset
    18
18289
56ddf617d6e8 add constant unit_when
huffman
parents: 18078
diff changeset
    19
translations
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18289
diff changeset
    20
  "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
18289
56ddf617d6e8 add constant unit_when
huffman
parents: 18078
diff changeset
    21
56ddf617d6e8 add constant unit_when
huffman
parents: 18078
diff changeset
    22
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
56ddf617d6e8 add constant unit_when
huffman
parents: 18078
diff changeset
    23
by (simp add: unit_when_def)
56ddf617d6e8 add constant unit_when
huffman
parents: 18078
diff changeset
    24
35926
e6aec5d665f0 completely remove constants cpair, cfst, csnd
huffman
parents: 35922
diff changeset
    25
subsection {* Continuous version of split function *}
17834
28414668b43d added xsymbols syntax for pairs; cleaned up
huffman
parents: 17816
diff changeset
    26
25131
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18289
diff changeset
    27
definition
2c8caac48ade modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents: 18289
diff changeset
    28
  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
35922
bfa52a972745 define csplit using fst, snd
huffman
parents: 35900
diff changeset
    29
  "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    30
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    31
translations
35926
e6aec5d665f0 completely remove constants cpair, cfst, csnd
huffman
parents: 35922
diff changeset
    32
  "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
17816
9942c5ed866a new syntax translations for continuous lambda abstraction
huffman
parents: 16916
diff changeset
    33
45786
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations
huffman
parents: 42151
diff changeset
    34
abbreviation
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations
huffman
parents: 42151
diff changeset
    35
  cfst :: "'a \<times> 'b \<rightarrow> 'a" where
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations
huffman
parents: 42151
diff changeset
    36
  "cfst \<equiv> Abs_cfun fst"
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations
huffman
parents: 42151
diff changeset
    37
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations
huffman
parents: 42151
diff changeset
    38
abbreviation
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations
huffman
parents: 42151
diff changeset
    39
  csnd :: "'a \<times> 'b \<rightarrow> 'b" where
3f07a7a91180 reinstate old functions cfst and csnd as abbreviations
huffman
parents: 42151
diff changeset
    40
  "csnd \<equiv> Abs_cfun snd"
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    41
15593
24d770bbc44a reordered and arranged for document generation, cleaned up some proofs
huffman
parents: 15577
diff changeset
    42
subsection {* Convert all lemmas to the continuous versions *}
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    43
18077
f1f4f951ec8d make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents: 17837
diff changeset
    44
lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
f1f4f951ec8d make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents: 17837
diff changeset
    45
by (simp add: csplit_def)
f1f4f951ec8d make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents: 17837
diff changeset
    46
33399
768b2bb9e66a add (LAM (x, y). t) syntax and lemma csplit_Pair
huffman
parents: 31113
diff changeset
    47
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
35922
bfa52a972745 define csplit using fst, snd
huffman
parents: 35900
diff changeset
    48
by (simp add: csplit_def)
33399
768b2bb9e66a add (LAM (x, y). t) syntax and lemma csplit_Pair
huffman
parents: 31113
diff changeset
    49
15576
efb95d0d01f7 converted to new-style theories, and combined numbered files
huffman
parents:
diff changeset
    50
end