src/HOLCF/Up1.thy
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     1
(*  Title:      HOLCF/Up1.thy
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     2
    ID:         $Id$
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     3
    Author:     Franz Regensburger
12030
wenzelm
parents: 10834
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     5
12030
wenzelm
parents: 10834
diff changeset
     6
Lifting.
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     7
*)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     8
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 6543
diff changeset
     9
Up1 = Cfun3 + Sum_Type + Datatype +
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    10
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    11
(* new type for lifting *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    12
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2278
diff changeset
    13
typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    14
3323
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents: 2640
diff changeset
    15
instance u :: (sq_ord)sq_ord
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents: 2640
diff changeset
    16
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    17
consts
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    18
  Iup         :: "'a => ('a)u"
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    19
  Ifup        :: "('a->'b)=>('a)u => 'b"
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    20
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    21
defs
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    22
  Iup_def     "Iup x == Abs_Up(Inr(x))"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10212
diff changeset
    23
  Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f$z"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3323
diff changeset
    24
  less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    25
               Inl(y1) => True          
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    26
             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    27
                                            | Inr(z2) => y2<<z2))"
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    28
end