author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 16070 | 4a83dd540b88 |
child 16083 | fca38c55c8fa |
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 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
14 |
subsection {* Definition of strict sum type *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
15 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
16 |
typedef (Ssum) ('a, 'b) "++" (infixr 10) = |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
17 |
"{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
|
18 |
by (rule_tac x="<\<bottom>,\<bottom>>" in exI, simp) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
19 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
syntax (xsymbols) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
syntax (HTML output) |
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 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
25 |
subsection {* Class instances *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
26 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
27 |
instance "++" :: (pcpo, pcpo) sq_ord .. |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
28 |
defs (overloaded) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
29 |
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
|
30 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
31 |
lemma adm_Ssum: "adm (\<lambda>x. x \<in> Ssum)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
32 |
by (simp add: Ssum_def cont_fst cont_snd) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
33 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
34 |
lemma UU_Ssum: "\<bottom> \<in> Ssum" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
35 |
by (simp add: Ssum_def inst_cprod_pcpo2) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
36 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
37 |
instance "++" :: (pcpo, pcpo) po |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
38 |
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
|
39 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
40 |
instance "++" :: (pcpo, pcpo) cpo |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
41 |
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
|
42 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
43 |
instance "++" :: (pcpo, pcpo) pcpo |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
44 |
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
|
45 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
46 |
lemmas cont_Rep_Ssum = |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
47 |
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
|
48 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
49 |
lemmas cont_Abs_Ssum = |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
50 |
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
|
51 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
52 |
lemmas strict_Rep_Ssum = |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
53 |
typedef_strict_Rep [OF type_definition_Ssum less_ssum_def UU_Ssum] |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
54 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
55 |
lemmas strict_Abs_Ssum = |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
56 |
typedef_strict_Abs [OF type_definition_Ssum less_ssum_def UU_Ssum] |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
57 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
58 |
lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
59 |
by (simp add: strict_Abs_Ssum inst_cprod_pcpo2 [symmetric]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
60 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
61 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
62 |
subsection {* Definitions of constructors *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
63 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
64 |
constdefs |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
65 |
sinl :: "'a \<rightarrow> ('a ++ 'b)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
66 |
"sinl \<equiv> \<Lambda> a. Abs_Ssum <a, \<bottom>>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
67 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
68 |
sinr :: "'b \<rightarrow> ('a ++ 'b)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
69 |
"sinr \<equiv> \<Lambda> b. Abs_Ssum <\<bottom>, b>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
70 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
71 |
subsection {* Properties of @{term sinl} and @{term sinr} *} |
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 |
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
|
74 |
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
|
75 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
79 |
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
|
80 |
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
|
81 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
85 |
lemma strict_sinl [simp]: "sinl\<cdot>\<bottom> = \<bottom>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
86 |
by (simp add: sinl_Abs_Ssum UU_Abs_Ssum) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
87 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
88 |
lemma strict_sinr [simp]: "sinr\<cdot>\<bottom> = \<bottom>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
89 |
by (simp add: sinr_Abs_Ssum UU_Abs_Ssum) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
90 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
91 |
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
|
92 |
apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum) |
15606
95617b30514b
simplified some definitions, many proofs are much shorter
huffman
parents:
15600
diff
changeset
|
93 |
apply (simp add: Abs_Ssum_inject Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
94 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
95 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
96 |
lemma inject_sinl: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
97 |
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
|
98 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
99 |
lemma inject_sinr: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
100 |
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
|
101 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
102 |
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
|
103 |
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
|
104 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
105 |
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
|
106 |
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
|
107 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
108 |
lemma defined_sinl [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
|
109 |
apply (erule contrapos_nn) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
110 |
apply (rule inject_sinl) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
111 |
apply auto |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
112 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
113 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
114 |
lemma defined_sinr [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
|
115 |
apply (erule contrapos_nn) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
116 |
apply (rule inject_sinr) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
117 |
apply auto |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
118 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
119 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
120 |
subsection {* Case analysis *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
121 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
122 |
lemma Exh_Ssum1: |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
123 |
"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
|
124 |
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
|
125 |
apply (rule_tac x=z in Abs_Ssum_cases) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
126 |
apply (rule_tac p=y in cprodE) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
127 |
apply (auto simp add: Ssum_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
128 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
129 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
130 |
lemma ssumE: |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
131 |
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
132 |
\<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
|
133 |
\<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
|
134 |
by (cut_tac z=p in Exh_Ssum1, auto) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
135 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
136 |
lemma ssumE2: |
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
137 |
"\<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
|
138 |
apply (rule_tac p=p in ssumE) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
139 |
apply (simp only: strict_sinl [symmetric]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
140 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
141 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
142 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
143 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
144 |
subsection {* Ordering properties of @{term sinl} and @{term sinr} *} |
15576
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 |
lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
147 |
apply (rule iffI) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
148 |
apply (erule less_cprod5c) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
149 |
apply (simp add: monofun_cfun) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
150 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
151 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
152 |
lemma less_ssum4a: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
153 |
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
|
154 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
155 |
lemma less_ssum4b: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
156 |
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
|
157 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
158 |
lemma less_ssum4c: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
159 |
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
|
160 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
161 |
lemma less_ssum4d: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
162 |
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
|
163 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
164 |
subsection {* Chains of strict sums *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
165 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
166 |
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
|
167 |
apply (rule_tac p=p in ssumE) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
168 |
apply (rule_tac x="\<bottom>" in exI, simp) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
169 |
apply (simp add: less_ssum4a sinl_eq) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
170 |
apply (simp add: less_ssum4d) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
171 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
172 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
173 |
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
|
174 |
apply (rule_tac p=p in ssumE) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
175 |
apply (rule_tac x="\<bottom>" in exI, simp) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
176 |
apply (simp add: less_ssum4c) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
177 |
apply (simp add: less_ssum4b sinr_eq) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
178 |
done |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
179 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
180 |
lemma ssum_chain_lemma: |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
181 |
"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
|
182 |
(\<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
|
183 |
apply (rule_tac p="lub (range Y)" in ssumE2) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
184 |
apply (rule disjI1) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
185 |
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
|
186 |
apply (rule conjI) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
187 |
apply (rule chain_monofun) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
188 |
apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
189 |
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
|
190 |
apply (drule less_sinlD, clarify) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
191 |
apply (simp add: sinl_eq Rep_Ssum_sinl) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
192 |
apply (rule disjI2) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
193 |
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
|
194 |
apply (rule conjI) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
195 |
apply (rule chain_monofun) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
196 |
apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
197 |
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
|
198 |
apply (drule less_sinrD, clarify) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
199 |
apply (simp add: sinr_eq Rep_Ssum_sinr) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
200 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
201 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
202 |
subsection {* Definitions of constants *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
203 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
204 |
constdefs |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
205 |
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
|
206 |
"Iwhen \<equiv> \<lambda>f g s. |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
207 |
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
|
208 |
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
|
209 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
210 |
text {* rewrites for @{term Iwhen} *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
211 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
212 |
lemma Iwhen1 [simp]: "Iwhen f g \<bottom> = \<bottom>" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
213 |
by (simp add: Iwhen_def strict_Rep_Ssum) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
214 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
215 |
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
|
216 |
by (simp add: Iwhen_def Rep_Ssum_sinl) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
217 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
218 |
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
|
219 |
by (simp add: Iwhen_def Rep_Ssum_sinr) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
220 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
221 |
lemma Iwhen4: "Iwhen f g (sinl\<cdot>x) = strictify\<cdot>f\<cdot>x" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
222 |
by (case_tac "x = \<bottom>", simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
223 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
224 |
lemma Iwhen5: "Iwhen f g (sinr\<cdot>y) = strictify\<cdot>g\<cdot>y" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
225 |
by (case_tac "y = \<bottom>" , simp_all) |
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 |
subsection {* Continuity of @{term Iwhen} *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
228 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
229 |
text {* @{term Iwhen} is continuous in all arguments *} |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
230 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
231 |
lemma cont_Iwhen1: "cont (\<lambda>f. Iwhen f g s)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
232 |
by (rule_tac p=s in ssumE, simp_all) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
233 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
234 |
lemma cont_Iwhen2: "cont (\<lambda>g. Iwhen f g s)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
235 |
by (rule_tac p=s in ssumE, simp_all) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
236 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
237 |
lemma cont_Iwhen3: "cont (\<lambda>s. Iwhen f g s)" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
238 |
apply (rule contI [rule_format]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
239 |
apply (drule ssum_chain_lemma, safe) |
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: Iwhen4) |
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) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
244 |
apply (simp add: contlub_cfun_arg [symmetric]) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
245 |
apply (simp add: Iwhen5) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
246 |
apply (simp add: contlub_cfun_arg) |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
247 |
apply (simp add: thelubE chain_monofun) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
248 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
249 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
250 |
subsection {* Continuous versions of constants *} |
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 |
constdefs |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
253 |
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
|
254 |
"sscase \<equiv> \<Lambda> f g s. Iwhen f g s" |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
255 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
256 |
translations |
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
257 |
"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
|
258 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
259 |
text {* continuous versions of lemmas for @{term sscase} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
260 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
261 |
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
|
262 |
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
|
263 |
|
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
264 |
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
|
265 |
by (simp add: beta_sscase) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
266 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
267 |
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
|
268 |
by (simp add: beta_sscase) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
269 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
270 |
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
|
271 |
by (simp add: beta_sscase) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
272 |
|
16060
833be7f71ecd
Simplified version of strict sum theory, using TypedefPcpo
huffman
parents:
15606
diff
changeset
|
273 |
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
|
274 |
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
|
275 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
276 |
end |