src/HOLCF/tr1.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/tr1.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for tr1.thy
     7 *)
     8 
     9 open Tr1;
    10 
    11 (* -------------------------------------------------------------------------- *) 
    12 (* distinctness for type tr                                                   *) 
    13 (* -------------------------------------------------------------------------- *)
    14 
    15 val dist_less_tr = [
    16 prove_goalw Tr1.thy [TT_def] "~TT << UU"
    17  (fn prems =>
    18 	[
    19 	(rtac classical3 1),
    20 	(rtac defined_sinl 1),
    21 	(rtac not_less2not_eq 1),
    22 	(resolve_tac dist_less_one 1),
    23 	(rtac (rep_tr_iso RS subst) 1),
    24 	(rtac (rep_tr_iso RS subst) 1),
    25 	(rtac cfun_arg_cong 1),
    26 	(rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) 		RS conjunct2 RS ssubst) 1),
    27 	(etac (eq_UU_iff RS ssubst) 1)
    28 	]),
    29 prove_goalw Tr1.thy [FF_def] "~FF << UU"
    30  (fn prems =>
    31 	[
    32 	(rtac classical3 1),
    33 	(rtac defined_sinr 1),
    34 	(rtac not_less2not_eq 1),
    35 	(resolve_tac dist_less_one 1),
    36 	(rtac (rep_tr_iso RS subst) 1),
    37 	(rtac (rep_tr_iso RS subst) 1),
    38 	(rtac cfun_arg_cong 1),
    39 	(rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) 		RS conjunct2 RS ssubst) 1),
    40 	(etac (eq_UU_iff RS ssubst) 1)
    41 	]),
    42 prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF"
    43  (fn prems =>
    44 	[
    45 	(rtac classical3 1),
    46 	(rtac (less_ssum4c RS iffD1) 2),
    47 	(rtac not_less2not_eq 1),
    48 	(resolve_tac dist_less_one 1),
    49 	(rtac (rep_tr_iso RS subst) 1),
    50 	(rtac (rep_tr_iso RS subst) 1),
    51 	(etac monofun_cfun_arg 1)
    52 	]),
    53 prove_goalw Tr1.thy [FF_def,TT_def] "~FF << TT"
    54  (fn prems =>
    55 	[
    56 	(rtac classical3 1),
    57 	(rtac (less_ssum4d RS iffD1) 2),
    58 	(rtac not_less2not_eq 1),
    59 	(resolve_tac dist_less_one 1),
    60 	(rtac (rep_tr_iso RS subst) 1),
    61 	(rtac (rep_tr_iso RS subst) 1),
    62 	(etac monofun_cfun_arg 1)
    63 	])
    64 ];
    65 
    66 fun prover s =  prove_goal Tr1.thy s
    67  (fn prems =>
    68 	[
    69 	(rtac not_less2not_eq 1),
    70 	(resolve_tac dist_less_tr 1)
    71 	]);
    72 
    73 val dist_eq_tr = map prover ["~TT=UU","~FF=UU","~TT=FF"];
    74 val dist_eq_tr = dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr);
    75 
    76 (* ------------------------------------------------------------------------ *) 
    77 (* Exhaustion and elimination for type tr                                   *) 
    78 (* ------------------------------------------------------------------------ *)
    79 
    80 val Exh_tr = prove_goalw Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
    81  (fn prems =>
    82 	[
    83 	(res_inst_tac [("p","rep_tr[t]")] ssumE 1),
    84 	(rtac disjI1 1),
    85 	(rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )
    86 		  RS conjunct2 RS subst) 1),
    87 	(rtac (abs_tr_iso RS subst) 1),
    88 	(etac cfun_arg_cong 1),
    89 	(rtac disjI2 1),
    90 	(rtac disjI1 1),
    91 	(rtac (abs_tr_iso RS subst) 1),
    92 	(rtac cfun_arg_cong 1),
    93 	(etac trans 1),
    94 	(rtac cfun_arg_cong 1),
    95 	(rtac (Exh_one RS disjE) 1),
    96 	(contr_tac 1),
    97 	(atac 1),
    98 	(rtac disjI2 1),
    99 	(rtac disjI2 1),
   100 	(rtac (abs_tr_iso RS subst) 1),
   101 	(rtac cfun_arg_cong 1),
   102 	(etac trans 1),
   103 	(rtac cfun_arg_cong 1),
   104 	(rtac (Exh_one RS disjE) 1),
   105 	(contr_tac 1),
   106 	(atac 1)
   107 	]);
   108 
   109 
   110 val trE = prove_goal Tr1.thy
   111 	"[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
   112  (fn prems =>
   113 	[
   114 	(rtac (Exh_tr RS disjE) 1),
   115 	(eresolve_tac prems 1),
   116 	(etac disjE 1),
   117 	(eresolve_tac prems 1),
   118 	(eresolve_tac prems 1)
   119 	]);
   120 
   121 
   122 (* ------------------------------------------------------------------------ *) 
   123 (* type tr is flat                                                          *) 
   124 (* ------------------------------------------------------------------------ *)
   125 
   126 val prems = goalw Tr1.thy [flat_def] "flat(TT)";
   127 by (rtac allI 1);
   128 by (rtac allI 1);
   129 by (res_inst_tac [("p","x")] trE 1);
   130 by (asm_simp_tac ccc1_ss 1);
   131 by (res_inst_tac [("p","y")] trE 1);
   132 by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
   133 by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
   134 by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
   135 by (res_inst_tac [("p","y")] trE 1);
   136 by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
   137 by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
   138 by (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1);
   139 val flat_tr = result();
   140 
   141 
   142 (* ------------------------------------------------------------------------ *) 
   143 (* properties of tr_when                                                    *) 
   144 (* ------------------------------------------------------------------------ *)
   145 
   146 fun prover s =  prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s
   147  (fn prems =>
   148 	[
   149 	(simp_tac Cfun_ss 1),
   150 	(simp_tac (Ssum_ss addsimps [(rep_tr_iso ),
   151 		(abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) 
   152 		RS iso_strict) RS conjunct1]@dist_eq_one)1)
   153 	]);
   154 
   155 val tr_when = map prover [
   156 			"tr_when[x][y][UU] = UU",
   157 			"tr_when[x][y][TT] = x",
   158 			"tr_when[x][y][FF] = y"
   159 			];
   160 
   161 
   162 
   163 
   164