isabelle: src/HOLCF/Tr2.thy@efca1e0710fb (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1	(* Title: HOLCF/tr2.thy
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	Author: Franz Regensburger
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	Introduce infix if_then_else_fi and boolean connectives andalso, orelse
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	Tr2 = Tr1 +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	11	consts
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	12	"@cifte" :: "tr=>'c=>'c=>'c"
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	13	("(3If _/ (then _/ else _) fi)" 60)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14	"Icifte" :: "tr->'c->'c->'c"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	16	"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17	"cop @andalso" :: "tr -> tr -> tr" ("trand")
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	18	"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19	"cop @orelse" :: "tr -> tr -> tr" ("tror")
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	20
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	21	"neg" :: "tr -> tr"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22
625 119391dd1d59 New version nipkow parents: 430 diff changeset	23	translations "x andalso y" => "trand[x][y]"
119391dd1d59 New version nipkow parents: 430 diff changeset	24	"x orelse y" => "tror[x][y]"
119391dd1d59 New version nipkow parents: 430 diff changeset	25	"If b then e1 else e2 fi" => "Icifte[b][e1][e2]"
119391dd1d59 New version nipkow parents: 430 diff changeset	26
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27	rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	29	ifte_def "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	30	andalso_def "trand == (LAM t1 t2.tr_when[t2][FF][t1])"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	31	orelse_def "tror == (LAM t1 t2.tr_when[TT][t2][t1])"
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	32	neg_def "neg == (LAM t. tr_when[FF][TT][t])"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	35
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	36
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	37
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	38
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	39

author	lcp
	Mon, 21 Nov 1994 10:51:40 +0100
changeset 718	efca1e0710fb
parent 625	119391dd1d59
child 752	b89462f9d5f1
permissions	-rw-r--r--