src/HOLCF/Sprod1.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15567 60743edae74a
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/Sprod1.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 *)
     5 
     6 (* ------------------------------------------------------------------------ *)
     7 (* less_sprod is a partial order on Sprod                                   *)
     8 (* ------------------------------------------------------------------------ *)
     9 
    10 Goalw [less_sprod_def]"(p::'a ** 'b) << p";
    11 by (fast_tac (HOL_cs addIs [refl_less]) 1);
    12 qed "refl_less_sprod";
    13 
    14 Goalw [less_sprod_def]
    15         "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2";
    16 by (rtac Sel_injective_Sprod 1);
    17 by (fast_tac (HOL_cs addIs [antisym_less]) 1);
    18 by (fast_tac (HOL_cs addIs [antisym_less]) 1);
    19 qed "antisym_less_sprod";
    20 
    21 Goalw [less_sprod_def]
    22         "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3";
    23 by (blast_tac (HOL_cs addIs [trans_less]) 1);
    24 qed "trans_less_sprod";