src/HOLCF/Sprod1.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 3323 194ae2e0c193
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Sprod1.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory Sprod1.thy
     7 *)
     8 
     9 open Sprod1;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* less_sprod is a partial order on Sprod                                   *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "refl_less_sprod" thy [less_sprod_def]"(p::'a ** 'b) << p"
    16 (fn prems => [(fast_tac (HOL_cs addIs [refl_less]) 1)]);
    17 
    18 qed_goalw "antisym_less_sprod" thy [less_sprod_def]
    19         "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
    20 (fn prems =>
    21         [
    22         (cut_facts_tac prems 1),
    23         (rtac Sel_injective_Sprod 1),
    24         (fast_tac (HOL_cs addIs [antisym_less]) 1),
    25         (fast_tac (HOL_cs addIs [antisym_less]) 1)
    26         ]);
    27 
    28 qed_goalw "trans_less_sprod" thy [less_sprod_def]
    29         "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
    30 (fn prems =>
    31         [
    32         (cut_facts_tac prems 1),
    33         (rtac conjI 1),
    34         (fast_tac (HOL_cs addIs [trans_less]) 1),
    35         (fast_tac (HOL_cs addIs [trans_less]) 1)
    36         ]);