src/HOLCF/Discrete.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5068 fb28eaa07e01
child 11346 0d28bc664955
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Discrete.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997 TUM
     5 *)
     6 
     7 Goalw [undiscr_def] "undiscr(Discr x) = x";
     8 by (Simp_tac 1);
     9 qed "undiscr_Discr";
    10 Addsimps [undiscr_Discr];
    11 
    12 Goal
    13  "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
    14 by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
    15 qed "discr_chain_f_range0";
    16 
    17 Goalw [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
    18 by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
    19 qed "cont_discr";
    20 AddIffs [cont_discr];