src/HOLCF/Cprod1.ML
author paulson
Wed Jul 05 16:37:52 2000 +0200 (2000-07-05)
changeset 9248 e1dee89de037
parent 9245 428385c4bc50
child 10212 33fe2d701ddd
permissions -rw-r--r--
massive tidy-up: goal -> Goal, remove use of prems, etc.
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
paulson@9245
     6
Partial ordering for cartesian product of HOL theory Prod.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
paulson@9248
    14
Goal "[|fst x = fst y; snd x = snd y|] ==> x = y";
paulson@9245
    15
by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
paulson@9245
    16
by (rotate_tac ~1 1);
paulson@9245
    17
by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
paulson@9245
    18
by (asm_simp_tac (simpset_of Prod.thy) 1);
paulson@9245
    19
qed "Sel_injective_cprod";
nipkow@243
    20
paulson@9248
    21
Goalw [less_cprod_def] "(p::'a*'b) << p";
paulson@9245
    22
by (Simp_tac 1);
paulson@9245
    23
qed "refl_less_cprod";
nipkow@243
    24
paulson@9245
    25
Goalw [less_cprod_def] "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2";
paulson@9245
    26
by (rtac Sel_injective_cprod 1);
paulson@9245
    27
by (fast_tac (HOL_cs addIs [antisym_less]) 1);
paulson@9245
    28
by (fast_tac (HOL_cs addIs [antisym_less]) 1);
paulson@9245
    29
qed "antisym_less_cprod";
nipkow@243
    30
paulson@9248
    31
Goalw [less_cprod_def]
paulson@9245
    32
        "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3";
paulson@9245
    33
by (rtac conjI 1);
paulson@9245
    34
by (fast_tac (HOL_cs addIs [trans_less]) 1);
paulson@9245
    35
by (fast_tac (HOL_cs addIs [trans_less]) 1);
paulson@9245
    36
qed "trans_less_cprod";