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