src/HOLCF/Void.ML

reflecting my recent changes of the classical reasoner

(*  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                                          *)
(* ------------------------------------------------------------------------ *)

qed_goalw "VoidI" Void.thy [UU_void_Rep_def,Void_def] 
 " UU_void_Rep : Void"
(fn prems =>
        [
        (stac mem_Collect_eq 1),
        (rtac refl 1)
        ]);

(* ------------------------------------------------------------------------ *)
(* less_void is a partial ordering on void                                  *)
(* ------------------------------------------------------------------------ *)

qed_goalw "refl_less_void" Void.thy [ less_void_def ] "less_void x x"
(fn prems =>
        [
        (fast_tac HOL_cs 1)
        ]);

qed_goalw "antisym_less_void" 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)
        ]);

qed_goalw "trans_less_void" 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                      *)
(* ------------------------------------------------------------------------ *)

qed_goal "unique_void" 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)
        ]);