src/HOLCF/Tr.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15649 f8345ee4f607
permissions -rw-r--r--
Merged in license change from Isabelle2004
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     1
(*  Title:      HOLCF/Tr.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     2
    ID:         $Id$
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     3
    Author:     Franz Regensburger
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     4
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     5
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     6
*)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     7
3327
9b8e638f8602 Eliminated ccc1. Moved ID,oo into Cfun.
slotosch
parents: 3036
diff changeset
     8
Tr = Lift + Fix +
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
     9
2782
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    10
types
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    11
  tr = "bool lift"
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    12
2766
3e90c5187ce1 "bool lift" now syntax instead of type abbrev;
wenzelm
parents: 2719
diff changeset
    13
translations
2782
5e8771682c73 tr is (again) type abbrev;
wenzelm
parents: 2766
diff changeset
    14
  "tr" <= (type) "bool lift" 
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    15
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    16
consts
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    17
	TT,FF           :: "tr"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    18
        Icifte          :: "tr -> 'c -> 'c -> 'c"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    19
        trand           :: "tr -> tr -> tr"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    20
        tror            :: "tr -> tr -> tr"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    21
        neg             :: "tr -> tr"
3036
5aa3bb94b729 deleted definitions for blift and plift
mueller
parents: 2782
diff changeset
    22
        If2             :: "tr=>'c=>'c=>'c"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    23
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    24
syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    25
        "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    26
        "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    27
 
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    28
translations 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 3842
diff changeset
    29
	     "x andalso y" == "trand$x$y"
a7897aebbffc *** empty log message ***
nipkow
parents: 3842
diff changeset
    30
             "x orelse y"  == "tror$x$y"
a7897aebbffc *** empty log message ***
nipkow
parents: 3842
diff changeset
    31
             "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    32
defs
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    33
  TT_def      "TT==Def True"
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    34
  FF_def      "FF==Def False"
2719
27167b432e7a Renamed constant "not" to "Not"
paulson
parents: 2647
diff changeset
    35
  neg_def     "neg == flift2 Not"
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 3842
diff changeset
    36
  ifte_def    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
3842
b55686a7b22c fixed dots;
wenzelm
parents: 3327
diff changeset
    37
  andalso_def "trand == (LAM x y. If x then y else FF fi)"
b55686a7b22c fixed dots;
wenzelm
parents: 3327
diff changeset
    38
  orelse_def  "tror == (LAM x y. If x then TT else y fi)"
3036
5aa3bb94b729 deleted definitions for blift and plift
mueller
parents: 2782
diff changeset
    39
  If2_def     "If2 Q x y == If Q then x else y fi"
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    40
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    41
end
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents:
diff changeset
    42