12 (* reduction properties for less_sprod *) |
12 (* reduction properties for less_sprod *) |
13 (* ------------------------------------------------------------------------ *) |
13 (* ------------------------------------------------------------------------ *) |
14 |
14 |
15 |
15 |
16 qed_goalw "less_sprod1a" Sprod1.thy [less_sprod_def] |
16 qed_goalw "less_sprod1a" Sprod1.thy [less_sprod_def] |
17 "p1=Ispair UU UU ==> less_sprod p1 p2" |
17 "p1=Ispair UU UU ==> less_sprod p1 p2" |
18 (fn prems => |
18 (fn prems => |
19 [ |
19 [ |
20 (cut_facts_tac prems 1), |
20 (cut_facts_tac prems 1), |
21 (asm_simp_tac HOL_ss 1) |
21 (asm_simp_tac HOL_ss 1) |
22 ]); |
22 ]); |
23 |
23 |
24 qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def] |
24 qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def] |
25 "p1~=Ispair UU UU ==> \ |
25 "p1~=Ispair UU UU ==> \ |
26 \ less_sprod p1 p2 = ( Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2)" |
26 \ less_sprod p1 p2 = ( Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2)" |
27 (fn prems => |
27 (fn prems => |
28 [ |
28 [ |
29 (cut_facts_tac prems 1), |
29 (cut_facts_tac prems 1), |
30 (asm_simp_tac HOL_ss 1) |
30 (asm_simp_tac HOL_ss 1) |
31 ]); |
31 ]); |
32 |
32 |
33 qed_goal "less_sprod2a" Sprod1.thy |
33 qed_goal "less_sprod2a" Sprod1.thy |
34 "less_sprod(Ispair x y)(Ispair UU UU) ==> x = UU | y = UU" |
34 "less_sprod(Ispair x y)(Ispair UU UU) ==> x = UU | y = UU" |
35 (fn prems => |
35 (fn prems => |
36 [ |
36 [ |
37 (cut_facts_tac prems 1), |
37 (cut_facts_tac prems 1), |
38 (rtac (excluded_middle RS disjE) 1), |
38 (rtac (excluded_middle RS disjE) 1), |
39 (atac 2), |
39 (atac 2), |
40 (rtac disjI1 1), |
40 (rtac disjI1 1), |
41 (rtac antisym_less 1), |
41 (rtac antisym_less 1), |
42 (rtac minimal 2), |
42 (rtac minimal 2), |
43 (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1), |
43 (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1), |
44 (rtac Isfst 1), |
44 (rtac Isfst 1), |
45 (fast_tac HOL_cs 1), |
45 (fast_tac HOL_cs 1), |
46 (fast_tac HOL_cs 1), |
46 (fast_tac HOL_cs 1), |
47 (res_inst_tac [("s","Isfst(Ispair UU UU)"),("t","UU")] subst 1), |
47 (res_inst_tac [("s","Isfst(Ispair UU UU)"),("t","UU")] subst 1), |
48 (simp_tac Sprod0_ss 1), |
48 (simp_tac Sprod0_ss 1), |
49 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1), |
49 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1), |
50 (REPEAT (fast_tac HOL_cs 1)) |
50 (REPEAT (fast_tac HOL_cs 1)) |
51 ]); |
51 ]); |
52 |
52 |
53 qed_goal "less_sprod2b" Sprod1.thy |
53 qed_goal "less_sprod2b" Sprod1.thy |
54 "less_sprod p (Ispair UU UU) ==> p = Ispair UU UU" |
54 "less_sprod p (Ispair UU UU) ==> p = Ispair UU UU" |
55 (fn prems => |
55 (fn prems => |
56 [ |
56 [ |
57 (cut_facts_tac prems 1), |
57 (cut_facts_tac prems 1), |
58 (res_inst_tac [("p","p")] IsprodE 1), |
58 (res_inst_tac [("p","p")] IsprodE 1), |
59 (atac 1), |
59 (atac 1), |
60 (hyp_subst_tac 1), |
60 (hyp_subst_tac 1), |
61 (rtac strict_Ispair 1), |
61 (rtac strict_Ispair 1), |
62 (etac less_sprod2a 1) |
62 (etac less_sprod2a 1) |
63 ]); |
63 ]); |
64 |
64 |
65 qed_goal "less_sprod2c" Sprod1.thy |
65 qed_goal "less_sprod2c" Sprod1.thy |
66 "[|less_sprod(Ispair xa ya)(Ispair x y);\ |
66 "[|less_sprod(Ispair xa ya)(Ispair x y);\ |
67 \ xa ~= UU ; ya ~= UU; x ~= UU ; y ~= UU |] ==> xa << x & ya << y" |
67 \ xa ~= UU ; ya ~= UU; x ~= UU ; y ~= UU |] ==> xa << x & ya << y" |
68 (fn prems => |
68 (fn prems => |
69 [ |
69 [ |
70 (rtac conjI 1), |
70 (rtac conjI 1), |
71 (res_inst_tac [("s","Isfst(Ispair xa ya)"),("t","xa")] subst 1), |
71 (res_inst_tac [("s","Isfst(Ispair xa ya)"),("t","xa")] subst 1), |
72 (simp_tac (Sprod0_ss addsimps prems)1), |
72 (simp_tac (Sprod0_ss addsimps prems)1), |
73 (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1), |
73 (res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1), |
74 (simp_tac (Sprod0_ss addsimps prems)1), |
74 (simp_tac (Sprod0_ss addsimps prems)1), |
75 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1), |
75 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1), |
76 (resolve_tac prems 1), |
76 (resolve_tac prems 1), |
77 (resolve_tac prems 1), |
77 (resolve_tac prems 1), |
78 (simp_tac (Sprod0_ss addsimps prems)1), |
78 (simp_tac (Sprod0_ss addsimps prems)1), |
79 (res_inst_tac [("s","Issnd(Ispair xa ya)"),("t","ya")] subst 1), |
79 (res_inst_tac [("s","Issnd(Ispair xa ya)"),("t","ya")] subst 1), |
80 (simp_tac (Sprod0_ss addsimps prems)1), |
80 (simp_tac (Sprod0_ss addsimps prems)1), |
81 (res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1), |
81 (res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1), |
82 (simp_tac (Sprod0_ss addsimps prems)1), |
82 (simp_tac (Sprod0_ss addsimps prems)1), |
83 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1), |
83 (rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1), |
84 (resolve_tac prems 1), |
84 (resolve_tac prems 1), |
85 (resolve_tac prems 1), |
85 (resolve_tac prems 1), |
86 (simp_tac (Sprod0_ss addsimps prems)1) |
86 (simp_tac (Sprod0_ss addsimps prems)1) |
87 ]); |
87 ]); |
88 |
88 |
89 (* ------------------------------------------------------------------------ *) |
89 (* ------------------------------------------------------------------------ *) |
90 (* less_sprod is a partial order on Sprod *) |
90 (* less_sprod is a partial order on Sprod *) |
91 (* ------------------------------------------------------------------------ *) |
91 (* ------------------------------------------------------------------------ *) |
92 |
92 |
93 qed_goal "refl_less_sprod" Sprod1.thy "less_sprod p p" |
93 qed_goal "refl_less_sprod" Sprod1.thy "less_sprod p p" |
94 (fn prems => |
94 (fn prems => |
95 [ |
95 [ |
96 (res_inst_tac [("p","p")] IsprodE 1), |
96 (res_inst_tac [("p","p")] IsprodE 1), |
97 (etac less_sprod1a 1), |
97 (etac less_sprod1a 1), |
98 (hyp_subst_tac 1), |
98 (hyp_subst_tac 1), |
99 (rtac (less_sprod1b RS ssubst) 1), |
99 (rtac (less_sprod1b RS ssubst) 1), |
100 (rtac defined_Ispair 1), |
100 (rtac defined_Ispair 1), |
101 (REPEAT (fast_tac (HOL_cs addIs [refl_less]) 1)) |
101 (REPEAT (fast_tac (HOL_cs addIs [refl_less]) 1)) |
102 ]); |
102 ]); |
103 |
103 |
104 |
104 |
105 qed_goal "antisym_less_sprod" Sprod1.thy |
105 qed_goal "antisym_less_sprod" Sprod1.thy |
106 "[|less_sprod p1 p2;less_sprod p2 p1|] ==> p1=p2" |
106 "[|less_sprod p1 p2;less_sprod p2 p1|] ==> p1=p2" |
107 (fn prems => |
107 (fn prems => |
108 [ |
108 [ |
109 (cut_facts_tac prems 1), |
109 (cut_facts_tac prems 1), |
110 (res_inst_tac [("p","p1")] IsprodE 1), |
110 (res_inst_tac [("p","p1")] IsprodE 1), |
111 (hyp_subst_tac 1), |
111 (hyp_subst_tac 1), |
112 (res_inst_tac [("p","p2")] IsprodE 1), |
112 (res_inst_tac [("p","p2")] IsprodE 1), |
113 (hyp_subst_tac 1), |
113 (hyp_subst_tac 1), |
114 (rtac refl 1), |
114 (rtac refl 1), |
115 (hyp_subst_tac 1), |
115 (hyp_subst_tac 1), |
116 (rtac (strict_Ispair RS sym) 1), |
116 (rtac (strict_Ispair RS sym) 1), |
117 (etac less_sprod2a 1), |
117 (etac less_sprod2a 1), |
118 (hyp_subst_tac 1), |
118 (hyp_subst_tac 1), |
119 (res_inst_tac [("p","p2")] IsprodE 1), |
119 (res_inst_tac [("p","p2")] IsprodE 1), |
120 (hyp_subst_tac 1), |
120 (hyp_subst_tac 1), |
121 (rtac (strict_Ispair) 1), |
121 (rtac (strict_Ispair) 1), |
122 (etac less_sprod2a 1), |
122 (etac less_sprod2a 1), |
123 (hyp_subst_tac 1), |
123 (hyp_subst_tac 1), |
124 (res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1), |
124 (res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1), |
125 (rtac antisym_less 1), |
125 (rtac antisym_less 1), |
126 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1), |
126 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1), |
127 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1), |
127 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1), |
128 (rtac antisym_less 1), |
128 (rtac antisym_less 1), |
129 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1), |
129 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1), |
130 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1) |
130 (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1) |
131 ]); |
131 ]); |
132 |
132 |
133 qed_goal "trans_less_sprod" Sprod1.thy |
133 qed_goal "trans_less_sprod" Sprod1.thy |
134 "[|less_sprod (p1::'a**'b) p2;less_sprod p2 p3|] ==> less_sprod p1 p3" |
134 "[|less_sprod (p1::'a**'b) p2;less_sprod p2 p3|] ==> less_sprod p1 p3" |
135 (fn prems => |
135 (fn prems => |
136 [ |
136 [ |
137 (cut_facts_tac prems 1), |
137 (cut_facts_tac prems 1), |
138 (res_inst_tac [("p","p1")] IsprodE 1), |
138 (res_inst_tac [("p","p1")] IsprodE 1), |
139 (etac less_sprod1a 1), |
139 (etac less_sprod1a 1), |
140 (hyp_subst_tac 1), |
140 (hyp_subst_tac 1), |
141 (res_inst_tac [("p","p3")] IsprodE 1), |
141 (res_inst_tac [("p","p3")] IsprodE 1), |
142 (hyp_subst_tac 1), |
142 (hyp_subst_tac 1), |
143 (res_inst_tac [("s","p2"),("t","Ispair (UU::'a)(UU::'b)")] subst 1), |
143 (res_inst_tac [("s","p2"),("t","Ispair (UU::'a)(UU::'b)")] subst 1), |
144 (etac less_sprod2b 1), |
144 (etac less_sprod2b 1), |
145 (atac 1), |
145 (atac 1), |
146 (hyp_subst_tac 1), |
146 (hyp_subst_tac 1), |
147 (res_inst_tac [("Q","p2=Ispair(UU::'a)(UU::'b)")] |
147 (res_inst_tac [("Q","p2=Ispair(UU::'a)(UU::'b)")] |
148 (excluded_middle RS disjE) 1), |
148 (excluded_middle RS disjE) 1), |
149 (rtac (defined_Ispair RS less_sprod1b RS ssubst) 1), |
149 (rtac (defined_Ispair RS less_sprod1b RS ssubst) 1), |
150 (REPEAT (atac 1)), |
150 (REPEAT (atac 1)), |
151 (rtac conjI 1), |
151 (rtac conjI 1), |
152 (res_inst_tac [("y","Isfst(p2)")] trans_less 1), |
152 (res_inst_tac [("y","Isfst(p2)")] trans_less 1), |
153 (rtac conjunct1 1), |
153 (rtac conjunct1 1), |
154 (rtac (less_sprod1b RS subst) 1), |
154 (rtac (less_sprod1b RS subst) 1), |
155 (rtac defined_Ispair 1), |
155 (rtac defined_Ispair 1), |
156 (REPEAT (atac 1)), |
156 (REPEAT (atac 1)), |
157 (rtac conjunct1 1), |
157 (rtac conjunct1 1), |
158 (rtac (less_sprod1b RS subst) 1), |
158 (rtac (less_sprod1b RS subst) 1), |
159 (REPEAT (atac 1)), |
159 (REPEAT (atac 1)), |
160 (res_inst_tac [("y","Issnd(p2)")] trans_less 1), |
160 (res_inst_tac [("y","Issnd(p2)")] trans_less 1), |
161 (rtac conjunct2 1), |
161 (rtac conjunct2 1), |
162 (rtac (less_sprod1b RS subst) 1), |
162 (rtac (less_sprod1b RS subst) 1), |
163 (rtac defined_Ispair 1), |
163 (rtac defined_Ispair 1), |
164 (REPEAT (atac 1)), |
164 (REPEAT (atac 1)), |
165 (rtac conjunct2 1), |
165 (rtac conjunct2 1), |
166 (rtac (less_sprod1b RS subst) 1), |
166 (rtac (less_sprod1b RS subst) 1), |
167 (REPEAT (atac 1)), |
167 (REPEAT (atac 1)), |
168 (hyp_subst_tac 1), |
168 (hyp_subst_tac 1), |
169 (res_inst_tac [("s","Ispair(UU::'a)(UU::'b)"),("t","Ispair x y")] |
169 (res_inst_tac [("s","Ispair(UU::'a)(UU::'b)"),("t","Ispair x y")] |
170 subst 1), |
170 subst 1), |
171 (etac (less_sprod2b RS sym) 1), |
171 (etac (less_sprod2b RS sym) 1), |
172 (atac 1) |
172 (atac 1) |
173 ]); |
173 ]); |
174 |
174 |
175 |
175 |
176 |
176 |
177 |
177 |
178 |
178 |