isabelle: src/HOLCF/Tr2.thy@d0dc8d057929 (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
752 b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	12	Icifte :: "tr -> 'c -> 'c -> 'c"
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	13	trand :: "tr -> tr -> tr"
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	14	tror :: "tr -> tr -> tr"
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	15	neg :: "tr -> tr"
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	16
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	17	syntax "@cifte" :: "tr=>'c=>'c=>'c"
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	18	("(3If _/ (then _/ else _) fi)" 60)
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	19	"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	20	"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
752 b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	21
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	22	translations "x andalso y" == "trand[x][y]"
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	23	"x orelse y" == "tror[x][y]"
b89462f9d5f1 ---------------------------------------------------------------------- regensbu parents: 625 diff changeset	24	"If b then e1 else e2 fi" == "Icifte[b][e1][e2]"
625 119391dd1d59 New version nipkow parents: 430 diff changeset	25
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	26	rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	27
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	28	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	29	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	30	orelse_def "tror == (LAM t1 t2.tr_when[TT][t2][t1])"
430 89e1986125fe Franz Regensburger's changes. nipkow parents: 243 diff changeset	31	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	32
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	33	end
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	34
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

author	clasohm
	Tue, 07 Feb 1995 11:59:32 +0100
changeset 892	d0dc8d057929
parent 752	b89462f9d5f1
child 1168	74be52691d62
permissions	-rw-r--r--