src/HOLCF/one.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
nipkow@243
     1
(*  Title: 	HOLCF/one.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     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
nipkow@243
    15
val Exh_one = prove_goalw One.thy [one_def] "z=UU | z = one"
nipkow@243
    16
 (fn prems =>
nipkow@243
    17
	[
nipkow@243
    18
	(res_inst_tac [("p","rep_one[z]")] liftE1 1),
nipkow@243
    19
	(rtac disjI1 1),
nipkow@243
    20
	(rtac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict )
nipkow@243
    21
		RS conjunct2 RS subst) 1),
nipkow@243
    22
	(rtac (abs_one_iso RS subst) 1),
nipkow@243
    23
	(etac cfun_arg_cong 1),
nipkow@243
    24
	(rtac disjI2 1),
nipkow@243
    25
	(rtac (abs_one_iso RS subst) 1),
nipkow@243
    26
	(rtac cfun_arg_cong 1),
nipkow@243
    27
	(rtac (unique_void2 RS subst) 1),
nipkow@243
    28
	(atac 1)
nipkow@243
    29
	]);
nipkow@243
    30
nipkow@243
    31
val oneE = prove_goal One.thy
nipkow@243
    32
	"[| p=UU ==> Q; p = one ==>Q|] ==>Q"
nipkow@243
    33
 (fn prems =>
nipkow@243
    34
	[
nipkow@243
    35
	(rtac (Exh_one RS disjE) 1),
nipkow@243
    36
	(eresolve_tac prems 1),
nipkow@243
    37
	(eresolve_tac prems 1)
nipkow@243
    38
	]);
nipkow@243
    39
nipkow@243
    40
(* ------------------------------------------------------------------------ *)
nipkow@243
    41
(* distinctness for type one : stored in a list                             *)
nipkow@243
    42
(* ------------------------------------------------------------------------ *)
nipkow@243
    43
nipkow@243
    44
val dist_less_one = [
nipkow@243
    45
prove_goalw One.thy [one_def] "~one << UU"
nipkow@243
    46
 (fn prems =>
nipkow@243
    47
	[
nipkow@243
    48
	(rtac classical3 1),
nipkow@243
    49
	(rtac less_lift4b 1),
nipkow@243
    50
	(rtac (rep_one_iso RS subst) 1),
nipkow@243
    51
	(rtac (rep_one_iso RS subst) 1),
nipkow@243
    52
	(rtac monofun_cfun_arg 1),
nipkow@243
    53
	(etac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict ) 
nipkow@243
    54
		RS conjunct2 RS ssubst) 1)
nipkow@243
    55
	])
nipkow@243
    56
];
nipkow@243
    57
nipkow@243
    58
val  dist_eq_one = [prove_goal One.thy "~one=UU"
nipkow@243
    59
 (fn prems =>
nipkow@243
    60
	[
nipkow@243
    61
	(rtac not_less2not_eq 1),
nipkow@243
    62
	(resolve_tac dist_less_one 1)
nipkow@243
    63
	])];
nipkow@243
    64
nipkow@243
    65
val dist_eq_one = dist_eq_one @ (map (fn thm => (thm RS not_sym)) dist_eq_one);
nipkow@243
    66
nipkow@243
    67
(* ------------------------------------------------------------------------ *)
nipkow@243
    68
(* one is flat                                                              *)
nipkow@243
    69
(* ------------------------------------------------------------------------ *)
nipkow@243
    70
nipkow@243
    71
val prems = goalw One.thy [flat_def] "flat(one)";
nipkow@243
    72
by (rtac allI 1);
nipkow@243
    73
by (rtac allI 1);
nipkow@243
    74
by (res_inst_tac [("p","x")] oneE 1);
nipkow@243
    75
by (asm_simp_tac ccc1_ss  1);
nipkow@243
    76
by (res_inst_tac [("p","y")] oneE 1);
nipkow@243
    77
by (asm_simp_tac (ccc1_ss addsimps dist_less_one) 1);
nipkow@243
    78
by (asm_simp_tac ccc1_ss  1);
nipkow@243
    79
val flat_one = result();
nipkow@243
    80
nipkow@243
    81
nipkow@243
    82
(* ------------------------------------------------------------------------ *)
nipkow@243
    83
(* properties of one_when                                                   *)
nipkow@243
    84
(* here I tried a generic prove procedure                                   *)
nipkow@243
    85
(* ------------------------------------------------------------------------ *)
nipkow@243
    86
nipkow@243
    87
fun prover s =  prove_goalw One.thy [one_when_def,one_def] s
nipkow@243
    88
 (fn prems =>
nipkow@243
    89
	[
nipkow@243
    90
	(simp_tac (ccc1_ss addsimps [(rep_one_iso ),
nipkow@243
    91
	(abs_one_iso RS allI) RS ((rep_one_iso RS allI) 
nipkow@243
    92
	RS iso_strict) RS conjunct1] )1)
nipkow@243
    93
	]);
nipkow@243
    94
nipkow@243
    95
val one_when = map prover ["one_when[x][UU] = UU","one_when[x][one] = x"];
nipkow@243
    96