src/HOLCF/Cprod1.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3323 194ae2e0c193
child 7661 8c3190b173aa
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Cprod1.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory Cprod1.thy 
     7 *)
     8 
     9 open Cprod1;
    10 
    11 
    12 (* ------------------------------------------------------------------------ *)
    13 (* less_cprod is a partial order on 'a * 'b                                 *)
    14 (* ------------------------------------------------------------------------ *)
    15 
    16 qed_goal "Sel_injective_cprod" Prod.thy 
    17         "[|fst x = fst y; snd x = snd y|] ==> x = y"
    18 (fn prems =>
    19         [
    20         (cut_facts_tac prems 1),
    21         (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1),
    22         (rotate_tac ~1 1),
    23         (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1),
    24         (Asm_simp_tac 1)
    25         ]);
    26 
    27 qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p"
    28  (fn prems => [Simp_tac 1]);
    29 
    30 qed_goalw "antisym_less_cprod" thy [less_cprod_def]
    31         "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
    32 (fn prems =>
    33         [
    34         (cut_facts_tac prems 1),
    35         (rtac Sel_injective_cprod 1),
    36         (fast_tac (HOL_cs addIs [antisym_less]) 1),
    37         (fast_tac (HOL_cs addIs [antisym_less]) 1)
    38         ]);
    39 
    40 qed_goalw "trans_less_cprod" thy [less_cprod_def]
    41         "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
    42 (fn prems =>
    43         [
    44         (cut_facts_tac prems 1),
    45         (rtac conjI 1),
    46         (fast_tac (HOL_cs addIs [trans_less]) 1),
    47         (fast_tac (HOL_cs addIs [trans_less]) 1)
    48         ]);