author | paulson |
Fri, 21 Nov 2003 11:15:40 +0100 | |
changeset 14265 | 95b42e69436c |
parent 13601 | fd3e3d6b37b2 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
9245 | 1 |
(* Title: HOLCF/Sprod0 |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
12030 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
9245 | 6 |
Strict product with typedef. |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
(* A non-emptyness result for Sprod *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
13 |
Goalw [Sprod_def] "(Spair_Rep a b):Sprod"; |
9245 | 14 |
by (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl]); |
15 |
qed "SprodI"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
17 |
Goal "inj_on Abs_Sprod Sprod"; |
9245 | 18 |
by (rtac inj_on_inverseI 1); |
19 |
by (etac Abs_Sprod_inverse 1); |
|
20 |
qed "inj_on_Abs_Sprod"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
21 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
23 |
(* Strictness and definedness of Spair_Rep *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
26 |
Goalw [Spair_Rep_def] |
9245 | 27 |
"(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"; |
28 |
by (rtac ext 1); |
|
29 |
by (rtac ext 1); |
|
30 |
by (rtac iffI 1); |
|
31 |
by (fast_tac HOL_cs 1); |
|
32 |
by (fast_tac HOL_cs 1); |
|
33 |
qed "strict_Spair_Rep"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
34 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
35 |
Goalw [Spair_Rep_def] |
9245 | 36 |
"(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"; |
37 |
by (case_tac "a=UU|b=UU" 1); |
|
38 |
by (atac 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
39 |
by (fast_tac (claset() addDs [fun_cong]) 1); |
9245 | 40 |
qed "defined_Spair_Rep_rev"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
43 |
(* injectivity of Spair_Rep and Ispair *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
44 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
45 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
46 |
Goalw [Spair_Rep_def] |
9245 | 47 |
"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
48 |
by (dtac fun_cong 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
49 |
by (dtac fun_cong 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
50 |
by (etac (iffD1 RS mp) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
51 |
by Auto_tac; |
9245 | 52 |
qed "inject_Spair_Rep"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
54 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
55 |
Goalw [Ispair_def] |
9245 | 56 |
"[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"; |
57 |
by (etac inject_Spair_Rep 1); |
|
58 |
by (atac 1); |
|
59 |
by (etac (inj_on_Abs_Sprod RS inj_onD) 1); |
|
60 |
by (rtac SprodI 1); |
|
61 |
by (rtac SprodI 1); |
|
62 |
qed "inject_Ispair"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
63 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
64 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
65 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
66 |
(* strictness and definedness of Ispair *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
67 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
68 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
69 |
Goalw [Ispair_def] |
9245 | 70 |
"(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"; |
71 |
by (etac (strict_Spair_Rep RS arg_cong) 1); |
|
72 |
qed "strict_Ispair"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
73 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
74 |
Goalw [Ispair_def] |
9245 | 75 |
"Ispair UU b = Ispair UU UU"; |
76 |
by (rtac (strict_Spair_Rep RS arg_cong) 1); |
|
77 |
by (rtac disjI1 1); |
|
78 |
by (rtac refl 1); |
|
79 |
qed "strict_Ispair1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
80 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
81 |
Goalw [Ispair_def] |
9245 | 82 |
"Ispair a UU = Ispair UU UU"; |
83 |
by (rtac (strict_Spair_Rep RS arg_cong) 1); |
|
84 |
by (rtac disjI2 1); |
|
85 |
by (rtac refl 1); |
|
86 |
qed "strict_Ispair2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
87 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
88 |
Goal "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"; |
9245 | 89 |
by (rtac (de_Morgan_disj RS subst) 1); |
10230 | 90 |
by (etac contrapos_nn 1); |
9245 | 91 |
by (etac strict_Ispair 1); |
92 |
qed "strict_Ispair_rev"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
93 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
94 |
Goalw [Ispair_def] |
9245 | 95 |
"Ispair a b = Ispair UU UU ==> (a = UU | b = UU)"; |
96 |
by (rtac defined_Spair_Rep_rev 1); |
|
97 |
by (rtac (inj_on_Abs_Sprod RS inj_onD) 1); |
|
98 |
by (atac 1); |
|
99 |
by (rtac SprodI 1); |
|
100 |
by (rtac SprodI 1); |
|
101 |
qed "defined_Ispair_rev"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
102 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
103 |
Goal "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"; |
10230 | 104 |
by (rtac contrapos_nn 1); |
9245 | 105 |
by (etac defined_Ispair_rev 2); |
106 |
by (rtac (de_Morgan_disj RS iffD2) 1); |
|
107 |
by (etac conjI 1); |
|
108 |
by (atac 1); |
|
109 |
qed "defined_Ispair"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
110 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
111 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
112 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
113 |
(* Exhaustion of the strict product ** *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
114 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
115 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
116 |
Goalw [Ispair_def] |
9245 | 117 |
"z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"; |
118 |
by (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1); |
|
119 |
by (etac exE 1); |
|
120 |
by (etac exE 1); |
|
121 |
by (rtac (excluded_middle RS disjE) 1); |
|
122 |
by (rtac disjI2 1); |
|
123 |
by (rtac exI 1); |
|
124 |
by (rtac exI 1); |
|
125 |
by (rtac conjI 1); |
|
126 |
by (rtac (Rep_Sprod_inverse RS sym RS trans) 1); |
|
127 |
by (etac arg_cong 1); |
|
128 |
by (rtac (de_Morgan_disj RS subst) 1); |
|
129 |
by (atac 1); |
|
130 |
by (rtac disjI1 1); |
|
131 |
by (rtac (Rep_Sprod_inverse RS sym RS trans) 1); |
|
132 |
by (res_inst_tac [("f","Abs_Sprod")] arg_cong 1); |
|
133 |
by (etac trans 1); |
|
134 |
by (etac strict_Spair_Rep 1); |
|
135 |
qed "Exh_Sprod"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
136 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
137 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
138 |
(* general elimination rule for strict product *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
139 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
140 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
141 |
val [prem1,prem2] = Goal |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
142 |
" [| p=Ispair UU UU ==> Q ; !!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] \ |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
143 |
\ ==> Q"; |
9245 | 144 |
by (rtac (Exh_Sprod RS disjE) 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
145 |
by (etac prem1 1); |
9245 | 146 |
by (etac exE 1); |
147 |
by (etac exE 1); |
|
148 |
by (etac conjE 1); |
|
149 |
by (etac conjE 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
150 |
by (etac prem2 1); |
9245 | 151 |
by (atac 1); |
152 |
by (atac 1); |
|
153 |
qed "IsprodE"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
154 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
155 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
156 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
157 |
(* some results about the selectors Isfst, Issnd *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
158 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
159 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
160 |
Goalw [Isfst_def] "p=Ispair UU UU ==> Isfst p = UU"; |
9969 | 161 |
by (rtac some_equality 1); |
9245 | 162 |
by (rtac conjI 1); |
163 |
by (fast_tac HOL_cs 1); |
|
164 |
by (strip_tac 1); |
|
165 |
by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1); |
|
166 |
by (rtac not_sym 1); |
|
167 |
by (rtac defined_Ispair 1); |
|
168 |
by (REPEAT (fast_tac HOL_cs 1)); |
|
169 |
qed "strict_Isfst"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
170 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
171 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
172 |
Goal "Isfst(Ispair UU y) = UU"; |
9245 | 173 |
by (stac strict_Ispair1 1); |
174 |
by (rtac strict_Isfst 1); |
|
175 |
by (rtac refl 1); |
|
176 |
qed "strict_Isfst1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
177 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
178 |
Addsimps [strict_Isfst1]; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
179 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
180 |
Goal "Isfst(Ispair x UU) = UU"; |
9245 | 181 |
by (stac strict_Ispair2 1); |
182 |
by (rtac strict_Isfst 1); |
|
183 |
by (rtac refl 1); |
|
184 |
qed "strict_Isfst2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
185 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
186 |
Addsimps [strict_Isfst2]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
187 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
188 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
189 |
Goalw [Issnd_def] "p=Ispair UU UU ==>Issnd p=UU"; |
9969 | 190 |
by (rtac some_equality 1); |
9245 | 191 |
by (rtac conjI 1); |
192 |
by (fast_tac HOL_cs 1); |
|
193 |
by (strip_tac 1); |
|
194 |
by (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1); |
|
195 |
by (rtac not_sym 1); |
|
196 |
by (rtac defined_Ispair 1); |
|
197 |
by (REPEAT (fast_tac HOL_cs 1)); |
|
198 |
qed "strict_Issnd"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
199 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
200 |
Goal "Issnd(Ispair UU y) = UU"; |
9245 | 201 |
by (stac strict_Ispair1 1); |
202 |
by (rtac strict_Issnd 1); |
|
203 |
by (rtac refl 1); |
|
204 |
qed "strict_Issnd1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
205 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
206 |
Addsimps [strict_Issnd1]; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
207 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
208 |
Goal "Issnd(Ispair x UU) = UU"; |
9245 | 209 |
by (stac strict_Ispair2 1); |
210 |
by (rtac strict_Issnd 1); |
|
211 |
by (rtac refl 1); |
|
212 |
qed "strict_Issnd2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
213 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
214 |
Addsimps [strict_Issnd2]; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
215 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
216 |
Goalw [Isfst_def] "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"; |
9969 | 217 |
by (rtac some_equality 1); |
9245 | 218 |
by (rtac conjI 1); |
219 |
by (strip_tac 1); |
|
220 |
by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1); |
|
221 |
by (etac defined_Ispair 1); |
|
222 |
by (atac 1); |
|
223 |
by (atac 1); |
|
224 |
by (strip_tac 1); |
|
225 |
by (rtac (inject_Ispair RS conjunct1) 1); |
|
226 |
by (fast_tac HOL_cs 3); |
|
227 |
by (fast_tac HOL_cs 1); |
|
228 |
by (fast_tac HOL_cs 1); |
|
229 |
by (fast_tac HOL_cs 1); |
|
230 |
qed "Isfst"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
231 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
232 |
Goalw [Issnd_def] "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"; |
9969 | 233 |
by (rtac some_equality 1); |
9245 | 234 |
by (rtac conjI 1); |
235 |
by (strip_tac 1); |
|
236 |
by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1); |
|
237 |
by (etac defined_Ispair 1); |
|
238 |
by (atac 1); |
|
239 |
by (atac 1); |
|
240 |
by (strip_tac 1); |
|
241 |
by (rtac (inject_Ispair RS conjunct2) 1); |
|
242 |
by (fast_tac HOL_cs 3); |
|
243 |
by (fast_tac HOL_cs 1); |
|
244 |
by (fast_tac HOL_cs 1); |
|
245 |
by (fast_tac HOL_cs 1); |
|
246 |
qed "Issnd"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
247 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
248 |
Goal "y~=UU ==>Isfst(Ispair x y)=x"; |
9245 | 249 |
by (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1); |
250 |
by (etac Isfst 1); |
|
251 |
by (atac 1); |
|
252 |
by (hyp_subst_tac 1); |
|
253 |
by (rtac strict_Isfst1 1); |
|
254 |
qed "Isfst2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
255 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
256 |
Goal "~x=UU ==>Issnd(Ispair x y)=y"; |
9245 | 257 |
by (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1); |
258 |
by (etac Issnd 1); |
|
259 |
by (atac 1); |
|
260 |
by (hyp_subst_tac 1); |
|
261 |
by (rtac strict_Issnd2 1); |
|
262 |
qed "Issnd2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
263 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
264 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
265 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
266 |
(* instantiate the simplifier *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
267 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
268 |
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
269 |
val Sprod0_ss = |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
270 |
HOL_ss |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
271 |
addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2, |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
272 |
Isfst2,Issnd2]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
273 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
274 |
Addsimps [Isfst2,Issnd2]; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
275 |
|
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
276 |
Goal "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"; |
9245 | 277 |
by (res_inst_tac [("p","p")] IsprodE 1); |
278 |
by (contr_tac 1); |
|
279 |
by (hyp_subst_tac 1); |
|
280 |
by (rtac conjI 1); |
|
281 |
by (asm_simp_tac Sprod0_ss 1); |
|
282 |
by (asm_simp_tac Sprod0_ss 1); |
|
283 |
qed "defined_IsfstIssnd"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
284 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
285 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
286 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
287 |
(* Surjective pairing: equivalent to Exh_Sprod *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
288 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
289 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
290 |
Goal "z = Ispair(Isfst z)(Issnd z)"; |
9245 | 291 |
by (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1); |
292 |
by (asm_simp_tac Sprod0_ss 1); |
|
293 |
by (etac exE 1); |
|
294 |
by (etac exE 1); |
|
295 |
by (asm_simp_tac Sprod0_ss 1); |
|
296 |
qed "surjective_pairing_Sprod"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
297 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
298 |
Goal "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"; |
9245 | 299 |
by (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1); |
300 |
by (rotate_tac ~1 1); |
|
13601 | 301 |
by (asm_lr_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1); |
9245 | 302 |
by (Asm_simp_tac 1); |
303 |
qed "Sel_injective_Sprod"; |