--- a/src/HOLCF/Tr1.ML Sat Feb 15 18:24:05 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,159 +0,0 @@
-(* Title: HOLCF/tr1.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for tr1.thy
-*)
-
-open Tr1;
-
-(* -------------------------------------------------------------------------- *)
-(* distinctness for type tr *)
-(* -------------------------------------------------------------------------- *)
-
-val dist_less_tr = [
-prove_goalw Tr1.thy [TT_def] "~TT << UU"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac defined_sinl 1),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
- (etac (eq_UU_iff RS ssubst) 1)
- ]),
-prove_goalw Tr1.thy [FF_def] "~FF << UU"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac defined_sinr 1),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
- (etac (eq_UU_iff RS ssubst) 1)
- ]),
-prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac (less_ssum4c RS iffD1) 2),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (etac monofun_cfun_arg 1)
- ]),
-prove_goalw Tr1.thy [FF_def,TT_def] "~FF << TT"
- (fn prems =>
- [
- (rtac classical2 1),
- (rtac (less_ssum4d RS iffD1) 2),
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (etac monofun_cfun_arg 1)
- ])
-];
-
-fun prover s = prove_goal Tr1.thy s
- (fn prems =>
- [
- (rtac not_less2not_eq 1),
- (resolve_tac dist_less_tr 1)
- ]);
-
-val dist_eq_tr = map prover ["TT~=UU","FF~=UU","TT~=FF"];
-val dist_eq_tr = dist_eq_tr @ (map (fn thm => (thm RS not_sym)) dist_eq_tr);
-
-(* ------------------------------------------------------------------------ *)
-(* Exhaustion and elimination for type tr *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "Exh_tr" Tr1.thy [FF_def,TT_def] "t=UU | t = TT | t = FF"
- (fn prems =>
- [
- (res_inst_tac [("p","rep_tr`t")] ssumE 1),
- (rtac disjI1 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )
- RS conjunct2 RS subst) 1),
- (rtac (abs_tr_iso RS subst) 1),
- (etac cfun_arg_cong 1),
- (rtac disjI2 1),
- (rtac disjI1 1),
- (rtac (abs_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (etac trans 1),
- (rtac cfun_arg_cong 1),
- (rtac (Exh_one RS disjE) 1),
- (contr_tac 1),
- (atac 1),
- (rtac disjI2 1),
- (rtac disjI2 1),
- (rtac (abs_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (etac trans 1),
- (rtac cfun_arg_cong 1),
- (rtac (Exh_one RS disjE) 1),
- (contr_tac 1),
- (atac 1)
- ]);
-
-
-qed_goal "trE" Tr1.thy
- "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
- (fn prems =>
- [
- (rtac (Exh_tr RS disjE) 1),
- (eresolve_tac prems 1),
- (etac disjE 1),
- (eresolve_tac prems 1),
- (eresolve_tac prems 1)
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* type tr is flat *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goalw "flat_tr" Tr1.thy [flat_def] "flat TT"
- (fn prems =>
- [
- (rtac allI 1),
- (rtac allI 1),
- (res_inst_tac [("p","x")] trE 1),
- (Asm_simp_tac 1),
- (res_inst_tac [("p","y")] trE 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (res_inst_tac [("p","y")] trE 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
- (asm_simp_tac (!simpset addsimps dist_less_tr) 1)
- ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* properties of tr_when *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s (fn prems => [
- (Simp_tac 1),
- (simp_tac (!simpset addsimps [rep_tr_iso,
- (abs_tr_iso RS allI) RS ((rep_tr_iso RS allI)
- RS iso_strict) RS conjunct1]) 1)]);
-
-val tr_when = map prover [
- "tr_when`x`y`UU = UU",
- "tr_when`x`y`TT = x",
- "tr_when`x`y`FF = y"
- ];
-