isabelle: src/HOLCF/tr1.ML@645f46a24c72

     1 (*  Title: 	HOLCF/tr1.ML

     2     ID:         $Id$

     3     Author: 	Franz Regensburger

     4     Copyright   1993 Technische Universitaet Muenchen

     6 Lemmas for tr1.thy

     7 *)

     9 open Tr1;

    11 (* -------------------------------------------------------------------------- *)

    12 (* distinctness for type tr                                                   *)

    13 (* -------------------------------------------------------------------------- *)

    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 ];

    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 	]);

    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);

    76 (* ------------------------------------------------------------------------ *)

    77 (* Exhaustion and elimination for type tr                                   *)

    78 (* ------------------------------------------------------------------------ *)

    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 	]);

   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 	]);

   122 (* ------------------------------------------------------------------------ *)

   123 (* type tr is flat                                                          *)

   124 (* ------------------------------------------------------------------------ *)

   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();

   142 (* ------------------------------------------------------------------------ *)

   143 (* properties of tr_when                                                    *)

   144 (* ------------------------------------------------------------------------ *)

   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 	]);

   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 			];

author	wenzelm
	Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400	645f46a24c72
parent 243	c22b85994e17
permissions	-rw-r--r--