9 |
9 |
10 (* ------------------------------------------------------------------------ *) |
10 (* ------------------------------------------------------------------------ *) |
11 (* less_cprod is a partial order on 'a * 'b *) |
11 (* less_cprod is a partial order on 'a * 'b *) |
12 (* ------------------------------------------------------------------------ *) |
12 (* ------------------------------------------------------------------------ *) |
13 |
13 |
14 val prems = goal Prod.thy |
14 Goal "[|fst x = fst y; snd x = snd y|] ==> x = y"; |
15 "[|fst x = fst y; snd x = snd y|] ==> x = y"; |
|
16 by (cut_facts_tac prems 1); |
|
17 by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1); |
15 by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1); |
18 by (rotate_tac ~1 1); |
16 by (rotate_tac ~1 1); |
19 by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1); |
17 by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1); |
20 by (asm_simp_tac (simpset_of Prod.thy) 1); |
18 by (asm_simp_tac (simpset_of Prod.thy) 1); |
21 qed "Sel_injective_cprod"; |
19 qed "Sel_injective_cprod"; |
22 |
20 |
23 val prems = goalw Cprod1.thy [less_cprod_def] "(p::'a*'b) << p"; |
21 Goalw [less_cprod_def] "(p::'a*'b) << p"; |
24 by (Simp_tac 1); |
22 by (Simp_tac 1); |
25 qed "refl_less_cprod"; |
23 qed "refl_less_cprod"; |
26 |
24 |
27 Goalw [less_cprod_def] "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"; |
25 Goalw [less_cprod_def] "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"; |
28 by (rtac Sel_injective_cprod 1); |
26 by (rtac Sel_injective_cprod 1); |
29 by (fast_tac (HOL_cs addIs [antisym_less]) 1); |
27 by (fast_tac (HOL_cs addIs [antisym_less]) 1); |
30 by (fast_tac (HOL_cs addIs [antisym_less]) 1); |
28 by (fast_tac (HOL_cs addIs [antisym_less]) 1); |
31 qed "antisym_less_cprod"; |
29 qed "antisym_less_cprod"; |
32 |
30 |
33 val prems = goalw thy [less_cprod_def] |
31 Goalw [less_cprod_def] |
34 "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"; |
32 "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"; |
35 by (cut_facts_tac prems 1); |
|
36 by (rtac conjI 1); |
33 by (rtac conjI 1); |
37 by (fast_tac (HOL_cs addIs [trans_less]) 1); |
34 by (fast_tac (HOL_cs addIs [trans_less]) 1); |
38 by (fast_tac (HOL_cs addIs [trans_less]) 1); |
35 by (fast_tac (HOL_cs addIs [trans_less]) 1); |
39 qed "trans_less_cprod"; |
36 qed "trans_less_cprod"; |