author | huffman |
Thu, 10 Mar 2005 20:22:45 +0100 | |
changeset 15600 | a59f07556a8d |
parent 15593 | 24d770bbc44a |
child 15609 | d12c459e2325 |
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 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
Partial ordering for cartesian product of HOL theory prod.thy |
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 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
9 |
header {* The cpo of cartesian products *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
10 |
|
15577 | 11 |
theory Cprod |
12 |
imports Cfun |
|
13 |
begin |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
14 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
defaultsort cpo |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
16 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
17 |
subsection {* Ordering on @{typ "'a * 'b"} *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
18 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
19 |
instance "*" :: (sq_ord, sq_ord) sq_ord .. |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
20 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
21 |
defs (overloaded) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
22 |
less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
23 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
24 |
subsection {* Type @{typ "'a * 'b"} is a partial order *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
25 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
26 |
lemma refl_less_cprod: "(p::'a*'b) << p" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
27 |
apply (unfold less_cprod_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
28 |
apply simp |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
30 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
31 |
lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
32 |
apply (unfold less_cprod_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
33 |
apply (rule injective_fst_snd) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
34 |
apply (fast intro: antisym_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
35 |
apply (fast intro: antisym_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
36 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
37 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
38 |
lemma trans_less_cprod: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
39 |
"[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
40 |
apply (unfold less_cprod_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
41 |
apply (rule conjI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
42 |
apply (fast intro: trans_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
43 |
apply (fast intro: trans_less) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
44 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
45 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
defaultsort pcpo |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
47 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
48 |
instance "*" :: (cpo, cpo) po |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
49 |
by intro_classes |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
50 |
(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
|
51 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
52 |
text {* for compatibility with old HOLCF-Version *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
53 |
lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
54 |
apply (fold less_cprod_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
55 |
apply (rule refl) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
56 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
57 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
58 |
lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
59 |
apply (simp add: inst_cprod_po) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
60 |
done |
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 |
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
63 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
64 |
text {* Pair @{text "(_,_)"} is monotone in both arguments *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
65 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
66 |
lemma monofun_pair1: "monofun Pair" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
67 |
by (simp add: monofun less_fun inst_cprod_po) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
68 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
69 |
lemma monofun_pair2: "monofun(Pair x)" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
70 |
by (simp add: monofun inst_cprod_po) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
71 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
72 |
lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
73 |
by (simp add: inst_cprod_po) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
74 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
75 |
text {* @{term fst} and @{term snd} are monotone *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
76 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
77 |
lemma monofun_fst: "monofun fst" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
78 |
by (simp add: monofun inst_cprod_po) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
79 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
80 |
lemma monofun_snd: "monofun snd" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
81 |
by (simp add: monofun inst_cprod_po) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
82 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
83 |
subsection {* Type @{typ "'a * 'b"} is a cpo *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
84 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
85 |
lemma lub_cprod: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
86 |
"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
87 |
apply (rule is_lubI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
88 |
apply (rule ub_rangeI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
89 |
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
|
90 |
apply (rule monofun_pair) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
91 |
apply (rule is_ub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
92 |
apply (erule monofun_fst [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
93 |
apply (rule is_ub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
94 |
apply (erule monofun_snd [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
95 |
apply (rule_tac t = "u" in surjective_pairing [THEN ssubst]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
96 |
apply (rule monofun_pair) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
97 |
apply (rule is_lub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
98 |
apply (erule monofun_fst [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
99 |
apply (erule monofun_fst [THEN ub2ub_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
100 |
apply (rule is_lub_thelub) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
101 |
apply (erule monofun_snd [THEN ch2ch_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
102 |
apply (erule monofun_snd [THEN ub2ub_monofun]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
103 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
104 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
105 |
lemmas thelub_cprod = lub_cprod [THEN thelubI, standard] |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
106 |
(* |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
107 |
"chain ?S1 ==> |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
108 |
lub (range ?S1) = |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
109 |
(lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
110 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
111 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
112 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
113 |
lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
114 |
by (rule exI, erule lub_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
115 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
116 |
instance "*" :: (cpo,cpo)cpo |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
117 |
by intro_classes (rule cpo_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
118 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
119 |
subsection {* Type @{typ "'a * 'b"} is pointed *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
120 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
121 |
lemma minimal_cprod: "(UU,UU)<<p" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
122 |
by (simp add: inst_cprod_po) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
123 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
124 |
lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard] |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
125 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
126 |
lemma least_cprod: "EX x::'a*'b. ALL y. x<<y" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
127 |
apply (rule_tac x = " (UU,UU) " in exI) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
128 |
apply (rule minimal_cprod [THEN allI]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
129 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
130 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
131 |
instance "*" :: (pcpo,pcpo)pcpo |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
132 |
by intro_classes (rule least_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
133 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
134 |
text {* for compatibility with old HOLCF-Version *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
135 |
lemma inst_cprod_pcpo: "UU = (UU,UU)" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
136 |
apply (simp add: UU_cprod_def[folded UU_def]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
137 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
138 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
139 |
subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
140 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
141 |
lemma contlub_pair1: "contlub(Pair)" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
142 |
apply (rule contlubI [rule_format]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
143 |
apply (rule ext) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
144 |
apply (subst lub_fun [THEN thelubI]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
145 |
apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
146 |
apply (subst thelub_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
147 |
apply (rule ch2ch_fun) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
148 |
apply (erule monofun_pair1 [THEN ch2ch_monofun]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
149 |
apply (simp add: lub_const [THEN thelubI]) |
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 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
152 |
lemma contlub_pair2: "contlub(Pair(x))" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
153 |
apply (rule contlubI [rule_format]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
154 |
apply (subst thelub_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
155 |
apply (erule monofun_pair2 [THEN ch2ch_monofun]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
156 |
apply (simp add: lub_const [THEN thelubI]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
157 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
158 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
159 |
lemma cont_pair1: "cont(Pair)" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
160 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
161 |
apply (rule monofun_pair1) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
162 |
apply (rule contlub_pair1) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
163 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
164 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
165 |
lemma cont_pair2: "cont(Pair(x))" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
166 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
167 |
apply (rule monofun_pair2) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
168 |
apply (rule contlub_pair2) |
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 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
171 |
lemma contlub_fst: "contlub(fst)" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
172 |
apply (rule contlubI [rule_format]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
173 |
apply (simp add: lub_cprod [THEN thelubI]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
174 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
175 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
176 |
lemma contlub_snd: "contlub(snd)" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
177 |
apply (rule contlubI [rule_format]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
178 |
apply (simp add: lub_cprod [THEN thelubI]) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
179 |
done |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
180 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
181 |
lemma cont_fst: "cont(fst)" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
182 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
183 |
apply (rule monofun_fst) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
184 |
apply (rule contlub_fst) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
185 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
186 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
187 |
lemma cont_snd: "cont(snd)" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
188 |
apply (rule monocontlub2cont) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
189 |
apply (rule monofun_snd) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
190 |
apply (rule contlub_snd) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
191 |
done |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
192 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
193 |
subsection {* Continuous versions of constants *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
194 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
195 |
consts |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
196 |
cpair :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
197 |
cfst :: "('a::cpo*'b::cpo)->'a" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
198 |
csnd :: "('a::cpo*'b::cpo)->'b" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
199 |
csplit :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
200 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
201 |
syntax |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
202 |
"@ctuple" :: "['a, args] => 'a * 'b" ("(1<_,/ _>)") |
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 |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
205 |
"<x, y, z>" == "<x, <y, z>>" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
206 |
"<x, y>" == "cpair$x$y" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
207 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
208 |
defs |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
209 |
cpair_def: "cpair == (LAM x y.(x,y))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
210 |
cfst_def: "cfst == (LAM p. fst(p))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
211 |
csnd_def: "csnd == (LAM p. snd(p))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
212 |
csplit_def: "csplit == (LAM f p. f$(cfst$p)$(csnd$p))" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
213 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
214 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
215 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
216 |
(* introduce syntax for |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
217 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
218 |
Let <x,y> = e1; z = E2 in E3 |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
219 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
220 |
and |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
221 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
222 |
LAM <x,y,z>.e |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
223 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
224 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
225 |
constdefs |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
226 |
CLet :: "'a -> ('a -> 'b) -> 'b" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
227 |
"CLet == LAM s f. f$s" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
228 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
229 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
230 |
(* syntax for Let *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
231 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
232 |
nonterminals |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
233 |
Cletbinds Cletbind |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
234 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
235 |
syntax |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
236 |
"_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
237 |
"" :: "Cletbind => Cletbinds" ("_") |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
238 |
"_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
239 |
"_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
240 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
241 |
translations |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
242 |
"_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
243 |
"Let x = a in e" == "CLet$a$(LAM x. e)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
244 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
245 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
246 |
(* syntax for LAM <x,y,z>.e *) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
247 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
248 |
syntax |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
249 |
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
250 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
251 |
translations |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
252 |
"LAM <x,y,zs>.b" == "csplit$(LAM x. LAM <y,zs>.b)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
253 |
"LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
254 |
"LAM <x,y>.b" == "csplit$(LAM x y. b)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
255 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
256 |
syntax (xsymbols) |
15577 | 257 |
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
258 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
259 |
subsection {* Convert all lemmas to the continuous versions *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
260 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
261 |
lemma beta_cfun_cprod: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
262 |
"(LAM x y.(x,y))$a$b = (a,b)" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
263 |
apply (subst beta_cfun) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
264 |
apply (simp add: cont_pair1 cont_pair2 cont2cont_CF1L) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
265 |
apply (subst beta_cfun) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
266 |
apply (rule cont_pair2) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
267 |
apply (rule refl) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
268 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
269 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
270 |
lemma inject_cpair: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
271 |
"<a,b> = <aa,ba> ==> a=aa & b=ba" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
272 |
by (simp add: cpair_def beta_cfun_cprod) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
273 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
274 |
lemma inst_cprod_pcpo2: "UU = <UU,UU>" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
275 |
by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
276 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
277 |
lemma defined_cpair_rev: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
278 |
"<a,b> = UU ==> a = UU & b = UU" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
279 |
apply (drule inst_cprod_pcpo2 [THEN subst]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
280 |
apply (erule inject_cpair) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
281 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
282 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
283 |
lemma Exh_Cprod2: "? a b. z=<a,b>" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
284 |
apply (unfold cpair_def) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
285 |
apply (rule PairE) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
286 |
apply (rule exI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
287 |
apply (rule exI) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
288 |
apply (erule beta_cfun_cprod [THEN ssubst]) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
289 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
290 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
291 |
lemma cprodE: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
292 |
assumes prems: "!!x y. [| p = <x,y> |] ==> Q" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
293 |
shows "Q" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
294 |
apply (rule PairE) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
295 |
apply (rule prems) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
296 |
apply (simp add: cpair_def beta_cfun_cprod) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
297 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
298 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
299 |
lemma cfst2 [simp]: "cfst$<x,y> = x" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
300 |
by (simp add: cpair_def cfst_def beta_cfun_cprod cont_fst) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
301 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
302 |
lemma csnd2 [simp]: "csnd$<x,y> = y" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
303 |
by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
304 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
305 |
lemma cfst_strict: "cfst$UU = UU" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
306 |
by (simp add: inst_cprod_pcpo2) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
307 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
308 |
lemma csnd_strict: "csnd$UU = UU" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
309 |
by (simp add: inst_cprod_pcpo2) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
310 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
311 |
lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p" |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
312 |
apply (unfold cfst_def csnd_def cpair_def) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
313 |
apply (simp add: cont_fst cont_snd beta_cfun_cprod) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
314 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
315 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
316 |
lemma less_cprod5c: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
317 |
"<xa,ya> << <x,y> ==> xa<<x & ya << y" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
318 |
by (simp add: cpair_def beta_cfun_cprod inst_cprod_po) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
319 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
320 |
lemma lub_cprod2: |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
321 |
"[|chain(S)|] ==> range(S) <<| |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
322 |
<(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
323 |
apply (simp add: cpair_def beta_cfun_cprod) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
324 |
apply (simp add: cfst_def csnd_def cont_fst cont_snd) |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
325 |
apply (erule lub_cprod) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
326 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
327 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
328 |
lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard] |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
329 |
(* |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
330 |
chain ?S1 ==> |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
331 |
lub (range ?S1) = |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
332 |
<lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
333 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
334 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
335 |
lemma csplit2 [simp]: "csplit$f$<x,y> = f$x$y" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
336 |
by (simp add: csplit_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
337 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
338 |
lemma csplit3: "csplit$cpair$z=z" |
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
339 |
by (simp add: csplit_def surjective_pairing_Cprod2) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
340 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
341 |
lemmas Cprod_rews = cfst2 csnd2 csplit2 |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
342 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
343 |
end |