src/HOLCF/Cprod3.thy
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12114 a8e860c86252
child 14857 252d9b36bf44
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:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2394
diff changeset
     1
(*  Title:      HOLCF/Cprod3.thy
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
     3
    Author:     Franz Regensburger
12030
wenzelm
parents: 10834
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
     6
Class instance of * for class pcpo and cpo.
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
Cprod3 = Cprod2 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
2840
7e03e61612b0 generalized theorems and class instances for Cprod.
slotosch
parents: 2640
diff changeset
    11
instance "*" :: (cpo,cpo)cpo   	  (cpo_cprod)
7e03e61612b0 generalized theorems and class instances for Cprod.
slotosch
parents: 2640
diff changeset
    12
instance "*" :: (pcpo,pcpo)pcpo   (least_cprod)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    14
consts
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    15
        cpair        :: "'a -> 'b -> ('a*'b)" (* continuous pairing *)
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    16
        cfst         :: "('a*'b)->'a"
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    17
        csnd         :: "('a*'b)->'b"
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    18
        csplit       :: "('a->'b->'c)->('a*'b)->'c"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    19
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    20
syntax
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    21
        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 752
diff changeset
    22
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    23
translations
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    24
        "<x, y, z>"   == "<x, <y, z>>"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 4191
diff changeset
    25
        "<x, y>"      == "cpair$x$y"
625
119391dd1d59 New version
nipkow
parents: 442
diff changeset
    26
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 752
diff changeset
    27
defs
1479
21eb5e156d91 expanded tabs
clasohm
parents: 1274
diff changeset
    28
cpair_def       "cpair  == (LAM x y.(x,y))"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3693
diff changeset
    29
cfst_def        "cfst   == (LAM p. fst(p))"
b55686a7b22c fixed dots;
wenzelm
parents: 3693
diff changeset
    30
csnd_def        "csnd   == (LAM p. snd(p))"      
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 4191
diff changeset
    31
csplit_def      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    32
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    33
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    34
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    35
(* introduce syntax for
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    36
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    37
   Let <x,y> = e1; z = E2 in E3
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    38
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    39
   and
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    40
2394
91d8abf108be adaptions for symbol font
oheimb
parents: 2291
diff changeset
    41
   LAM <x,y,z>.e
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    42
*)
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    43
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    44
constdefs
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    45
  CLet           :: "'a -> ('a -> 'b) -> 'b"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 4191
diff changeset
    46
  "CLet == LAM s f. f$s"
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    47
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    48
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    49
(* syntax for Let *)
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    50
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    51
types
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    52
  Cletbinds  Cletbind
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    53
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    54
syntax
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    55
  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    56
  ""        :: "Cletbind => Cletbinds"               ("_")
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    57
  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    58
  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    59
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    60
translations
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    61
  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 4191
diff changeset
    62
  "Let x = a in e"          == "CLet$a$(LAM x. e)"
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    63
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    64
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    65
(* syntax for LAM <x,y,z>.e *)
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    66
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    67
syntax
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    68
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    69
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    70
translations
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 4191
diff changeset
    71
  "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
a7897aebbffc *** empty log message ***
nipkow
parents: 4191
diff changeset
    72
  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
a7897aebbffc *** empty log message ***
nipkow
parents: 4191
diff changeset
    73
  "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
3693
37aa547fb564 fixed LAM <x,y,zs>.b syntax (may break some unusual cases);
wenzelm
parents: 2840
diff changeset
    74
12114
a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents: 12030
diff changeset
    75
syntax (xsymbols)
4191
f967419250d1 fixed LAM<...> syntax;
wenzelm
parents: 3842
diff changeset
    76
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1168
diff changeset
    77
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    78
end