author | huffman |
Fri, 04 Jan 2008 00:01:02 +0100 | |
changeset 25827 | c2adeb1bae5c |
parent 25757 | 5957e3d72fec |
child 25881 | d80bd899ea95 |
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 |
16699 | 11 |
imports Cprod |
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 |
|
17817 | 18 |
pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) = |
16059
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>)}" |
16699 | 20 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
22 |
instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
23 |
by (rule typedef_finite_po [OF type_definition_Sprod]) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
24 |
|
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
25 |
instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
26 |
by (rule typedef_chfin [OF type_definition_Sprod less_Sprod_def]) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
27 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
syntax (xsymbols) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
syntax (HTML output) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
31 |
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20) |
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 spair_lemma: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
34 |
"<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
|
35 |
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
|
36 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
37 |
subsection {* Definitions of constants *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
39 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
40 |
sfst :: "('a ** 'b) \<rightarrow> 'a" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
41 |
"sfst = (\<Lambda> p. cfst\<cdot>(Rep_Sprod p))" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
42 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
43 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
44 |
ssnd :: "('a ** 'b) \<rightarrow> 'b" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
45 |
"ssnd = (\<Lambda> p. csnd\<cdot>(Rep_Sprod p))" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
47 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
48 |
spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
49 |
"spair = (\<Lambda> a b. Abs_Sprod |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
50 |
<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
|
51 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
52 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
53 |
ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
54 |
"ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
55 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
56 |
syntax |
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
57 |
"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
58 |
translations |
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
59 |
"(:x, y, z:)" == "(:x, (:y, z:):)" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18078
diff
changeset
|
60 |
"(:x, y:)" == "CONST spair\<cdot>x\<cdot>y" |
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
61 |
|
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
62 |
translations |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18078
diff
changeset
|
63 |
"\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
64 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
65 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
66 |
subsection {* Case analysis *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
67 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
68 |
lemma spair_Abs_Sprod: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
69 |
"(: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
|
70 |
apply (unfold spair_def) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
71 |
apply (simp add: cont_Abs_Sprod spair_lemma) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
72 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
73 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
74 |
lemma Exh_Sprod2: |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
75 |
"z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
76 |
apply (cases z rule: Abs_Sprod_cases) |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
77 |
apply (simp add: Sprod_def) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
78 |
apply (erule disjE) |
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
79 |
apply (simp add: Abs_Sprod_strict) |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
80 |
apply (rule disjI2) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
81 |
apply (rule_tac x="cfst\<cdot>y" in exI) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
82 |
apply (rule_tac x="csnd\<cdot>y" in exI) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
83 |
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
|
84 |
apply (simp add: surjective_pairing_Cprod2) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
85 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
|
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
87 |
lemma sprodE [cases type: **]: |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
88 |
"\<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
|
89 |
by (cut_tac z=p in Exh_Sprod2, auto) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
90 |
|
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
91 |
lemma sprod_induct [induct type: **]: |
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
92 |
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x" |
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
93 |
by (cases x, simp_all) |
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
94 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
95 |
subsection {* Properties of @{term spair} *} |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
96 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
97 |
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>" |
16920 | 98 |
by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
99 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
100 |
lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>" |
16920 | 101 |
by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
102 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
103 |
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
|
104 |
by auto |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
105 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
106 |
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
|
107 |
by (erule contrapos_np, auto) |
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
108 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
109 |
lemma spair_defined [simp]: |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
110 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>" |
18078
20e5a6440790
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
huffman
parents:
17837
diff
changeset
|
111 |
by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
112 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
113 |
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
|
114 |
by (erule contrapos_pp, simp) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
115 |
|
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
116 |
lemma spair_eq: |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
117 |
"\<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
|
118 |
apply (simp add: spair_Abs_Sprod) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
119 |
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
|
120 |
apply (simp add: strictify_conv_if) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
121 |
done |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
122 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
123 |
lemma spair_inject: |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
124 |
"\<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
|
125 |
by (rule spair_eq [THEN iffD1]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
126 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
127 |
lemma inst_sprod_pcpo2: "UU = (:UU,UU:)" |
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
128 |
by simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
129 |
|
17837 | 130 |
lemma Rep_Sprod_spair: |
131 |
"Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>" |
|
132 |
apply (unfold spair_def) |
|
133 |
apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma) |
|
134 |
done |
|
135 |
||
136 |
lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)" |
|
137 |
by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if) |
|
138 |
||
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
139 |
subsection {* Properties of @{term sfst} and @{term ssnd} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
140 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
141 |
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
|
142 |
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
|
143 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
144 |
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
|
145 |
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
|
146 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
|
16212
422f836f6b39
renamed strict, defined, and inject lemmas; renamed sfst2, ssnd2 to sfst_spair, ssnd_spair
huffman
parents:
16082
diff
changeset
|
150 |
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
|
151 |
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
|
152 |
|
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
153 |
lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
154 |
by (cases p, simp_all) |
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
155 |
|
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
156 |
lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
157 |
by (cases p, simp_all) |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
158 |
|
16777
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
159 |
lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>" |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
160 |
by simp |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
161 |
|
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
162 |
lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>" |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
163 |
by simp |
555c8951f05c
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
huffman
parents:
16751
diff
changeset
|
164 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
165 |
lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
166 |
by (cases p, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
167 |
|
16751 | 168 |
lemma less_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)" |
16699 | 169 |
apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod) |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
170 |
apply (rule less_cprod) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
171 |
done |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
172 |
|
16751 | 173 |
lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)" |
174 |
by (auto simp add: po_eq_conv less_sprod) |
|
175 |
||
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
176 |
lemma spair_less: |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
177 |
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
178 |
apply (cases "a = \<bottom>", simp) |
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
179 |
apply (cases "b = \<bottom>", simp) |
16317
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
180 |
apply (simp add: less_sprod) |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
181 |
done |
868eddbcaf6e
added theorems less_sprod, spair_less, spair_eq, spair_inject
huffman
parents:
16212
diff
changeset
|
182 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
183 |
subsection {* Properties of @{term ssplit} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
184 |
|
16059
dab0d004732f
Simplified version of strict product theory, using TypedefPcpo
huffman
parents:
15930
diff
changeset
|
185 |
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
|
186 |
by (simp add: ssplit_def) |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
187 |
|
16920 | 188 |
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
|
189 |
by (simp add: ssplit_def) |
50c3384ca6c4
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
190 |
|
16553 | 191 |
lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z" |
25757
5957e3d72fec
declare sprodE as cases rule; new induction rule sprod_induct
huffman
parents:
25135
diff
changeset
|
192 |
by (cases z, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
193 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
194 |
subsection {* Strict product preserves flatness *} |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
195 |
|
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
196 |
instance "**" :: (flat, flat) flat |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
197 |
apply (intro_classes, clarify) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
198 |
apply (rule_tac p=x in sprodE, simp) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
199 |
apply (rule_tac p=y in sprodE, simp) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
200 |
apply (simp add: flat_less_iff spair_less) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
201 |
done |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25757
diff
changeset
|
202 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
203 |
end |