author | wenzelm |
Tue, 21 Jun 2005 09:51:59 +0200 | |
changeset 16513 | f38693aad717 |
parent 16317 | 868eddbcaf6e |
child 16553 | aa36d41e4263 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Sprod.thy |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
2 |
ID: $Id$ |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
3 |
Author: Franz Regensburger and 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 |
Strict product with typedef. |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
8 |
header {* The type of strict products *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
|
15577 | 10 |
theory Sprod |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
11 |
imports Cprod TypedefPcpo |
15577 | 12 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
|
16082 | 14 |
defaultsort pcpo |
15 |
||
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
16 |
subsection {* Definition of strict product type *} |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
17 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
18 |
typedef (Sprod) ('a, 'b) "**" (infixr 20) = |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
19 |
"{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
20 |
by (auto simp add: inst_cprod_pcpo) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
syntax (xsymbols) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
23 |
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
24 |
syntax (HTML output) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
25 |
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
27 |
subsection {* Class instances *} |
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 |
instance "**" :: (pcpo, pcpo) sq_ord .. |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
30 |
defs (overloaded) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
31 |
less_sprod_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Sprod x \<sqsubseteq> Rep_Sprod y" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
33 |
lemma adm_Sprod: "adm (\<lambda>x. x \<in> Sprod)" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
34 |
by (simp add: Sprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
35 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
36 |
lemma UU_Sprod: "\<bottom> \<in> Sprod" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
37 |
by (simp add: Sprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
39 |
instance "**" :: (pcpo, pcpo) po |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
40 |
by (rule typedef_po [OF type_definition_Sprod less_sprod_def]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
41 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
42 |
instance "**" :: (pcpo, pcpo) cpo |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
43 |
by (rule typedef_cpo [OF type_definition_Sprod less_sprod_def adm_Sprod]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
44 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
45 |
instance "**" :: (pcpo, pcpo) pcpo |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
46 |
by (rule typedef_pcpo_UU [OF type_definition_Sprod less_sprod_def UU_Sprod]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
47 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
48 |
lemmas cont_Rep_Sprod = |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
49 |
typedef_cont_Rep [OF type_definition_Sprod less_sprod_def adm_Sprod] |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
50 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
51 |
lemmas cont_Abs_Sprod = |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
52 |
typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod] |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
53 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
54 |
lemmas Rep_Sprod_strict = |
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
55 |
typedef_Rep_strict [OF type_definition_Sprod less_sprod_def UU_Sprod] |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
56 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
57 |
lemmas Abs_Sprod_strict = |
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
58 |
typedef_Abs_strict [OF type_definition_Sprod less_sprod_def UU_Sprod] |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
59 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
60 |
lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>" |
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
61 |
by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
62 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
63 |
lemma spair_lemma: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
64 |
"<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod" |
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
65 |
by (simp add: Sprod_def strictify_conv_if cpair_strict) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
66 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
67 |
subsection {* Definitions of constants *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
68 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
69 |
consts |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
70 |
sfst :: "('a ** 'b) \<rightarrow> 'a" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
71 |
ssnd :: "('a ** 'b) \<rightarrow> 'b" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
72 |
spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
73 |
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
74 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
75 |
defs |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
76 |
sfst_def: "sfst \<equiv> \<Lambda> p. cfst\<cdot>(Rep_Sprod p)" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
77 |
ssnd_def: "ssnd \<equiv> \<Lambda> p. csnd\<cdot>(Rep_Sprod p)" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
78 |
spair_def: "spair \<equiv> \<Lambda> a b. Abs_Sprod |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
79 |
<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
80 |
ssplit_def: "ssplit \<equiv> \<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p))" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
81 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
82 |
syntax |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
83 |
"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
84 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
85 |
translations |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
"(:x, y, z:)" == "(:x, (:y, z:):)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
87 |
"(:x, y:)" == "spair$x$y" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
88 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
89 |
subsection {* Case analysis *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
90 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
91 |
lemma spair_Abs_Sprod: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
92 |
"(:a, b:) = Abs_Sprod <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
93 |
apply (unfold spair_def) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
94 |
apply (simp add: cont_Abs_Sprod spair_lemma) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
95 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
96 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
97 |
lemma Exh_Sprod2: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
98 |
"z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
99 |
apply (rule_tac x=z in Abs_Sprod_cases) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
100 |
apply (simp add: Sprod_def) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
101 |
apply (erule disjE) |
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
102 |
apply (simp add: Abs_Sprod_strict) |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
103 |
apply (rule disjI2) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
104 |
apply (rule_tac x="cfst\<cdot>y" in exI) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
105 |
apply (rule_tac x="csnd\<cdot>y" in exI) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
106 |
apply (simp add: spair_Abs_Sprod Abs_Sprod_inject spair_lemma) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
107 |
apply (simp add: surjective_pairing_Cprod2) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
108 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
109 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
110 |
lemma sprodE: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
111 |
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
112 |
by (cut_tac z=p in Exh_Sprod2, auto) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
113 |
|
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
114 |
subsection {* Properties of @{term spair} *} |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
115 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
116 |
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>" |
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
117 |
by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
118 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
119 |
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" |
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
120 |
by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
121 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
122 |
lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
123 |
by auto |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
124 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
125 |
lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
126 |
by (erule contrapos_np, auto) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
127 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
128 |
lemma spair_defined [simp]: |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
129 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
130 |
apply (simp add: spair_Abs_Sprod UU_Abs_Sprod) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
131 |
apply (subst Abs_Sprod_inject) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
132 |
apply (simp add: Sprod_def) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
133 |
apply (simp add: Sprod_def inst_cprod_pcpo2) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
134 |
apply simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
135 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
136 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
137 |
lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
138 |
by (erule contrapos_pp, simp) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
139 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
140 |
lemma spair_eq: |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
141 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)" |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
142 |
apply (simp add: spair_Abs_Sprod) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
143 |
apply (simp add: Abs_Sprod_inject [OF _ spair_lemma] Sprod_def) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
144 |
apply (simp add: strictify_conv_if) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
145 |
done |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
146 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
147 |
lemma spair_inject: |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
148 |
"\<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
|
149 |
by (rule spair_eq [THEN iffD1]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
150 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
151 |
lemma inst_sprod_pcpo2: "UU = (:UU,UU:)" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
152 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
153 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
154 |
subsection {* Properties of @{term sfst} and @{term ssnd} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
155 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
156 |
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>" |
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
157 |
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
|
158 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
159 |
lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>" |
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
160 |
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
|
161 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
162 |
lemma Rep_Sprod_spair: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
163 |
"Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
164 |
apply (unfold spair_def) |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
165 |
apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
166 |
done |
15591
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
167 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
168 |
lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
169 |
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
|
170 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
171 |
lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
172 |
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
|
173 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
174 |
lemma sfstssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom> \<and> ssnd\<cdot>p \<noteq> \<bottom>" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
175 |
by (rule_tac p=p in sprodE, simp_all) |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
176 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
177 |
lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
178 |
by (rule_tac p=p in sprodE, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
179 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
180 |
lemma less_sprod: "p1 \<sqsubseteq> p2 = (sfst\<cdot>p1 \<sqsubseteq> sfst\<cdot>p2 \<and> ssnd\<cdot>p1 \<sqsubseteq> ssnd\<cdot>p2)" |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
181 |
apply (simp add: less_sprod_def sfst_def ssnd_def cont_Rep_Sprod) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
182 |
apply (rule less_cprod) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
183 |
done |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
184 |
|
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
185 |
lemma spair_less: |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
186 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)" |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
187 |
apply (case_tac "a = \<bottom>") |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
188 |
apply (simp add: eq_UU_iff [symmetric]) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
189 |
apply (case_tac "b = \<bottom>") |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
190 |
apply (simp add: eq_UU_iff [symmetric]) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
191 |
apply (simp add: less_sprod) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
192 |
done |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
193 |
|
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
194 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
195 |
subsection {* Properties of @{term ssplit} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
196 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
197 |
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
|
198 |
by (simp add: ssplit_def) |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
199 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
200 |
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
|
201 |
by (simp add: ssplit_def) |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
202 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
203 |
lemma ssplit3: "ssplit\<cdot>spair\<cdot>z = z" |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
204 |
by (rule_tac p=z in sprodE, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
205 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
206 |
end |