|
1 (* Title: HOLCF/sprod1.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Lemmas for theory sprod1.thy |
|
7 *) |
|
8 |
|
9 open Sprod1; |
|
10 |
|
11 (* ------------------------------------------------------------------------ *) |
|
12 (* reduction properties for less_sprod *) |
|
13 (* ------------------------------------------------------------------------ *) |
|
14 |
|
15 |
|
16 val less_sprod1a = prove_goalw Sprod1.thy [less_sprod_def] |
|
17 "p1=Ispair(UU,UU) ==> less_sprod(p1,p2)" |
|
18 (fn prems => |
|
19 [ |
|
20 (cut_facts_tac prems 1), |
|
21 (rtac eqTrueE 1), |
|
22 (rtac select_equality 1), |
|
23 (rtac conjI 1), |
|
24 (fast_tac HOL_cs 1), |
|
25 (strip_tac 1), |
|
26 (contr_tac 1), |
|
27 (dtac conjunct1 1), |
|
28 (etac rev_mp 1), |
|
29 (atac 1) |
|
30 ]); |
|
31 |
|
32 val less_sprod1b = prove_goalw Sprod1.thy [less_sprod_def] |
|
33 "~p1=Ispair(UU,UU) ==> \ |
|
34 \ less_sprod(p1,p2) = ( Isfst(p1) << Isfst(p2) & Issnd(p1) << Issnd(p2))" |
|
35 (fn prems => |
|
36 [ |
|
37 (cut_facts_tac prems 1), |
|
38 (rtac select_equality 1), |
|
39 (rtac conjI 1), |
|
40 (strip_tac 1), |
|
41 (contr_tac 1), |
|
42 (fast_tac HOL_cs 1), |
|
43 (dtac conjunct2 1), |
|
44 (etac rev_mp 1), |
|
45 (atac 1) |
|
46 ]); |
|
47 |
|
48 val less_sprod2a = prove_goal Sprod1.thy |
|
49 "less_sprod(Ispair(x,y),Ispair(UU,UU)) ==> x = UU | y = UU" |
|
50 (fn prems => |
|
51 [ |
|
52 (cut_facts_tac prems 1), |
|
53 (rtac (excluded_middle RS disjE) 1), |
|
54 (atac 2), |
|
55 (rtac disjI1 1), |
|
56 (rtac antisym_less 1), |
|
57 (rtac minimal 2), |
|
58 (res_inst_tac [("s","Isfst(Ispair(x,y))"),("t","x")] subst 1), |
|
59 (rtac Isfst 1), |
|
60 (fast_tac HOL_cs 1), |
|
61 (fast_tac HOL_cs 1), |
|
62 (res_inst_tac [("s","Isfst(Ispair(UU,UU))"),("t","UU")] subst 1), |
|
63 (simp_tac Sprod_ss 1), |
|
64 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1), |
|
65 (REPEAT (fast_tac HOL_cs 1)) |
|
66 ]); |
|
67 |
|
68 val less_sprod2b = prove_goal Sprod1.thy |
|
69 "less_sprod(p,Ispair(UU,UU)) ==> p = Ispair(UU,UU)" |
|
70 (fn prems => |
|
71 [ |
|
72 (cut_facts_tac prems 1), |
|
73 (res_inst_tac [("p","p")] IsprodE 1), |
|
74 (atac 1), |
|
75 (hyp_subst_tac 1), |
|
76 (rtac strict_Ispair 1), |
|
77 (etac less_sprod2a 1) |
|
78 ]); |
|
79 |
|
80 val less_sprod2c = prove_goal Sprod1.thy |
|
81 "[|less_sprod(Ispair(xa,ya),Ispair(x,y));\ |
|
82 \~ xa = UU ; ~ ya = UU;~ x = UU ; ~ y = UU |] ==> xa << x & ya << y" |
|
83 (fn prems => |
|
84 [ |
|
85 (rtac conjI 1), |
|
86 (res_inst_tac [("s","Isfst(Ispair(xa,ya))"),("t","xa")] subst 1), |
|
87 (simp_tac (Sprod_ss addsimps prems)1), |
|
88 (res_inst_tac [("s","Isfst(Ispair(x,y))"),("t","x")] subst 1), |
|
89 (simp_tac (Sprod_ss addsimps prems)1), |
|
90 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1), |
|
91 (resolve_tac prems 1), |
|
92 (resolve_tac prems 1), |
|
93 (simp_tac (Sprod_ss addsimps prems)1), |
|
94 (res_inst_tac [("s","Issnd(Ispair(xa,ya))"),("t","ya")] subst 1), |
|
95 (simp_tac (Sprod_ss addsimps prems)1), |
|
96 (res_inst_tac [("s","Issnd(Ispair(x,y))"),("t","y")] subst 1), |
|
97 (simp_tac (Sprod_ss addsimps prems)1), |
|
98 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1), |
|
99 (resolve_tac prems 1), |
|
100 (resolve_tac prems 1), |
|
101 (simp_tac (Sprod_ss addsimps prems)1) |
|
102 ]); |
|
103 |
|
104 (* ------------------------------------------------------------------------ *) |
|
105 (* less_sprod is a partial order on Sprod *) |
|
106 (* ------------------------------------------------------------------------ *) |
|
107 |
|
108 val refl_less_sprod = prove_goal Sprod1.thy "less_sprod(p,p)" |
|
109 (fn prems => |
|
110 [ |
|
111 (res_inst_tac [("p","p")] IsprodE 1), |
|
112 (etac less_sprod1a 1), |
|
113 (hyp_subst_tac 1), |
|
114 (rtac (less_sprod1b RS ssubst) 1), |
|
115 (rtac defined_Ispair 1), |
|
116 (REPEAT (fast_tac (HOL_cs addIs [refl_less]) 1)) |
|
117 ]); |
|
118 |
|
119 |
|
120 val antisym_less_sprod = prove_goal Sprod1.thy |
|
121 "[|less_sprod(p1,p2);less_sprod(p2,p1)|] ==> p1=p2" |
|
122 (fn prems => |
|
123 [ |
|
124 (cut_facts_tac prems 1), |
|
125 (res_inst_tac [("p","p1")] IsprodE 1), |
|
126 (hyp_subst_tac 1), |
|
127 (res_inst_tac [("p","p2")] IsprodE 1), |
|
128 (hyp_subst_tac 1), |
|
129 (rtac refl 1), |
|
130 (hyp_subst_tac 1), |
|
131 (rtac (strict_Ispair RS sym) 1), |
|
132 (etac less_sprod2a 1), |
|
133 (hyp_subst_tac 1), |
|
134 (res_inst_tac [("p","p2")] IsprodE 1), |
|
135 (hyp_subst_tac 1), |
|
136 (rtac (strict_Ispair) 1), |
|
137 (etac less_sprod2a 1), |
|
138 (hyp_subst_tac 1), |
|
139 (res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1), |
|
140 (rtac antisym_less 1), |
|
141 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1), |
|
142 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1), |
|
143 (rtac antisym_less 1), |
|
144 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1), |
|
145 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1) |
|
146 ]); |
|
147 |
|
148 val trans_less_sprod = prove_goal Sprod1.thy |
|
149 "[|less_sprod(p1,p2);less_sprod(p2,p3)|] ==> less_sprod(p1,p3)" |
|
150 (fn prems => |
|
151 [ |
|
152 (cut_facts_tac prems 1), |
|
153 (res_inst_tac [("p","p1")] IsprodE 1), |
|
154 (etac less_sprod1a 1), |
|
155 (hyp_subst_tac 1), |
|
156 (res_inst_tac [("p","p3")] IsprodE 1), |
|
157 (hyp_subst_tac 1), |
|
158 (res_inst_tac [("s","p2"),("t","Ispair(UU,UU)")] subst 1), |
|
159 (etac less_sprod2b 1), |
|
160 (atac 1), |
|
161 (hyp_subst_tac 1), |
|
162 (res_inst_tac [("Q","p2=Ispair(UU,UU)")] |
|
163 (excluded_middle RS disjE) 1), |
|
164 (rtac (defined_Ispair RS less_sprod1b RS ssubst) 1), |
|
165 (atac 1), |
|
166 (atac 1), |
|
167 (rtac conjI 1), |
|
168 (res_inst_tac [("y","Isfst(p2)")] trans_less 1), |
|
169 (rtac conjunct1 1), |
|
170 (rtac (less_sprod1b RS subst) 1), |
|
171 (rtac defined_Ispair 1), |
|
172 (atac 1), |
|
173 (atac 1), |
|
174 (atac 1), |
|
175 (rtac conjunct1 1), |
|
176 (rtac (less_sprod1b RS subst) 1), |
|
177 (atac 1), |
|
178 (atac 1), |
|
179 (res_inst_tac [("y","Issnd(p2)")] trans_less 1), |
|
180 (rtac conjunct2 1), |
|
181 (rtac (less_sprod1b RS subst) 1), |
|
182 (rtac defined_Ispair 1), |
|
183 (atac 1), |
|
184 (atac 1), |
|
185 (atac 1), |
|
186 (rtac conjunct2 1), |
|
187 (rtac (less_sprod1b RS subst) 1), |
|
188 (atac 1), |
|
189 (atac 1), |
|
190 (hyp_subst_tac 1), |
|
191 (res_inst_tac [("s","Ispair(UU,UU)"),("t","Ispair(x,y)")] subst 1), |
|
192 (etac (less_sprod2b RS sym) 1), |
|
193 (atac 1) |
|
194 ]); |
|
195 |
|
196 |
|
197 |
|
198 |
|
199 |
|
200 |
|
201 |
|
202 |
|
203 |
|
204 |