--- a/src/LCF/LCF.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/LCF/LCF.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: LCF/lcf.ML
+(* Title: LCF/lcf.ML
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1992 University of Cambridge
For lcf.thy. Basic lemmas about LCF
@@ -53,26 +53,26 @@
fun strip_tac i = REPEAT(rstac [impI,allI] i);
val eq_imp_less1 = prove_goal thy "x=y ==> x << y"
- (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]);
+ (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]);
val eq_imp_less2 = prove_goal thy "x=y ==> y << x"
- (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]);
+ (fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]);
val less_refl = refl RS eq_imp_less1;
val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y"
- (fn prems => [rewrite_goals_tac[eq_def],
- REPEAT(rstac(conjI::prems)1)]);
+ (fn prems => [rewtac eq_def,
+ REPEAT(rstac(conjI::prems)1)]);
val ext = prove_goal thy
- "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
- (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
- prem RS eq_imp_less1,
- prem RS eq_imp_less2]1)]);
+ "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
+ (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
+ prem RS eq_imp_less1,
+ prem RS eq_imp_less2]1)]);
val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)"
- (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
- rtac refl 1]);
+ (fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
+ rtac refl 1]);
val less_ap_term = less_refl RS mono;
val less_ap_thm = less_refl RSN (2,mono);
@@ -80,24 +80,24 @@
val ap_thm = refl RSN (2,cong);
val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU"
- (fn _ => [rtac less_anti_sym 1, rtac minimal 2,
- rtac less_ext 1, rtac allI 1, rtac minimal 1]);
+ (fn _ => [rtac less_anti_sym 1, rtac minimal 2,
+ rtac less_ext 1, rtac allI 1, rtac minimal 1]);
val UU_app = UU_abs RS sym RS ap_thm;
val less_UU = prove_goal thy "x << UU ==> x=UU"
- (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
+ (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b.P(b)"
- (fn prems => [rtac allI 1, rtac mp 1,
- res_inst_tac[("p","b")]tr_cases 2,
- fast_tac (FOL_cs addIs prems) 1]);
+ (fn prems => [rtac allI 1, rtac mp 1,
+ res_inst_tac[("p","b")]tr_cases 2,
+ fast_tac (FOL_cs addIs prems) 1]);
val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)"
- (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
- rstac prems 1, atac 1]);
+ (fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
+ rstac prems 1, atac 1]);
val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos;
val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos;
@@ -112,14 +112,14 @@
val COND_cases_iff = (prove_goal thy
"ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
- (fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,
- not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,
- rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,
- stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec;
+ (fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,
+ not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,
+ rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,
+ stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec;
val lemma = prove_goal thy "A<->B ==> B ==> A"
- (fn prems => [cut_facts_tac prems 1, rewrite_goals_tac [iff_def],
- fast_tac FOL_cs 1]);
+ (fn prems => [cut_facts_tac prems 1, rewtac iff_def,
+ fast_tac FOL_cs 1]);
val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma));