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;
oheimb@2275
     1
(*  Title:      HOLCF/One.ML
nipkow@243
     2
    ID:         $Id$
slotosch@2640
     3
    Author:     Oscar Slotosch
slotosch@2640
     4
    Copyright   1997 Technische Universitaet Muenchen
nipkow@243
     5
slotosch@2640
     6
Lemmas for One.thy
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open One;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* Exhaustion and Elimination for type one                                  *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
slotosch@2640
    15
qed_goalw "Exh_one" thy [ONE_def] "t=UU | t = ONE"
nipkow@243
    16
 (fn prems =>
clasohm@1461
    17
        [
slotosch@2640
    18
	(lift.induct_tac "t" 1),
slotosch@2640
    19
	(Simp_tac 1),
wenzelm@5087
    20
	(Simp_tac 1)
slotosch@2640
    21
	]);
nipkow@243
    22
slotosch@2640
    23
qed_goal "oneE" thy
slotosch@2640
    24
        "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"
nipkow@243
    25
 (fn prems =>
clasohm@1461
    26
        [
clasohm@1461
    27
        (rtac (Exh_one RS disjE) 1),
clasohm@1461
    28
        (eresolve_tac prems 1),
clasohm@1461
    29
        (eresolve_tac prems 1)
clasohm@1461
    30
        ]);
nipkow@243
    31
slotosch@2640
    32
(* ------------------------------------------------------------------------ *) 
slotosch@2640
    33
(* tactic for one-thms                                                      *)
slotosch@2640
    34
(* ------------------------------------------------------------------------ *)
slotosch@2640
    35
slotosch@2640
    36
fun prover t = prove_goalw thy [ONE_def] t
slotosch@2640
    37
 (fn prems =>
slotosch@2640
    38
        [
wenzelm@4098
    39
	(asm_simp_tac (simpset() addsimps [inst_lift_po]) 1)
slotosch@2640
    40
	]);
slotosch@2640
    41
nipkow@243
    42
(* ------------------------------------------------------------------------ *)
nipkow@243
    43
(* distinctness for type one : stored in a list                             *)
nipkow@243
    44
(* ------------------------------------------------------------------------ *)
nipkow@243
    45
slotosch@2640
    46
val dist_less_one = map prover ["~ONE << UU"];
nipkow@243
    47
slotosch@2640
    48
val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"];
nipkow@243
    49
slotosch@2640
    50
Addsimps (dist_less_one@dist_eq_one);