(* Title: HOLCF/tr1.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Introduce the domain of truth values tr = one ++ one
The type is axiomatized as the least solution of a domain equation.
The functor term that specifies the domain equation is:
FT = <++,K_{one},K_{one}>
For details see chapter 5 of:
[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
Dissertation, Technische Universit"at M"unchen, 1994
*)
Tr1 = One +
types tr 0
arities tr :: pcpo
consts
abs_tr :: "one ++ one -> tr"
rep_tr :: "tr -> one ++ one"
TT :: "tr"
FF :: "tr"
tr_when :: "'c -> 'c -> tr -> 'c"
rules
abs_tr_iso "abs_tr[rep_tr[u]] = u"
rep_tr_iso "rep_tr[abs_tr[x]] = x"
TT_def "TT == abs_tr[sinl[one]]"
FF_def "FF == abs_tr[sinr[one]]"
tr_when_def "tr_when == (LAM e1 e2 t.when[LAM x.e1][LAM y.e2][rep_tr[t]])"
end