src/HOLCF/Discrete1.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5192 704dd3a6d47d
child 11346 0d28bc664955
permissions -rw-r--r--
tidying
nipkow@2841
     1
(*  Title:      HOLCF/Discrete1.ML
nipkow@2841
     2
    ID:         $Id$
nipkow@2841
     3
    Author:     Tobias Nipkow
nipkow@2841
     4
    Copyright   1997 TUM
nipkow@2841
     5
nipkow@2841
     6
Proves that 'a discr is a cpo
nipkow@2841
     7
*)
nipkow@2841
     8
wenzelm@5068
     9
Goalw [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
paulson@3018
    10
by (rtac refl 1);
nipkow@2841
    11
qed "discr_less_eq";
nipkow@2841
    12
AddIffs [discr_less_eq];
nipkow@2841
    13
wenzelm@5068
    14
Goalw [chain]
oheimb@4721
    15
 "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
berghofe@5192
    16
by (induct_tac "i" 1);
slotosch@3323
    17
by (rtac refl 1);
paulson@3018
    18
by (etac subst 1);
paulson@3018
    19
by (rtac sym 1);
paulson@3018
    20
by (Fast_tac 1);
nipkow@2841
    21
qed "discr_chain0";
nipkow@2841
    22
wenzelm@5068
    23
Goal
oheimb@4721
    24
 "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
wenzelm@4098
    25
by (fast_tac (claset() addEs [discr_chain0]) 1);
nipkow@2841
    26
qed "discr_chain_range0";
nipkow@2841
    27
Addsimps [discr_chain_range0];
nipkow@2841
    28
wenzelm@5068
    29
Goalw [is_lub,is_ub]
oheimb@4721
    30
 "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
paulson@3018
    31
by (Asm_simp_tac 1);
nipkow@2841
    32
qed "discr_cpo";