src/HOLCF/Discrete.ML
author wenzelm
Sat, 03 Nov 2001 01:41:26 +0100
changeset 12030 46d57d0290a2
parent 11346 0d28bc664955
child 12338 de0f4a63baa5
permissions -rw-r--r--
GPLed;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/Discrete.ML
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
12030
wenzelm
parents: 11346
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     5
*)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     6
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4721
diff changeset
     7
Goalw [undiscr_def] "undiscr(Discr x) = x";
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
     8
by (Simp_tac 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     9
qed "undiscr_Discr";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    10
Addsimps [undiscr_Discr];
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    11
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4721
diff changeset
    12
Goal
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4423
diff changeset
    13
 "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
    14
by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    15
qed "discr_chain_f_range0";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    16
11346
0d28bc664955 corrected ML names of definitions
oheimb
parents: 5068
diff changeset
    17
Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::term)discr. f x)";
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
    18
by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    19
qed "cont_discr";
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    20
AddIffs [cont_discr];