author | huffman |
Wed, 08 Jun 2005 00:16:28 +0200 | |
changeset 16316 | 17db5df51a35 |
parent 16211 | faa9691da2bc |
child 16699 | 24b494ff8f0f |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Ssum.thy |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
2 |
ID: $Id$ |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
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 |
|
16070
4a83dd540b88
removed LICENCE note -- everything is subject to Isabelle licence as
wenzelm
parents:
16060
diff
changeset
|
5 |
Strict sum with typedef. |
15576
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 sums *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
|
15577 | 10 |
theory Ssum |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
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 |
|
16083
fca38c55c8fa
added defaultsort declaration, moved cpair_less to Cprod.thy
huffman
parents:
16070
diff
changeset
|
14 |
defaultsort pcpo |
fca38c55c8fa
added defaultsort declaration, moved cpair_less to Cprod.thy
huffman
parents:
16070
diff
changeset
|
15 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
16 |
subsection {* Definition of strict sum type *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
17 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
18 |
typedef (Ssum) ('a, 'b) "++" (infixr 10) = |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
19 |
"{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
20 |
by (rule_tac x="<\<bottom>,\<bottom>>" in exI, simp) |
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" ("(_ \<oplus>/ _)" [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" ("(_ \<oplus>/ _)" [21, 20] 20) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
27 |
subsection {* Class instances *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
28 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
29 |
instance "++" :: (pcpo, pcpo) sq_ord .. |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
30 |
defs (overloaded) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
31 |
less_ssum_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Ssum x \<sqsubseteq> Rep_Ssum y" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
32 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
33 |
lemma adm_Ssum: "adm (\<lambda>x. x \<in> Ssum)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
34 |
by (simp add: Ssum_def cont_fst cont_snd) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
35 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
36 |
lemma UU_Ssum: "\<bottom> \<in> Ssum" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
37 |
by (simp add: Ssum_def inst_cprod_pcpo2) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
38 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
39 |
instance "++" :: (pcpo, pcpo) po |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
40 |
by (rule typedef_po [OF type_definition_Ssum less_ssum_def]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
41 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
42 |
instance "++" :: (pcpo, pcpo) cpo |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
43 |
by (rule typedef_cpo [OF type_definition_Ssum less_ssum_def adm_Ssum]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
44 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
45 |
instance "++" :: (pcpo, pcpo) pcpo |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
46 |
by (rule typedef_pcpo_UU [OF type_definition_Ssum less_ssum_def UU_Ssum]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
47 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
48 |
lemmas cont_Rep_Ssum = |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
49 |
typedef_cont_Rep [OF type_definition_Ssum less_ssum_def adm_Ssum] |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
50 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
51 |
lemmas cont_Abs_Ssum = |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
52 |
typedef_cont_Abs [OF type_definition_Ssum less_ssum_def adm_Ssum] |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
53 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
54 |
lemmas Rep_Ssum_strict = |
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
55 |
typedef_Rep_strict [OF type_definition_Ssum less_ssum_def UU_Ssum] |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
56 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
57 |
lemmas Abs_Ssum_strict = |
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
58 |
typedef_Abs_strict [OF type_definition_Ssum less_ssum_def UU_Ssum] |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
59 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
60 |
lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>" |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
61 |
by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric]) |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
62 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
63 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
64 |
subsection {* Definitions of constructors *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
65 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
66 |
constdefs |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
67 |
sinl :: "'a \<rightarrow> ('a ++ 'b)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
68 |
"sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
69 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
70 |
sinr :: "'b \<rightarrow> ('a ++ 'b)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
71 |
"sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
72 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
73 |
subsection {* Properties of @{term sinl} and @{term sinr} *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
74 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
75 |
lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum <a, \<bottom>>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
76 |
by (unfold sinl_def, simp add: cont_Abs_Ssum Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
77 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
78 |
lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum <\<bottom>, b>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
79 |
by (unfold sinr_def, simp add: cont_Abs_Ssum Ssum_def) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
80 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
81 |
lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = <a, \<bottom>>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
82 |
by (unfold sinl_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
83 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
84 |
lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
85 |
by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
87 |
lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
88 |
by (simp add: sinl_Abs_Ssum UU_Abs_Ssum) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
89 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
90 |
lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
91 |
by (simp add: sinr_Abs_Ssum UU_Abs_Ssum) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
92 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
93 |
lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
94 |
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) |
15606
95617b30514b
simplified some definitions, many proofs are much shorter
huffman
parents:
15600
diff
changeset
|
95 |
apply (simp add: Abs_Ssum_inject Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
96 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
97 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
98 |
lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
99 |
by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
100 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
101 |
lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
102 |
by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
103 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
104 |
lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
105 |
by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
106 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
107 |
lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
108 |
by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
109 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
110 |
lemma sinl_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
111 |
apply (erule contrapos_nn) |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
112 |
apply (rule sinl_inject) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
113 |
apply auto |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
114 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
115 |
|
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
116 |
lemma sinr_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
117 |
apply (erule contrapos_nn) |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
118 |
apply (rule sinr_inject) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
119 |
apply auto |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
120 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
121 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
122 |
subsection {* Case analysis *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
123 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
124 |
lemma Exh_Ssum1: |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
125 |
"z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
126 |
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
127 |
apply (rule_tac x=z in Abs_Ssum_cases) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
128 |
apply (rule_tac p=y in cprodE) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
129 |
apply (auto simp add: Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
130 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
131 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
132 |
lemma ssumE: |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
133 |
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
134 |
\<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q; |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
135 |
\<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
136 |
by (cut_tac z=p in Exh_Ssum1, auto) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
137 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
138 |
lemma ssumE2: |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
139 |
"\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
140 |
apply (rule_tac p=p in ssumE) |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
141 |
apply (simp only: sinl_strict [symmetric]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
142 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
143 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
144 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
145 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
146 |
subsection {* Ordering properties of @{term sinl} and @{term sinr} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
147 |
|
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
148 |
lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
149 |
by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
150 |
|
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
151 |
lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
152 |
by (simp add: less_ssum_def Rep_Ssum_sinr cpair_less) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
153 |
|
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
154 |
lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
155 |
by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
156 |
|
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
157 |
lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)" |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
158 |
by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
159 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
160 |
subsection {* Chains of strict sums *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
161 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
162 |
lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
163 |
apply (rule_tac p=p in ssumE) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
164 |
apply (rule_tac x="\<bottom>" in exI, simp) |
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
165 |
apply (simp add: sinl_less sinl_eq) |
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
166 |
apply (simp add: sinr_less_sinl) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
167 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
168 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
169 |
lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
170 |
apply (rule_tac p=p in ssumE) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
171 |
apply (rule_tac x="\<bottom>" in exI, simp) |
16316
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
172 |
apply (simp add: sinl_less_sinr) |
17db5df51a35
renamed theorems less_ssum4a,b,c,d to more meaningful names
huffman
parents:
16211
diff
changeset
|
173 |
apply (simp add: sinr_less sinr_eq) |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
174 |
done |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
175 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
176 |
lemma ssum_chain_lemma: |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
177 |
"chain Y \<Longrightarrow> (\<exists>A. chain A \<and> Y = (\<lambda>i. sinl\<cdot>(A i))) \<or> |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
178 |
(\<exists>B. chain B \<and> Y = (\<lambda>i. sinr\<cdot>(B i)))" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
179 |
apply (rule_tac p="lub (range Y)" in ssumE2) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
180 |
apply (rule disjI1) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
181 |
apply (rule_tac x="\<lambda>i. cfst\<cdot>(Rep_Ssum (Y i))" in exI) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
182 |
apply (rule conjI) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
183 |
apply (rule chain_monofun) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
184 |
apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
185 |
apply (rule ext, drule_tac x=i in is_ub_thelub, simp) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
186 |
apply (drule less_sinlD, clarify) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
187 |
apply (simp add: sinl_eq Rep_Ssum_sinl) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
188 |
apply (rule disjI2) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
189 |
apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
190 |
apply (rule conjI) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
191 |
apply (rule chain_monofun) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
192 |
apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
193 |
apply (rule ext, drule_tac x=i in is_ub_thelub, simp) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
194 |
apply (drule less_sinrD, clarify) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
195 |
apply (simp add: sinr_eq Rep_Ssum_sinr) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
196 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
197 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
198 |
subsection {* Definitions of constants *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
199 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
200 |
constdefs |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
201 |
Iwhen :: "['a \<rightarrow> 'c, 'b \<rightarrow> 'c, 'a ++ 'b] \<Rightarrow> 'c" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
202 |
"Iwhen \<equiv> \<lambda>f g s. |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
203 |
if cfst\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then f\<cdot>(cfst\<cdot>(Rep_Ssum s)) else |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
204 |
if csnd\<cdot>(Rep_Ssum s) \<noteq> \<bottom> then g\<cdot>(csnd\<cdot>(Rep_Ssum s)) else \<bottom>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
205 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
206 |
text {* rewrites for @{term Iwhen} *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
207 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
208 |
lemma Iwhen1 [simp]: "Iwhen f g \<bottom> = \<bottom>" |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
209 |
by (simp add: Iwhen_def Rep_Ssum_strict) |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
210 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
211 |
lemma Iwhen2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinl\<cdot>x) = f\<cdot>x" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
212 |
by (simp add: Iwhen_def Rep_Ssum_sinl) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
213 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
214 |
lemma Iwhen3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> Iwhen f g (sinr\<cdot>y) = g\<cdot>y" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
215 |
by (simp add: Iwhen_def Rep_Ssum_sinr) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
216 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
217 |
lemma Iwhen4: "Iwhen f g (sinl\<cdot>x) = strictify\<cdot>f\<cdot>x" |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
218 |
by (simp add: strictify_conv_if) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
219 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
220 |
lemma Iwhen5: "Iwhen f g (sinr\<cdot>y) = strictify\<cdot>g\<cdot>y" |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
221 |
by (simp add: strictify_conv_if) |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
222 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
223 |
subsection {* Continuity of @{term Iwhen} *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
224 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
225 |
text {* @{term Iwhen} is continuous in all arguments *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
226 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
227 |
lemma cont_Iwhen1: "cont (\<lambda>f. Iwhen f g s)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
228 |
by (rule_tac p=s in ssumE, simp_all) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
229 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
230 |
lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
231 |
by (rule_tac p=s in ssumE, simp_all) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
232 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
233 |
lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)" |
16211
faa9691da2bc
changed to use new contI; renamed strict, defined, and inject lemmas
huffman
parents:
16083
diff
changeset
|
234 |
apply (rule contI) |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
235 |
apply (drule ssum_chain_lemma, safe) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
236 |
apply (simp add: contlub_cfun_arg [symmetric]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
237 |
apply (simp add: Iwhen4) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
238 |
apply (simp add: contlub_cfun_arg) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
239 |
apply (simp add: thelubE chain_monofun) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
240 |
apply (simp add: contlub_cfun_arg [symmetric]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
241 |
apply (simp add: Iwhen5) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
242 |
apply (simp add: contlub_cfun_arg) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
243 |
apply (simp add: thelubE chain_monofun) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
244 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
245 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
246 |
subsection {* Continuous versions of constants *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
247 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
248 |
constdefs |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
249 |
sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
250 |
"sscase \<equiv> \<Lambda> f g s. Iwhen f g s" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
251 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
252 |
translations |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
253 |
"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
254 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
255 |
text {* continuous versions of lemmas for @{term sscase} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
256 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
257 |
lemma beta_sscase: "sscase\<cdot>f\<cdot>g\<cdot>s = Iwhen f g s" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
258 |
by (simp add: sscase_def cont_Iwhen1 cont_Iwhen2 cont_Iwhen3) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
259 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
260 |
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
261 |
by (simp add: beta_sscase) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
262 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
263 |
lemma sscase2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = f\<cdot>x" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
264 |
by (simp add: beta_sscase) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
265 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
266 |
lemma sscase3 [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sscase\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>y) = g\<cdot>y" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
267 |
by (simp add: beta_sscase) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
268 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
269 |
lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
270 |
by (rule_tac p=z in ssumE, simp_all) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
271 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
272 |
end |