src/HOLCF/Discrete1.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5192 704dd3a6d47d
child 11346 0d28bc664955
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Discrete1.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997 TUM
     5 
     6 Proves that 'a discr is a cpo
     7 *)
     8 
     9 Goalw [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
    10 by (rtac refl 1);
    11 qed "discr_less_eq";
    12 AddIffs [discr_less_eq];
    13 
    14 Goalw [chain]
    15  "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
    16 by (induct_tac "i" 1);
    17 by (rtac refl 1);
    18 by (etac subst 1);
    19 by (rtac sym 1);
    20 by (Fast_tac 1);
    21 qed "discr_chain0";
    22 
    23 Goal
    24  "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
    25 by (fast_tac (claset() addEs [discr_chain0]) 1);
    26 qed "discr_chain_range0";
    27 Addsimps [discr_chain_range0];
    28 
    29 Goalw [is_lub,is_ub]
    30  "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
    31 by (Asm_simp_tac 1);
    32 qed "discr_cpo";