author | wenzelm |
Mon, 01 Jan 2018 23:07:24 +0100 | |
changeset 67312 | 0d25e02759b7 |
parent 62175 | 8ffc4d0e652d |
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 |
|
62175 | 6 |
section \<open>The type of strict products\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
|
15577 | 8 |
theory Sprod |
67312 | 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 |
|
67312 | 14 |
|
62175 | 15 |
subsection \<open>Definition of strict product type\<close> |
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
16 |
|
45695 | 17 |
definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}" |
18 |
||
61998 | 19 |
pcpodef ('a, 'b) sprod ("(_ \<otimes>/ _)" [21,20] 20) = "sprod :: ('a \<times> 'b) set" |
67312 | 20 |
by (simp_all add: sprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
|
35525 | 22 |
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
67312 | 23 |
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
|
24 |
|
61998 | 25 |
type_notation (ASCII) |
26 |
sprod (infixr "**" 20) |
|
61378 | 27 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
|
62175 | 29 |
subsection \<open>Definitions of constants\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
|
67312 | 31 |
definition sfst :: "('a ** 'b) \<rightarrow> 'a" |
32 |
where "sfst = (\<Lambda> p. fst (Rep_sprod p))" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
33 |
|
67312 | 34 |
definition ssnd :: "('a ** 'b) \<rightarrow> 'b" |
35 |
where "ssnd = (\<Lambda> p. snd (Rep_sprod p))" |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
36 |
|
67312 | 37 |
definition spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" |
38 |
where "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
|
39 |
|
67312 | 40 |
definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" |
41 |
where "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
|
42 |
|
67312 | 43 |
syntax "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))") |
44 |
translations |
|
45 |
"(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)" |
|
46 |
"(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y" |
|
41479 | 47 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
48 |
translations |
67312 | 49 |
"\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" \<rightleftharpoons> "CONST ssplit\<cdot>(\<Lambda> x y. t)" |
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
|
50 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
51 |
|
62175 | 52 |
subsection \<open>Case analysis\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
53 |
|
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
54 |
lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod" |
67312 | 55 |
by (simp add: sprod_def seq_conv_if) |
40083 | 56 |
|
40767
a3e505b236e7
rename function 'strict' to 'seq', which is its name in Haskell
huffman
parents:
40502
diff
changeset
|
57 |
lemma Rep_sprod_spair: "Rep_sprod (:a, b:) = (seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b)" |
67312 | 58 |
by (simp add: spair_def cont_Abs_sprod Abs_sprod_inverse spair_sprod) |
40080 | 59 |
|
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
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
Rep_sprod_strict Rep_sprod_spair |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
64 |
|
35783 | 65 |
lemma sprodE [case_names bottom spair, cases type: sprod]: |
40080 | 66 |
obtains "p = \<bottom>" | x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>" |
67312 | 67 |
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
|
68 |
|
35783 | 69 |
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
|
70 |
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x" |
67312 | 71 |
by (cases x) simp_all |
72 |
||
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
73 |
|
62175 | 74 |
subsection \<open>Properties of \emph{spair}\<close> |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
75 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
76 |
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>" |
67312 | 77 |
by (simp add: Rep_sprod_simps) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
78 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
79 |
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" |
67312 | 80 |
by (simp add: Rep_sprod_simps) |
25914 | 81 |
|
67312 | 82 |
lemma spair_bottom_iff [simp]: "(:x, y:) = \<bottom> \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom>" |
83 |
by (simp add: Rep_sprod_simps seq_conv_if) |
|
25914 | 84 |
|
67312 | 85 |
lemma spair_below_iff: "(:a, b:) \<sqsubseteq> (:c, d:) \<longleftrightarrow> a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)" |
86 |
by (simp add: Rep_sprod_simps seq_conv_if) |
|
25914 | 87 |
|
67312 | 88 |
lemma spair_eq_iff: "(:a, b:) = (:c, d:) \<longleftrightarrow> a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>)" |
89 |
by (simp add: Rep_sprod_simps seq_conv_if) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
90 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
91 |
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>" |
67312 | 92 |
by simp |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
93 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
94 |
lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
67312 | 95 |
by simp |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
96 |
|
25914 | 97 |
lemma spair_defined: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" |
67312 | 98 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
99 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
100 |
lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>" |
67312 | 101 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
102 |
|
67312 | 103 |
lemma spair_below: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) \<longleftrightarrow> x \<sqsubseteq> a \<and> y \<sqsubseteq> b" |
104 |
by (simp add: spair_below_iff) |
|
40095 | 105 |
|
67312 | 106 |
lemma spair_eq: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> (:x, y:) = (:a, b:) \<longleftrightarrow> x = a \<and> y = b" |
107 |
by (simp add: spair_eq_iff) |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
108 |
|
67312 | 109 |
lemma spair_inject: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> (:x, y:) = (:a, b:) \<Longrightarrow> x = a \<and> y = b" |
110 |
by (rule spair_eq [THEN iffD1]) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
111 |
|
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
40774
diff
changeset
|
112 |
lemma inst_sprod_pcpo2: "\<bottom> = (:\<bottom>, \<bottom>:)" |
67312 | 113 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
114 |
|
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset
|
115 |
lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q" |
67312 | 116 |
by (cases p) (simp only: inst_sprod_pcpo2, simp) |
117 |
||
33504
b4210cc3ac97
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
huffman
parents:
32960
diff
changeset
|
118 |
|
62175 | 119 |
subsection \<open>Properties of \emph{sfst} and \emph{ssnd}\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
120 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
121 |
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>" |
67312 | 122 |
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
|
123 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
124 |
lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>" |
67312 | 125 |
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
|
126 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
127 |
lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x" |
67312 | 128 |
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
|
129 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
130 |
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y" |
67312 | 131 |
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
|
132 |
|
67312 | 133 |
lemma sfst_bottom_iff [simp]: "sfst\<cdot>p = \<bottom> \<longleftrightarrow> p = \<bottom>" |
134 |
by (cases p) simp_all |
|
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
135 |
|
67312 | 136 |
lemma ssnd_bottom_iff [simp]: "ssnd\<cdot>p = \<bottom> \<longleftrightarrow> p = \<bottom>" |
137 |
by (cases p) simp_all |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
138 |
|
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
139 |
lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>" |
67312 | 140 |
by simp |
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
141 |
|
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
142 |
lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>" |
67312 | 143 |
by simp |
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
144 |
|
40094
0295606b6a36
rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd
huffman
parents:
40093
diff
changeset
|
145 |
lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p" |
67312 | 146 |
by (cases p) simp_all |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
147 |
|
67312 | 148 |
lemma below_sprod: "x \<sqsubseteq> y \<longleftrightarrow> sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y" |
149 |
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
|
150 |
|
67312 | 151 |
lemma eq_sprod: "x = y \<longleftrightarrow> sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y" |
152 |
by (auto simp add: po_eq_conv below_sprod) |
|
16751 | 153 |
|
40436 | 154 |
lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:y, ssnd\<cdot>x:)" |
67312 | 155 |
by (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp, simp add: below_sprod) |
25881 | 156 |
|
40436 | 157 |
lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:sfst\<cdot>x, y:)" |
67312 | 158 |
by (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp, simp add: below_sprod) |
159 |
||
25881 | 160 |
|
62175 | 161 |
subsection \<open>Compactness\<close> |
25881 | 162 |
|
163 |
lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)" |
|
67312 | 164 |
by (rule compactI) (simp add: sfst_below_iff) |
25881 | 165 |
|
166 |
lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)" |
|
67312 | 167 |
by (rule compactI) (simp add: ssnd_below_iff) |
25881 | 168 |
|
67312 | 169 |
lemma compact_spair: "compact x \<Longrightarrow> compact y \<Longrightarrow> compact (:x, y:)" |
170 |
by (rule compact_sprod) (simp add: Rep_sprod_spair seq_conv_if) |
|
25881 | 171 |
|
67312 | 172 |
lemma compact_spair_iff: "compact (:x, y:) \<longleftrightarrow> x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y)" |
173 |
apply (safe elim!: compact_spair) |
|
174 |
apply (drule compact_sfst, simp) |
|
175 |
apply (drule compact_ssnd, simp) |
|
176 |
apply simp |
|
177 |
apply simp |
|
178 |
done |
|
179 |
||
25881 | 180 |
|
62175 | 181 |
subsection \<open>Properties of \emph{ssplit}\<close> |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
182 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
183 |
lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>" |
67312 | 184 |
by (simp add: ssplit_def) |
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
185 |
|
67312 | 186 |
lemma ssplit2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y" |
187 |
by (simp add: ssplit_def) |
|
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
188 |
|
16553 | 189 |
lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z" |
67312 | 190 |
by (cases z) simp_all |
191 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
192 |
|
62175 | 193 |
subsection \<open>Strict product preserves flatness\<close> |
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
194 |
|
35525 | 195 |
instance sprod :: (flat, flat) flat |
27310 | 196 |
proof |
197 |
fix x y :: "'a \<otimes> 'b" |
|
67312 | 198 |
assume "x \<sqsubseteq> y" |
199 |
then show "x = \<bottom> \<or> x = y" |
|
27310 | 200 |
apply (induct x, simp) |
201 |
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
|
202 |
apply (simp add: spair_below_iff flat_below_iff) |
27310 | 203 |
done |
204 |
qed |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
205 |
|
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
25914
diff
changeset
|
206 |
end |