Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Discrete0.ML
author paulson
Wed, 23 Jul 1997 11:52:22 +0200
changeset 3564 f886dbd91ee5
parent 3323 194ae2e0c193
child 5068 fb28eaa07e01
permissions -rw-r--r--
Now Datatype.occs_in_prems prints the necessary warning ITSELF. It is also easier to invoke and even works if the induction variable is a parameter (rather than a free variable).
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/Discrete0.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
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset 
     4
 
    Copyright   1997 TUM
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


Proves that 'a discr is a po













c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




     7


*)













c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




     8









3323






194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord



slotosch


parents: 
3018

diff
changeset




     9


goalw thy [less_discr_def] "(x::('a::term)discr) << x";








3018






e65b60b28341
Ran expandshort



paulson


parents: 
2841

diff
changeset




    10


by (rtac refl 1);








2841






c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




    11


qed "less_discr_refl";













c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




    12














c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




    13


goalw thy [less_discr_def]








3323






194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord



slotosch


parents: 
3018

diff
changeset




    14


  "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x <<  z";








3018






e65b60b28341
Ran expandshort



paulson


parents: 
2841

diff
changeset




    15


by (etac trans 1);













e65b60b28341
Ran expandshort



paulson


parents: 
2841

diff
changeset




    16


by (assume_tac 1);








2841






c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




    17


qed "less_discr_trans";













c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




    18














c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




    19


goalw thy [less_discr_def]








3323






194ae2e0c193
eliminated the constant less by the introduction of the axclass sq_ord



slotosch


parents: 
3018

diff
changeset




    20


  "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";








3018






e65b60b28341
Ran expandshort



paulson


parents: 
2841

diff
changeset




    21


by (assume_tac 1);








2841






c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"



nipkow


parents: 

diff
changeset




    22


qed "less_discr_antisym";















isabelle