converted dist_less_one and dist_eq_one to single theorems instead of thm lists
re-added lost Addsimps (dist_less_one::dist_eq_one::one_when);
--- a/src/HOLCF/One.ML Thu Dec 19 11:58:39 1996 +0100
+++ b/src/HOLCF/One.ML Thu Dec 19 17:01:47 1996 +0100
@@ -3,7 +3,7 @@
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for one.thy
+Lemmas for One.thy
*)
open One;
@@ -41,28 +41,18 @@
(* distinctness for type one : stored in a list *)
(* ------------------------------------------------------------------------ *)
-val dist_less_one = [
-prove_goalw One.thy [one_def] "~one << UU"
- (fn prems =>
- [
+qed_goalw "dist_less_one" One.thy [one_def] "~one << UU" (fn prems => [
(rtac classical2 1),
(rtac less_up4b 1),
(rtac (rep_one_iso RS subst) 1),
(rtac (rep_one_iso RS subst) 1),
(rtac monofun_cfun_arg 1),
(etac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict )
- RS conjunct2 RS ssubst) 1)
- ])
-];
+ RS conjunct2 RS ssubst) 1)]);
-val dist_eq_one = [prove_goal One.thy "one~=UU"
- (fn prems =>
- [
+qed_goal "dist_eq_one" One.thy "one~=UU" (fn prems => [
(rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 1)
- ])];
-
-val dist_eq_one = dist_eq_one @ (map (fn thm => (thm RS not_sym)) dist_eq_one);
+ (rtac dist_less_one 1)]);
(* ------------------------------------------------------------------------ *)
(* one is flat *)
@@ -76,7 +66,7 @@
(res_inst_tac [("p","x")] oneE 1),
(Asm_simp_tac 1),
(res_inst_tac [("p","y")] oneE 1),
- (asm_simp_tac (!simpset addsimps dist_less_one) 1),
+ (asm_simp_tac (!simpset addsimps [dist_less_one]) 1),
(Asm_simp_tac 1)
]);
@@ -96,3 +86,4 @@
val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
+Addsimps (dist_less_one::dist_eq_one::one_when);
--- a/src/HOLCF/Tr1.ML Thu Dec 19 11:58:39 1996 +0100
+++ b/src/HOLCF/Tr1.ML Thu Dec 19 17:01:47 1996 +0100
@@ -19,7 +19,7 @@
(rtac classical2 1),
(rtac defined_sinl 1),
(rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 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),
@@ -32,7 +32,7 @@
(rtac classical2 1),
(rtac defined_sinr 1),
(rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 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),
@@ -45,7 +45,7 @@
(rtac classical2 1),
(rtac (less_ssum4c RS iffD1) 2),
(rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 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)
@@ -56,7 +56,7 @@
(rtac classical2 1),
(rtac (less_ssum4d RS iffD1) 2),
(rtac not_less2not_eq 1),
- (resolve_tac dist_less_one 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)
@@ -145,14 +145,11 @@
(* properties of tr_when *)
(* ------------------------------------------------------------------------ *)
-fun prover s = prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s
- (fn prems =>
- [
+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 ),
+ (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)
- ]);
+ RS iso_strict) RS conjunct1]) 1)]);
val tr_when = map prover [
"tr_when`x`y`UU = UU",