author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58880 | 0baae4311a9f |
child 61378 | 3e04c9ca001a |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Sprod.thy |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40436
diff
changeset
|
2 |
Author: Franz Regensburger |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40436
diff
changeset
|
3 |
Author: Brian Huffman |
15576
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 |
|
58880 | 6 |
section {* The type of strict products *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
|
15577 | 8 |
theory Sprod |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40436
diff
changeset
|
9 |
imports Cfun |
15577 | 10 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
|
36452 | 12 |
default_sort pcpo |
16082 | 13 |
|
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
14 |
subsection {* Definition of strict product type *} |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
15 |
|
45695 | 16 |
definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}" |
17 |
||
49759
ecf1d5d87e5e
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
huffman
parents:
45695
diff
changeset
|
18 |
pcpodef ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set" |
45695 | 19 |
unfolding sprod_def by simp_all |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
|
35525 | 21 |
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
22 |
by (rule typedef_chfin [OF type_definition_sprod below_sprod_def]) |
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
23 |
|
35427 | 24 |
type_notation (xsymbols) |
35547 | 25 |
sprod ("(_ \<otimes>/ _)" [21,20] 20) |
35427 | 26 |
type_notation (HTML output) |
35547 | 27 |
sprod ("(_ \<otimes>/ _)" [21,20] 20) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
29 |
subsection {* Definitions of constants *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
31 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
32 |
sfst :: "('a ** 'b) \<rightarrow> 'a" where |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
33 |
"sfst = (\<Lambda> p. fst (Rep_sprod p))" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
34 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
35 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
36 |
ssnd :: "('a ** 'b) \<rightarrow> 'b" where |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
37 |
"ssnd = (\<Lambda> p. snd (Rep_sprod p))" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
39 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
40 |
spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where |
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
41 |
"spair = (\<Lambda> a b. Abs_sprod (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b))" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
43 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
44 |
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where |
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
45 |
"ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
46 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
47 |
syntax |
41479 | 48 |
"_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))") |
49 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
50 |
translations |
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
51 |
"(:x, y, z:)" == "(:x, (:y, z:):)" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18078
diff
changeset
|
52 |
"(:x, y:)" == "CONST spair\<cdot>x\<cdot>y" |
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
53 |
|
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
54 |
translations |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18078
diff
changeset
|
55 |
"\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
56 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
57 |
subsection {* Case analysis *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
58 |
|
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
59 |
lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod" |
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
60 |
by (simp add: sprod_def seq_conv_if) |
40083 | 61 |
|
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
62 |
lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
63 |
by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) |
40080 | 64 |
|
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
65 |
lemmas Rep_sprod_simps = |
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
66 |
Rep_sprod_inject [symmetric] below_sprod_def |
44066
d74182c93f04
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
huffman
parents:
42151
diff
changeset
|
67 |
prod_eq_iff below_prod_def |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
68 |
Rep_sprod_strict Rep_sprod_spair |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
69 |
|
35783 | 70 |
lemma sprodE [case_names bottom spair, cases type: sprod]: |
40080 | 71 |
obtains "p = \<bottom>" | x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
72 |
using Rep_sprod [of p] by (auto simp add: sprod_def Rep_sprod_simps) |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
73 |
|
35783 | 74 |
lemma sprod_induct [case_names bottom spair, induct type: sprod]: |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
75 |
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x" |
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
76 |
by (cases x, simp_all) |
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
77 |
|
35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35783
diff
changeset
|
78 |
subsection {* Properties of \emph{spair} *} |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
79 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
80 |
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
81 |
by (simp add: Rep_sprod_simps) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
82 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
83 |
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
84 |
by (simp add: Rep_sprod_simps) |
25914 | 85 |
|
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40098
diff
changeset
|
86 |
lemma spair_bottom_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)" |
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
87 |
by (simp add: Rep_sprod_simps seq_conv_if) |
25914 | 88 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
89 |
lemma spair_below_iff: |
25914 | 90 |
"((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))" |
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
91 |
by (simp add: Rep_sprod_simps seq_conv_if) |
25914 | 92 |
|
93 |
lemma spair_eq_iff: |
|
94 |
"((:a, b:) = (:c, d:)) = |
|
95 |
(a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))" |
|
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
96 |
by (simp add: Rep_sprod_simps seq_conv_if) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
97 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
98 |
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>" |
25914 | 99 |
by simp |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
100 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
101 |
lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
25914 | 102 |
by simp |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
103 |
|
25914 | 104 |
lemma spair_defined: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" |
105 |
by simp |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
106 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
107 |
lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>" |
25914 | 108 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
109 |
|
40095 | 110 |
lemma spair_below: |
111 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)" |
|
112 |
by (simp add: spair_below_iff) |
|
113 |
||
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
114 |
lemma spair_eq: |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
115 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)" |
25914 | 116 |
by (simp add: spair_eq_iff) |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
117 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
118 |
lemma spair_inject: |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
119 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b" |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
120 |
by (rule spair_eq [THEN iffD1]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
121 |
|
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40774
diff
changeset
|
122 |
lemma inst_sprod_pcpo2: "\<bottom> = (:\<bottom>, \<bottom>:)" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
123 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
124 |
|
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset
|
125 |
lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q" |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset
|
126 |
by (cases p, simp only: inst_sprod_pcpo2, simp) |
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset
|
127 |
|
35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35783
diff
changeset
|
128 |
subsection {* Properties of \emph{sfst} and \emph{ssnd} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
129 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
130 |
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
131 |
by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
132 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
133 |
lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
134 |
by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_strict) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
135 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
136 |
lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
137 |
by (simp add: sfst_def cont_Rep_sprod Rep_sprod_spair) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
138 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
139 |
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
140 |
by (simp add: ssnd_def cont_Rep_sprod Rep_sprod_spair) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
141 |
|
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40098
diff
changeset
|
142 |
lemma sfst_bottom_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
143 |
by (cases p, simp_all) |
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
144 |
|
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40098
diff
changeset
|
145 |
lemma ssnd_bottom_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
146 |
by (cases p, simp_all) |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
147 |
|
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
148 |
lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>" |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
149 |
by simp |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
150 |
|
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
151 |
lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>" |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
152 |
by simp |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
153 |
|
40094
0295606b6a36
rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd
huffman
parents:
40093
diff
changeset
|
154 |
lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
155 |
by (cases p, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
156 |
|
40436 | 157 |
lemma below_sprod: "(x \<sqsubseteq> y) = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)" |
40098
9dbb01456031
use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum
huffman
parents:
40095
diff
changeset
|
158 |
by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod) |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
159 |
|
16751 | 160 |
lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
161 |
by (auto simp add: po_eq_conv below_sprod) |
16751 | 162 |
|
40436 | 163 |
lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:y, ssnd\<cdot>x:)" |
25881 | 164 |
apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp) |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
165 |
apply (simp add: below_sprod) |
25881 | 166 |
done |
167 |
||
40436 | 168 |
lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:sfst\<cdot>x, y:)" |
25881 | 169 |
apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp) |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
170 |
apply (simp add: below_sprod) |
25881 | 171 |
done |
172 |
||
173 |
subsection {* Compactness *} |
|
174 |
||
175 |
lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
176 |
by (rule compactI, simp add: sfst_below_iff) |
25881 | 177 |
|
178 |
lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
179 |
by (rule compactI, simp add: ssnd_below_iff) |
25881 | 180 |
|
181 |
lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)" |
|
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
182 |
by (rule compact_sprod, simp add: Rep_sprod_spair seq_conv_if) |
25881 | 183 |
|
184 |
lemma compact_spair_iff: |
|
185 |
"compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))" |
|
186 |
apply (safe elim!: compact_spair) |
|
187 |
apply (drule compact_sfst, simp) |
|
188 |
apply (drule compact_ssnd, simp) |
|
189 |
apply simp |
|
190 |
apply simp |
|
191 |
done |
|
192 |
||
35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35783
diff
changeset
|
193 |
subsection {* Properties of \emph{ssplit} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
194 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
195 |
lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>" |
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
196 |
by (simp add: ssplit_def) |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
197 |
|
16920 | 198 |
lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y" |
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
199 |
by (simp add: ssplit_def) |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
200 |
|
16553 | 201 |
lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
202 |
by (cases z, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
203 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
204 |
subsection {* Strict product preserves flatness *} |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
205 |
|
35525 | 206 |
instance sprod :: (flat, flat) flat |
27310 | 207 |
proof |
208 |
fix x y :: "'a \<otimes> 'b" |
|
209 |
assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y" |
|
210 |
apply (induct x, simp) |
|
211 |
apply (induct y, simp) |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29138
diff
changeset
|
212 |
apply (simp add: spair_below_iff flat_below_iff) |
27310 | 213 |
done |
214 |
qed |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
215 |
|
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
25914
diff
changeset
|
216 |
end |