src/HOLCF/One.ML
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 9248 e1dee89de037
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
     1 (*  Title:      HOLCF/One.ML
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 The unit domain.
     7 *)
     8 
     9 (* ------------------------------------------------------------------------ *)
    10 (* Exhaustion and Elimination for type one                                  *)
    11 (* ------------------------------------------------------------------------ *)
    12 
    13 Goalw [ONE_def] "t=UU | t = ONE";
    14 by (induct_tac "t" 1);
    15 by (Simp_tac 1);
    16 by (Simp_tac 1);
    17 qed "Exh_one";
    18 
    19 val prems = Goal "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q";
    20 by (rtac (Exh_one RS disjE) 1);
    21 by (eresolve_tac prems 1);
    22 by (eresolve_tac prems 1);
    23 qed "oneE";
    24 
    25 (* ------------------------------------------------------------------------ *) 
    26 (* tactic for one-thms                                                      *)
    27 (* ------------------------------------------------------------------------ *)
    28 
    29 fun prover t = prove_goalw thy [ONE_def] t
    30  (fn prems =>
    31         [
    32 	(asm_simp_tac (simpset() addsimps [inst_lift_po]) 1)
    33 	]);
    34 
    35 (* ------------------------------------------------------------------------ *)
    36 (* distinctness for type one : stored in a list                             *)
    37 (* ------------------------------------------------------------------------ *)
    38 
    39 val dist_less_one = map prover ["~ONE << UU"];
    40 
    41 val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"];
    42 
    43 Addsimps (dist_less_one@dist_eq_one);