author | oheimb |
Thu, 01 Feb 2001 20:51:48 +0100 | |
changeset 11025 | a70b796d9af8 |
parent 10212 | 33fe2d701ddd |
child 11343 | d5f1b482bfbf |
permissions | -rw-r--r-- |
slotosch@2640 | 1 |
(* Title: HOLCF/Cprod1.ML |
nipkow@243 | 2 |
ID: $Id$ |
clasohm@1461 | 3 |
Author: Franz Regensburger |
nipkow@243 | 4 |
Copyright 1993 Technische Universitaet Muenchen |
nipkow@243 | 5 |
|
nipkow@10212 | 6 |
Partial ordering for cartesian product of HOL theory Product_Type.thy |
nipkow@243 | 7 |
*) |
nipkow@243 | 8 |
|
nipkow@243 | 9 |
|
nipkow@243 | 10 |
(* ------------------------------------------------------------------------ *) |
nipkow@243 | 11 |
(* less_cprod is a partial order on 'a * 'b *) |
nipkow@243 | 12 |
(* ------------------------------------------------------------------------ *) |
nipkow@243 | 13 |
|
oheimb@11025 | 14 |
(*###TO Product_Type_lemmas.ML *) |
paulson@9248 | 15 |
Goal "[|fst x = fst y; snd x = snd y|] ==> x = y"; |
paulson@9245 | 16 |
by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1); |
paulson@9245 | 17 |
by (rotate_tac ~1 1); |
paulson@9245 | 18 |
by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1); |
oheimb@11025 | 19 |
by (asm_simp_tac (simpset_of (theory "Product_Type")) 1); |
paulson@9245 | 20 |
qed "Sel_injective_cprod"; |
slotosch@2640 | 21 |
|
paulson@9248 | 22 |
Goalw [less_cprod_def] "(p::'a*'b) << p"; |
paulson@9245 | 23 |
by (Simp_tac 1); |
paulson@9245 | 24 |
qed "refl_less_cprod"; |
nipkow@243 | 25 |
|
paulson@9245 | 26 |
Goalw [less_cprod_def] "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"; |
paulson@9245 | 27 |
by (rtac Sel_injective_cprod 1); |
paulson@9245 | 28 |
by (fast_tac (HOL_cs addIs [antisym_less]) 1); |
paulson@9245 | 29 |
by (fast_tac (HOL_cs addIs [antisym_less]) 1); |
paulson@9245 | 30 |
qed "antisym_less_cprod"; |
nipkow@243 | 31 |
|
paulson@9248 | 32 |
Goalw [less_cprod_def] |
paulson@9245 | 33 |
"[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"; |
paulson@9245 | 34 |
by (rtac conjI 1); |
paulson@9245 | 35 |
by (fast_tac (HOL_cs addIs [trans_less]) 1); |
paulson@9245 | 36 |
by (fast_tac (HOL_cs addIs [trans_less]) 1); |
paulson@9245 | 37 |
qed "trans_less_cprod"; |