--- a/src/HOLCF/Tr1.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/HOLCF/Tr1.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/tr1.ML
+(* Title: HOLCF/tr1.ML
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Lemmas for tr1.thy
@@ -15,60 +15,60 @@
val dist_less_tr = [
prove_goalw Tr1.thy [TT_def] "~TT << UU"
(fn prems =>
- [
- (rtac classical3 1),
- (rtac defined_sinl 1),
- (rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
- (etac (eq_UU_iff RS ssubst) 1)
- ]),
+ [
+ (rtac classical3 1),
+ (rtac defined_sinl 1),
+ (rtac not_less2not_eq 1),
+ (resolve_tac dist_less_one 1),
+ (rtac (rep_tr_iso RS subst) 1),
+ (rtac (rep_tr_iso RS subst) 1),
+ (rtac cfun_arg_cong 1),
+ (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
+ (etac (eq_UU_iff RS ssubst) 1)
+ ]),
prove_goalw Tr1.thy [FF_def] "~FF << UU"
(fn prems =>
- [
- (rtac classical3 1),
- (rtac defined_sinr 1),
- (rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
- (etac (eq_UU_iff RS ssubst) 1)
- ]),
+ [
+ (rtac classical3 1),
+ (rtac defined_sinr 1),
+ (rtac not_less2not_eq 1),
+ (resolve_tac dist_less_one 1),
+ (rtac (rep_tr_iso RS subst) 1),
+ (rtac (rep_tr_iso RS subst) 1),
+ (rtac cfun_arg_cong 1),
+ (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
+ (etac (eq_UU_iff RS ssubst) 1)
+ ]),
prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF"
(fn prems =>
- [
- (rtac classical3 1),
- (rtac (less_ssum4c RS iffD1) 2),
- (rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (etac monofun_cfun_arg 1)
- ]),
+ [
+ (rtac classical3 1),
+ (rtac (less_ssum4c RS iffD1) 2),
+ (rtac not_less2not_eq 1),
+ (resolve_tac 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 classical3 1),
- (rtac (less_ssum4d RS iffD1) 2),
- (rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 1),
- (rtac (rep_tr_iso RS subst) 1),
- (rtac (rep_tr_iso RS subst) 1),
- (etac monofun_cfun_arg 1)
- ])
+ [
+ (rtac classical3 1),
+ (rtac (less_ssum4d RS iffD1) 2),
+ (rtac not_less2not_eq 1),
+ (resolve_tac 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)
- ]);
+ [
+ (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);
@@ -79,44 +79,44 @@
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)
- ]);
+ [
+ (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"
+ "[| 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)
- ]);
+ [
+ (rtac (Exh_tr RS disjE) 1),
+ (eresolve_tac prems 1),
+ (etac disjE 1),
+ (eresolve_tac prems 1),
+ (eresolve_tac prems 1)
+ ]);
(* ------------------------------------------------------------------------ *)
@@ -125,20 +125,20 @@
qed_goalw "flat_tr" Tr1.thy [is_flat_def] "is_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)
- ]);
+ [
+ (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)
+ ]);
(* ------------------------------------------------------------------------ *)
@@ -147,16 +147,16 @@
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]@dist_eq_one)1)
- ]);
+ [
+ (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]@dist_eq_one)1)
+ ]);
val tr_when = map prover [
- "tr_when`x`y`UU = UU",
- "tr_when`x`y`TT = x",
- "tr_when`x`y`FF = y"
- ];
+ "tr_when`x`y`UU = UU",
+ "tr_when`x`y`TT = x",
+ "tr_when`x`y`FF = y"
+ ];