src/HOLCF/One.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5087 ee8a754f1981
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/One.ML
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 Lemmas for One.thy
     7 *)
     8 
     9 open One;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* Exhaustion and Elimination for type one                                  *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "Exh_one" thy [ONE_def] "t=UU | t = ONE"
    16  (fn prems =>
    17         [
    18 	(lift.induct_tac "t" 1),
    19 	(Simp_tac 1),
    20 	(Simp_tac 1)
    21 	]);
    22 
    23 qed_goal "oneE" thy
    24         "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"
    25  (fn prems =>
    26         [
    27         (rtac (Exh_one RS disjE) 1),
    28         (eresolve_tac prems 1),
    29         (eresolve_tac prems 1)
    30         ]);
    31 
    32 (* ------------------------------------------------------------------------ *) 
    33 (* tactic for one-thms                                                      *)
    34 (* ------------------------------------------------------------------------ *)
    35 
    36 fun prover t = prove_goalw thy [ONE_def] t
    37  (fn prems =>
    38         [
    39 	(asm_simp_tac (simpset() addsimps [inst_lift_po]) 1)
    40 	]);
    41 
    42 (* ------------------------------------------------------------------------ *)
    43 (* distinctness for type one : stored in a list                             *)
    44 (* ------------------------------------------------------------------------ *)
    45 
    46 val dist_less_one = map prover ["~ONE << UU"];
    47 
    48 val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"];
    49 
    50 Addsimps (dist_less_one@dist_eq_one);