equal
deleted
inserted
replaced
34 THEN (atac 2) |
34 THEN (atac 2) |
35 THEN (etac sym 1)); |
35 THEN (etac sym 1)); |
36 |
36 |
37 Goalw [less_ssum_def] |
37 Goalw [less_ssum_def] |
38 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"; |
38 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"; |
39 by (rtac select_equality 1); |
39 by (rtac some_equality 1); |
40 by (dtac conjunct1 2); |
40 by (dtac conjunct1 2); |
41 by (dtac spec 2); |
41 by (dtac spec 2); |
42 by (dtac spec 2); |
42 by (dtac spec 2); |
43 by (etac mp 2); |
43 by (etac mp 2); |
44 by (fast_tac HOL_cs 2); |
44 by (fast_tac HOL_cs 2); |
72 qed "less_ssum1a"; |
72 qed "less_ssum1a"; |
73 |
73 |
74 |
74 |
75 Goalw [less_ssum_def] |
75 Goalw [less_ssum_def] |
76 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"; |
76 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"; |
77 by (rtac select_equality 1); |
77 by (rtac some_equality 1); |
78 by (dtac conjunct2 2); |
78 by (dtac conjunct2 2); |
79 by (dtac conjunct1 2); |
79 by (dtac conjunct1 2); |
80 by (dtac spec 2); |
80 by (dtac spec 2); |
81 by (dtac spec 2); |
81 by (dtac spec 2); |
82 by (etac mp 2); |
82 by (etac mp 2); |
111 qed "less_ssum1b"; |
111 qed "less_ssum1b"; |
112 |
112 |
113 |
113 |
114 Goalw [less_ssum_def] |
114 Goalw [less_ssum_def] |
115 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"; |
115 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"; |
116 by (rtac select_equality 1); |
116 by (rtac some_equality 1); |
117 by (rtac conjI 1); |
117 by (rtac conjI 1); |
118 by (strip_tac 1); |
118 by (strip_tac 1); |
119 by (etac conjE 1); |
119 by (etac conjE 1); |
120 by (eq_left "x" "u"); |
120 by (eq_left "x" "u"); |
121 by (UU_left "xa"); |
121 by (UU_left "xa"); |
150 qed "less_ssum1c"; |
150 qed "less_ssum1c"; |
151 |
151 |
152 |
152 |
153 Goalw [less_ssum_def] |
153 Goalw [less_ssum_def] |
154 "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"; |
154 "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"; |
155 by (rtac select_equality 1); |
155 by (rtac some_equality 1); |
156 by (dtac conjunct2 2); |
156 by (dtac conjunct2 2); |
157 by (dtac conjunct2 2); |
157 by (dtac conjunct2 2); |
158 by (dtac conjunct2 2); |
158 by (dtac conjunct2 2); |
159 by (dtac spec 2); |
159 by (dtac spec 2); |
160 by (dtac spec 2); |
160 by (dtac spec 2); |