src/HOLCF/tr2.ML

eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord

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

Lemmas for tr2.thy
*)

open Tr2;

(* ------------------------------------------------------------------------ *) 
(* lemmas about andalso                                                     *) 
(* ------------------------------------------------------------------------ *)

fun prover s =  prove_goalw Tr2.thy [andalso_def] s
 (fn prems =>
	[
	(simp_tac (ccc1_ss addsimps tr_when) 1)
	]);

val andalso_thms = map prover [
			"TT andalso y = y",
			"FF andalso y = FF",
			"UU andalso y = UU"
			];

val andalso_thms = andalso_thms @ 
 [prove_goalw Tr2.thy [andalso_def] "x andalso TT =  x"
 (fn prems =>
	[
	(res_inst_tac [("p","x")] trE 1),
	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
	])];

(* ------------------------------------------------------------------------ *) 
(* lemmas about orelse                                                      *) 
(* ------------------------------------------------------------------------ *)

fun prover s =  prove_goalw Tr2.thy [orelse_def] s
 (fn prems =>
	[
	(simp_tac (ccc1_ss addsimps tr_when) 1)
	]);

val orelse_thms = map prover [
			"TT orelse y  = TT",
			"FF orelse y =  y",
			"UU orelse y = UU"
			];

val orelse_thms = orelse_thms @ 
 [prove_goalw Tr2.thy [orelse_def] "x orelse FF =  x"
 (fn prems =>
	[
	(res_inst_tac [("p","x")] trE 1),
	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
	(asm_simp_tac (ccc1_ss addsimps tr_when) 1),
	(asm_simp_tac (ccc1_ss addsimps tr_when) 1)
	])];


(* ------------------------------------------------------------------------ *) 
(* lemmas about If_then_else_fi                                             *) 
(* ------------------------------------------------------------------------ *)

fun prover s =  prove_goalw Tr2.thy [ifte_def] s
 (fn prems =>
	[
	(simp_tac (ccc1_ss addsimps tr_when) 1)
	]);

val ifte_thms = map prover [
			"If UU then e1 else e2 fi = UU",
			"If FF then e1 else e2 fi = e2",
			"If TT then e1 else e2 fi = e1"];