author | huffman |
Thu, 03 Nov 2005 01:02:29 +0100 | |
changeset 18077 | f1f4f951ec8d |
parent 17837 | 2922be3544f8 |
child 18078 | 20e5a6440790 |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Cprod.thy |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
2 |
ID: $Id$ |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
3 |
Author: Franz Regensburger |
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:
16057
diff
changeset
|
5 |
Partial ordering for cartesian product of HOL products. |
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 cpo of cartesian products *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
|
15577 | 10 |
theory Cprod |
11 |
imports Cfun |
|
12 |
begin |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
13 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
14 |
defaultsort cpo |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
|
16008 | 16 |
subsection {* Type @{typ unit} is a pcpo *} |
17 |
||
18 |
instance unit :: sq_ord .. |
|
19 |
||
20 |
defs (overloaded) |
|
21 |
less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True" |
|
22 |
||
23 |
instance unit :: po |
|
24 |
by intro_classes simp_all |
|
25 |
||
26 |
instance unit :: cpo |
|
27 |
by intro_classes (simp add: is_lub_def is_ub_def) |
|
28 |
||
29 |
instance unit :: pcpo |
|
30 |
by intro_classes simp |
|
31 |
||
32 |
||
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
33 |
subsection {* Type @{typ "'a * 'b"} is a partial order *} |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
34 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
35 |
instance "*" :: (sq_ord, sq_ord) sq_ord .. |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
36 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
defs (overloaded) |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
38 |
less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
39 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
40 |
lemma refl_less_cprod: "(p::'a * 'b) \<sqsubseteq> p" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
41 |
by (simp add: less_cprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
43 |
lemma antisym_less_cprod: "\<lbrakk>(p1::'a * 'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p1\<rbrakk> \<Longrightarrow> p1 = p2" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
44 |
apply (unfold less_cprod_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
45 |
apply (rule injective_fst_snd) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
apply (fast intro: antisym_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
47 |
apply (fast intro: antisym_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
48 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
49 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
50 |
lemma trans_less_cprod: "\<lbrakk>(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
51 |
apply (unfold less_cprod_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
52 |
apply (fast intro: trans_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
53 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
54 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
55 |
instance "*" :: (cpo, cpo) po |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
56 |
by intro_classes |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
57 |
(assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+ |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
58 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
59 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
60 |
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
61 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
62 |
text {* Pair @{text "(_,_)"} is monotone in both arguments *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
63 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
64 |
lemma monofun_pair1: "monofun (\<lambda>x. (x, y))" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
65 |
by (simp add: monofun_def less_cprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
66 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
67 |
lemma monofun_pair2: "monofun (\<lambda>y. (x, y))" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
68 |
by (simp add: monofun_def less_cprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
69 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
70 |
lemma monofun_pair: |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
71 |
"\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
72 |
by (simp add: less_cprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
73 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
74 |
text {* @{term fst} and @{term snd} are monotone *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
75 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
76 |
lemma monofun_fst: "monofun fst" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
77 |
by (simp add: monofun_def less_cprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
78 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
79 |
lemma monofun_snd: "monofun snd" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
80 |
by (simp add: monofun_def less_cprod_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
81 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
82 |
subsection {* Type @{typ "'a * 'b"} is a cpo *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
83 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
84 |
lemma lub_cprod: |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
85 |
"chain S \<Longrightarrow> range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
apply (rule is_lubI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
87 |
apply (rule ub_rangeI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
88 |
apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
89 |
apply (rule monofun_pair) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
90 |
apply (rule is_ub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
91 |
apply (erule monofun_fst [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
92 |
apply (rule is_ub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
93 |
apply (erule monofun_snd [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
94 |
apply (rule_tac t = "u" in surjective_pairing [THEN ssubst]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
95 |
apply (rule monofun_pair) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
96 |
apply (rule is_lub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
97 |
apply (erule monofun_fst [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
98 |
apply (erule monofun_fst [THEN ub2ub_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
99 |
apply (rule is_lub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
100 |
apply (erule monofun_snd [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
101 |
apply (erule monofun_snd [THEN ub2ub_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
102 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
103 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
104 |
lemma thelub_cprod: |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
105 |
"chain S \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
106 |
by (rule lub_cprod [THEN thelubI]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
107 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
108 |
lemma cpo_cprod: |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
109 |
"chain (S::nat \<Rightarrow> 'a::cpo * 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
110 |
by (rule exI, erule lub_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
111 |
|
15609 | 112 |
instance "*" :: (cpo, cpo) cpo |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
113 |
by intro_classes (rule cpo_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
114 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
115 |
subsection {* Type @{typ "'a * 'b"} is pointed *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
116 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
117 |
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
118 |
by (simp add: less_cprod_def) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
119 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
120 |
lemma least_cprod: "EX x::'a::pcpo * 'b::pcpo. ALL y. x \<sqsubseteq> y" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
121 |
apply (rule_tac x = "(\<bottom>, \<bottom>)" in exI) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
122 |
apply (rule minimal_cprod [THEN allI]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
123 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
124 |
|
15609 | 125 |
instance "*" :: (pcpo, pcpo) pcpo |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
126 |
by intro_classes (rule least_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
127 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
128 |
text {* for compatibility with old HOLCF-Version *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
129 |
lemma inst_cprod_pcpo: "UU = (UU,UU)" |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
130 |
by (rule minimal_cprod [THEN UU_I, symmetric]) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
131 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
132 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
133 |
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
134 |
|
16916 | 135 |
lemma contlub_pair1: "contlub (\<lambda>x. (x, y))" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
136 |
apply (rule contlubI) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
137 |
apply (subst thelub_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
138 |
apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
139 |
apply simp |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
140 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
141 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
142 |
lemma contlub_pair2: "contlub (\<lambda>y. (x, y))" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
143 |
apply (rule contlubI) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
144 |
apply (subst thelub_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
145 |
apply (erule monofun_pair2 [THEN ch2ch_monofun]) |
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
146 |
apply simp |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
147 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
148 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
149 |
lemma cont_pair1: "cont (\<lambda>x. (x, y))" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
150 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
151 |
apply (rule monofun_pair1) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
152 |
apply (rule contlub_pair1) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
153 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
154 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
155 |
lemma cont_pair2: "cont (\<lambda>y. (x, y))" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
156 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
157 |
apply (rule monofun_pair2) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
158 |
apply (rule contlub_pair2) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
159 |
done |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
160 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
161 |
lemma contlub_fst: "contlub fst" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
162 |
apply (rule contlubI) |
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
163 |
apply (simp add: thelub_cprod) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
164 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
165 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
166 |
lemma contlub_snd: "contlub snd" |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
167 |
apply (rule contlubI) |
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
168 |
apply (simp add: thelub_cprod) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
169 |
done |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
170 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
171 |
lemma cont_fst: "cont fst" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
172 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
173 |
apply (rule monofun_fst) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
174 |
apply (rule contlub_fst) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
175 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
176 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
177 |
lemma cont_snd: "cont snd" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
178 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
179 |
apply (rule monofun_snd) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
180 |
apply (rule contlub_snd) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
181 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
182 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
183 |
subsection {* Continuous versions of constants *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
184 |
|
17834 | 185 |
constdefs |
186 |
cpair :: "'a \<rightarrow> 'b \<rightarrow> ('a * 'b)" (* continuous pairing *) |
|
187 |
"cpair \<equiv> (\<Lambda> x y. (x, y))" |
|
188 |
||
189 |
cfst :: "('a * 'b) \<rightarrow> 'a" |
|
190 |
"cfst \<equiv> (\<Lambda> p. fst p)" |
|
191 |
||
192 |
csnd :: "('a * 'b) \<rightarrow> 'b" |
|
193 |
"csnd \<equiv> (\<Lambda> p. snd p)" |
|
194 |
||
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
195 |
csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" |
17834 | 196 |
"csplit \<equiv> (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
197 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
198 |
syntax |
17834 | 199 |
"_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(1<_,/ _>)") |
200 |
||
201 |
syntax (xsymbols) |
|
202 |
"_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(1\<langle>_,/ _\<rangle>)") |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
203 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
204 |
translations |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
205 |
"<x, y, z>" == "<x, <y, z>>" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
206 |
"<x, y>" == "cpair$x$y" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
207 |
|
17834 | 208 |
text {* syntax for @{text "LAM <x,y,z>.e"} *} |
209 |
||
17816
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset
|
210 |
syntax |
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset
|
211 |
"_ctuple_pttrn" :: "[pttrn, patterns] => pttrn" ("<_,/ _>") |
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset
|
212 |
|
17834 | 213 |
syntax (xsymbols) |
214 |
"_ctuple_pttrn" :: "[pttrn, patterns] => pttrn" ("\<langle>_,/ _\<rangle>") |
|
215 |
||
17816
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset
|
216 |
translations |
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset
|
217 |
"LAM <x,y,zs>. t" == "csplit$(LAM x <y,zs>. t)" |
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset
|
218 |
"LAM <x,y>. t" == "csplit$(LAM x y. t)" |
9942c5ed866a
new syntax translations for continuous lambda abstraction
huffman
parents:
16916
diff
changeset
|
219 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
220 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
221 |
subsection {* Convert all lemmas to the continuous versions *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
222 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
223 |
lemma cpair_eq_pair: "<x, y> = (x, y)" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
224 |
by (simp add: cpair_def cont_pair1 cont_pair2) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
225 |
|
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
226 |
lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
227 |
by (simp add: cpair_eq_pair) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
228 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
229 |
lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
230 |
by (simp add: cpair_eq_pair) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
231 |
|
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
232 |
lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')" |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
233 |
by (simp add: cpair_eq_pair less_cprod_def) |
16057
e23a61b3406f
added lemma cpair_eq, made cfst_strict and csnd_strict into simp rules
huffman
parents:
16008
diff
changeset
|
234 |
|
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
235 |
lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)" |
16916 | 236 |
by (simp add: inst_cprod_pcpo cpair_eq_pair) |
237 |
||
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
238 |
lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>" |
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
239 |
by simp |
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
240 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
241 |
lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>" |
16916 | 242 |
by (rule cpair_strict [symmetric]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
243 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
244 |
lemma defined_cpair_rev: |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
245 |
"<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>" |
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
246 |
by simp |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
247 |
|
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
248 |
lemma Exh_Cprod2: "\<exists>a b. z = <a, b>" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
249 |
by (simp add: cpair_eq_pair) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
250 |
|
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
251 |
lemma cprodE: "\<lbrakk>\<And>x y. p = <x, y> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
252 |
by (cut_tac Exh_Cprod2, auto) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
253 |
|
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
254 |
lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x" |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
255 |
by (simp add: cpair_eq_pair cfst_def cont_fst) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
256 |
|
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
257 |
lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y" |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
258 |
by (simp add: cpair_eq_pair csnd_def cont_snd) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
259 |
|
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
260 |
lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
261 |
by (simp add: inst_cprod_pcpo2) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
262 |
|
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
263 |
lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
264 |
by (simp add: inst_cprod_pcpo2) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
265 |
|
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
266 |
lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
267 |
apply (unfold cfst_def csnd_def) |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
268 |
apply (simp add: cont_fst cont_snd cpair_eq_pair) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
269 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
270 |
|
16750 | 271 |
lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)" |
16315 | 272 |
by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd) |
273 |
||
16750 | 274 |
lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)" |
275 |
by (auto simp add: po_eq_conv less_cprod) |
|
276 |
||
17837 | 277 |
lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>" |
278 |
by (rule compactI, simp add: less_cprod) |
|
279 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
280 |
lemma lub_cprod2: |
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
281 |
"chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
282 |
apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
283 |
apply (erule lub_cprod) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
284 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
285 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
286 |
lemma thelub_cprod2: |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
287 |
"chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>" |
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
288 |
by (rule lub_cprod2 [THEN thelubI]) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
289 |
|
18077
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
290 |
lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>" |
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
291 |
by (simp add: csplit_def) |
f1f4f951ec8d
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
huffman
parents:
17837
diff
changeset
|
292 |
|
16081
81a4b4a245b0
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff
huffman
parents:
16070
diff
changeset
|
293 |
lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
294 |
by (simp add: csplit_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
295 |
|
16553 | 296 |
lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
297 |
by (simp add: csplit_def surjective_pairing_Cprod2) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
298 |
|
16210
5d1b752cacc1
changed to use new contlubI, monofun_def; renamed cfst2, csnd2 to cfst_cpair, csnd_cpair; added lemma cpair_strict
huffman
parents:
16093
diff
changeset
|
299 |
lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2 |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
300 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
301 |
end |