src/HOLCF/tr1.thy

quick_and_dirty_prove_goalw_cterm;

(*  Title: 	HOLCF/tr1.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

Introduve the domain of truth values tr = {UU,TT,FF}

This type is introduced using a domain isomorphism.

The type axiom 

	arities tr :: pcpo

and the continuity of the Isomorphisms are taken for granted. Since the
type is not recursive, it could be easily introduced in a purely conservative
style as it was used for the types sprod, ssum, lift. The definition of the 
ordering is canonical using abstraction and representation, but this would take
again a lot of internal constants. It can be easily seen that the axioms below
are consistent.

Partial Ordering is implicit in isomorphims abs_tr,rep_tr and their continuity

*)

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