equal
deleted
inserted
replaced
6 Partial ordering for cartesian product of HOL theory prod.thy |
6 Partial ordering for cartesian product of HOL theory prod.thy |
7 *) |
7 *) |
8 |
8 |
9 header {* The cpo of cartesian products *} |
9 header {* The cpo of cartesian products *} |
10 |
10 |
11 theory Cprod = Cfun: |
11 theory Cprod |
|
12 imports Cfun |
|
13 begin |
12 |
14 |
13 defaultsort cpo |
15 defaultsort cpo |
14 |
16 |
15 instance "*"::(sq_ord,sq_ord)sq_ord .. |
17 instance "*"::(sq_ord,sq_ord)sq_ord .. |
16 |
18 |
229 "LAM <x,y,zs>.b" == "csplit$(LAM x. LAM <y,zs>.b)" |
231 "LAM <x,y,zs>.b" == "csplit$(LAM x. LAM <y,zs>.b)" |
230 "LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)" |
232 "LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)" |
231 "LAM <x,y>.b" == "csplit$(LAM x y. b)" |
233 "LAM <x,y>.b" == "csplit$(LAM x y. b)" |
232 |
234 |
233 syntax (xsymbols) |
235 syntax (xsymbols) |
234 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\\<Lambda>()<_>./ _)" [0, 10] 10) |
236 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10) |
235 |
237 |
236 (* for compatibility with old HOLCF-Version *) |
238 (* for compatibility with old HOLCF-Version *) |
237 lemma inst_cprod_pcpo: "UU = (UU,UU)" |
239 lemma inst_cprod_pcpo: "UU = (UU,UU)" |
238 apply (simp add: UU_cprod_def[folded UU_def]) |
240 apply (simp add: UU_cprod_def[folded UU_def]) |
239 done |
241 done |