equal
deleted
inserted
replaced
11 |
11 |
12 (* ------------------------------------------------------------------------ *) |
12 (* ------------------------------------------------------------------------ *) |
13 (* less_cprod is a partial order on 'a * 'b *) |
13 (* less_cprod is a partial order on 'a * 'b *) |
14 (* ------------------------------------------------------------------------ *) |
14 (* ------------------------------------------------------------------------ *) |
15 |
15 |
16 qed_goal "Sel_injective_cprod" Prod.thy |
16 qed_goal "Sel_injective_cprod" Prod.thy |
17 "[|fst x = fst y; snd x = snd y|] ==> x = y" |
17 "[|fst x = fst y; snd x = snd y|] ==> x = y" |
18 (fn prems => |
18 (fn prems => |
19 [ |
19 [ |
20 (cut_facts_tac prems 1), |
20 (cut_facts_tac prems 1), |
21 (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1), |
21 (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1), |
22 (rotate_tac ~1 1), |
22 (rotate_tac ~1 1), |
23 (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1), |
23 (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1), |
24 (Asm_simp_tac 1) |
24 (asm_simp_tac (simpset_of Prod.thy) 1) |
25 ]); |
25 ]); |
26 |
26 |
27 qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p" |
27 qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p" |
28 (fn prems => [Simp_tac 1]); |
28 (fn prems => [Simp_tac 1]); |
29 |
29 |