src/HOLCF/void.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     1 (*  Title: 	HOLCF/void.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for void.thy.
     7 
     8 These lemmas are prototype lemmas for class porder 
     9 see class theory porder.thy
    10 *)
    11 
    12 open Void;
    13 
    14 (* ------------------------------------------------------------------------ *)
    15 (* A non-emptyness result for Void                                          *)
    16 (* ------------------------------------------------------------------------ *)
    17 
    18 val VoidI = prove_goalw Void.thy [UU_void_Rep_def,Void_def] 
    19  " UU_void_Rep : Void"
    20 (fn prems =>
    21 	[
    22 	(rtac (mem_Collect_eq RS ssubst) 1),
    23 	(rtac refl 1)
    24 	]);
    25 
    26 (* ------------------------------------------------------------------------ *)
    27 (* less_void is a partial ordering on void                                  *)
    28 (* ------------------------------------------------------------------------ *)
    29 
    30 val refl_less_void = prove_goalw Void.thy [ less_void_def ] "less_void(x,x)"
    31 (fn prems =>
    32 	[
    33 	(fast_tac HOL_cs 1)
    34 	]);
    35 
    36 val antisym_less_void = prove_goalw Void.thy [ less_void_def ] 
    37 	"[|less_void(x,y); less_void(y,x)|] ==> x = y"
    38 (fn prems =>
    39 	[
    40 	(cut_facts_tac prems 1),
    41 	(rtac (Rep_Void_inverse RS subst) 1),
    42 	(etac subst 1),
    43 	(rtac (Rep_Void_inverse RS sym) 1)
    44 	]);
    45 
    46 val trans_less_void = prove_goalw Void.thy [ less_void_def ] 
    47 	"[|less_void(x,y); less_void(y,z)|] ==> less_void(x,z)"
    48 (fn prems =>
    49 	[
    50 	(cut_facts_tac prems 1),
    51 	(fast_tac HOL_cs 1)
    52 	]);
    53 
    54 (* ------------------------------------------------------------------------ *)
    55 (* a technical lemma about void:                                            *)
    56 (* every element in void is represented by UU_void_Rep                      *)
    57 (* ------------------------------------------------------------------------ *)
    58 
    59 val unique_void = prove_goal Void.thy "Rep_Void(x) = UU_void_Rep"
    60 (fn prems =>
    61 	[
    62 	(rtac (mem_Collect_eq RS subst) 1), 
    63 	(fold_goals_tac [Void_def]),
    64 	(rtac Rep_Void 1)
    65 	]);
    66 
    67 	
    68 
    69