equal
deleted
inserted
replaced
39 THEN (etac sym 1)) |
39 THEN (etac sym 1)) |
40 |
40 |
41 in |
41 in |
42 |
42 |
43 val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def] |
43 val less_ssum1a = prove_goalw Ssum1.thy [less_ssum_def] |
44 "[|s1=Isinl(x); s2=Isinl(y)|] ==> less_ssum(s1,s2) = (x << y)" |
44 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less_ssum(s1,s2) = (x << y)" |
45 (fn prems => |
45 (fn prems => |
46 [ |
46 [ |
47 (cut_facts_tac prems 1), |
47 (cut_facts_tac prems 1), |
48 (rtac select_equality 1), |
48 (rtac select_equality 1), |
49 (dtac conjunct1 2), |
49 (dtac conjunct1 2), |
68 (etac conjE 1), |
68 (etac conjE 1), |
69 (eq_left "x" "u"), |
69 (eq_left "x" "u"), |
70 (UU_left "y"), |
70 (UU_left "y"), |
71 (rtac iffI 1), |
71 (rtac iffI 1), |
72 (etac UU_I 1), |
72 (etac UU_I 1), |
73 (res_inst_tac [("s","x"),("t","UU")] subst 1), |
73 (res_inst_tac [("s","x"),("t","UU::'a")] subst 1), |
74 (atac 1), |
74 (atac 1), |
75 (rtac refl_less 1), |
75 (rtac refl_less 1), |
76 (strip_tac 1), |
76 (strip_tac 1), |
77 (etac conjE 1), |
77 (etac conjE 1), |
78 (UU_left "x"), |
78 (UU_left "x"), |
80 (simp_tac Cfun_ss 1) |
80 (simp_tac Cfun_ss 1) |
81 ]); |
81 ]); |
82 |
82 |
83 |
83 |
84 val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def] |
84 val less_ssum1b = prove_goalw Ssum1.thy [less_ssum_def] |
85 "[|s1=Isinr(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x << y)" |
85 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = (x << y)" |
86 (fn prems => |
86 (fn prems => |
87 [ |
87 [ |
88 (cut_facts_tac prems 1), |
88 (cut_facts_tac prems 1), |
89 (rtac select_equality 1), |
89 (rtac select_equality 1), |
90 (dtac conjunct2 2), |
90 (dtac conjunct2 2), |
115 (etac conjE 1), |
115 (etac conjE 1), |
116 (eq_right "x" "v"), |
116 (eq_right "x" "v"), |
117 (UU_right "y"), |
117 (UU_right "y"), |
118 (rtac iffI 1), |
118 (rtac iffI 1), |
119 (etac UU_I 1), |
119 (etac UU_I 1), |
120 (res_inst_tac [("s","UU"),("t","x")] subst 1), |
120 (res_inst_tac [("s","UU::'b"),("t","x")] subst 1), |
121 (etac sym 1), |
121 (etac sym 1), |
122 (rtac refl_less 1) |
122 (rtac refl_less 1) |
123 ]); |
123 ]); |
124 |
124 |
125 |
125 |
126 val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def] |
126 val less_ssum1c = prove_goalw Ssum1.thy [less_ssum_def] |
127 "[|s1=Isinl(x); s2=Isinr(y)|] ==> less_ssum(s1,s2) = (x = UU)" |
127 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less_ssum(s1,s2) = ((x::'a) = UU)" |
128 (fn prems => |
128 (fn prems => |
129 [ |
129 [ |
130 (cut_facts_tac prems 1), |
130 (cut_facts_tac prems 1), |
131 (rtac select_equality 1), |
131 (rtac select_equality 1), |
132 (rtac conjI 1), |
132 (rtac conjI 1), |
133 (strip_tac 1), |
133 (strip_tac 1), |
134 (etac conjE 1), |
134 (etac conjE 1), |
135 (eq_left "x" "u"), |
135 (eq_left "x" "u"), |
136 (UU_left "xa"), |
136 (UU_left "xa"), |
137 (rtac iffI 1), |
137 (rtac iffI 1), |
138 (res_inst_tac [("s","x"),("t","UU")] subst 1), |
138 (res_inst_tac [("s","x"),("t","UU::'a")] subst 1), |
139 (atac 1), |
139 (atac 1), |
140 (rtac refl_less 1), |
140 (rtac refl_less 1), |
141 (etac UU_I 1), |
141 (etac UU_I 1), |
142 (rtac conjI 1), |
142 (rtac conjI 1), |
143 (strip_tac 1), |
143 (strip_tac 1), |