--- a/src/HOLCF/One.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/One.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
(* Title: HOLCF/One.ML
ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
+ Author: Oscar Slotosch
+ Copyright 1997 Technische Universitaet Muenchen
-Lemmas for One.thy
+Lemmas for One.thy
*)
open One;
@@ -12,24 +12,17 @@
(* Exhaustion and Elimination for type one *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "Exh_one" One.thy [one_def] "z=UU | z = one"
+qed_goalw "Exh_one" thy [ONE_def] "t=UU | t = ONE"
(fn prems =>
[
- (res_inst_tac [("p","rep_one`z")] upE1 1),
- (rtac disjI1 1),
- (rtac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict )
- RS conjunct2 RS subst) 1),
- (rtac (abs_one_iso RS subst) 1),
- (etac cfun_arg_cong 1),
- (rtac disjI2 1),
- (rtac (abs_one_iso RS subst) 1),
- (rtac cfun_arg_cong 1),
- (rtac (unique_void2 RS subst) 1),
- (atac 1)
- ]);
+ (lift.induct_tac "t" 1),
+ (fast_tac HOL_cs 1),
+ (Simp_tac 1),
+ (rtac unit_eq 1)
+ ]);
-qed_goal "oneE" One.thy
- "[| p=UU ==> Q; p = one ==>Q|] ==>Q"
+qed_goal "oneE" thy
+ "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"
(fn prems =>
[
(rtac (Exh_one RS disjE) 1),
@@ -37,53 +30,22 @@
(eresolve_tac prems 1)
]);
+(* ------------------------------------------------------------------------ *)
+(* tactic for one-thms *)
+(* ------------------------------------------------------------------------ *)
+
+fun prover t = prove_goalw thy [ONE_def] t
+ (fn prems =>
+ [
+ (asm_simp_tac (!simpset addsimps [inst_lift_po]) 1)
+ ]);
+
(* ------------------------------------------------------------------------ *)
(* distinctness for type one : stored in a list *)
(* ------------------------------------------------------------------------ *)
-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)]);
-
-qed_goal "dist_eq_one" One.thy "one~=UU" (fn prems => [
- (rtac not_less2not_eq 1),
- (rtac dist_less_one 1)]);
-
-(* ------------------------------------------------------------------------ *)
-(* one is flat *)
-(* ------------------------------------------------------------------------ *)
+val dist_less_one = map prover ["~ONE << UU"];
-qed_goalw "flat_one" One.thy [flat_def] "flat one"
- (fn prems =>
- [
- (rtac allI 1),
- (rtac allI 1),
- (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 1)
- ]);
-
+val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"];
-(* ------------------------------------------------------------------------ *)
-(* properties of one_when *)
-(* here I tried a generic prove procedure *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s = prove_goalw One.thy [one_when_def,one_def] s
- (fn prems =>
- [
- (simp_tac (!simpset addsimps [(rep_one_iso ),
- (abs_one_iso RS allI) RS ((rep_one_iso RS allI)
- RS iso_strict) RS conjunct1] )1)
- ]);
-
-val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
-
-Addsimps (dist_less_one::dist_eq_one::one_when);
+Addsimps (dist_less_one@dist_eq_one);