--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/void.ML Wed Jan 19 17:35:01 1994 +0100
@@ -0,0 +1,69 @@
+(* Title: HOLCF/void.ML
+ ID: $Id$
+ Author: Franz Regensburger
+ Copyright 1993 Technische Universitaet Muenchen
+
+Lemmas for void.thy.
+
+These lemmas are prototype lemmas for class porder
+see class theory porder.thy
+*)
+
+open Void;
+
+(* ------------------------------------------------------------------------ *)
+(* A non-emptyness result for Void *)
+(* ------------------------------------------------------------------------ *)
+
+val VoidI = prove_goalw Void.thy [UU_void_Rep_def,Void_def]
+ " UU_void_Rep : Void"
+(fn prems =>
+ [
+ (rtac (mem_Collect_eq RS ssubst) 1),
+ (rtac refl 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* less_void is a partial ordering on void *)
+(* ------------------------------------------------------------------------ *)
+
+val refl_less_void = prove_goalw Void.thy [ less_void_def ] "less_void(x,x)"
+(fn prems =>
+ [
+ (fast_tac HOL_cs 1)
+ ]);
+
+val antisym_less_void = prove_goalw Void.thy [ less_void_def ]
+ "[|less_void(x,y); less_void(y,x)|] ==> x = y"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac (Rep_Void_inverse RS subst) 1),
+ (etac subst 1),
+ (rtac (Rep_Void_inverse RS sym) 1)
+ ]);
+
+val trans_less_void = prove_goalw Void.thy [ less_void_def ]
+ "[|less_void(x,y); less_void(y,z)|] ==> less_void(x,z)"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (fast_tac HOL_cs 1)
+ ]);
+
+(* ------------------------------------------------------------------------ *)
+(* a technical lemma about void: *)
+(* every element in void is represented by UU_void_Rep *)
+(* ------------------------------------------------------------------------ *)
+
+val unique_void = prove_goal Void.thy "Rep_Void(x) = UU_void_Rep"
+(fn prems =>
+ [
+ (rtac (mem_Collect_eq RS subst) 1),
+ (fold_goals_tac [Void_def]),
+ (rtac Rep_Void 1)
+ ]);
+
+
+
+