Eliminated the prediates flat,chfin
Changed theorems with flat(x::'a) to (x::'a::flat)
Since flat<chfin theorems adm_flat,adm_flatdom are eliminated.
Use adm_chain_finite and adm_chfindom instead!
Examples do not use flat_flat any more
--- a/src/HOLCF/Fix.ML Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Fix.ML Sun May 25 16:17:09 1997 +0200
@@ -550,114 +550,71 @@
(etac spec 1)
]);
-qed_goalw "adm_chain_finite" thy [chain_finite_def]
- "chain_finite(x::'a) ==> adm(P::'a=>bool)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac adm_max_in_chain 1)
- ]);
+bind_thm ("adm_chain_finite" ,chfin RS adm_max_in_chain);
(* ------------------------------------------------------------------------ *)
(* flat types are chain_finite *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_imp_chain_finite" thy [flat_def,chain_finite_def]
- "flat(x::'a)==>chain_finite(x::'a)"
- (fn prems =>
+qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
+ "!Y::nat=>'a::flat.is_chain Y-->(? n.max_in_chain n Y)"
+ (fn _ =>
[
- (rewtac max_in_chain_def),
- (cut_facts_tac prems 1),
(strip_tac 1),
(case_tac "!i.Y(i)=UU" 1),
(res_inst_tac [("x","0")] exI 1),
- (strip_tac 1),
- (rtac trans 1),
- (etac spec 1),
- (rtac sym 1),
- (etac spec 1),
- (rtac (chain_mono2 RS exE) 1),
- (fast_tac HOL_cs 1),
- (atac 1),
- (res_inst_tac [("x","Suc(x)")] exI 1),
+ (Asm_simp_tac 1),
+ (Asm_full_simp_tac 1),
+ (etac exE 1),
+ (res_inst_tac [("x","i")] exI 1),
(strip_tac 1),
- (rtac disjE 1),
- (atac 3),
- (rtac mp 1),
- (dtac spec 1),
- (etac spec 1),
+ (dres_inst_tac [("x","i"),("y","j")] chain_mono 1),
(etac (le_imp_less_or_eq RS disjE) 1),
- (etac (chain_mono RS mp) 1),
- (atac 1),
- (hyp_subst_tac 1),
- (rtac refl_less 1),
- (res_inst_tac [("P","Y(Suc(x)) = UU")] notE 1),
- (atac 2),
- (rtac mp 1),
- (etac spec 1),
- (Asm_simp_tac 1)
+ (safe_tac HOL_cs),
+ (dtac (ax_flat RS spec RS spec RS mp) 1),
+ (fast_tac HOL_cs 1)
]);
-
-bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite);
-(* flat(?x::?'a) ==> adm(?P::?'a => bool) *)
+(* flat subclass of chfin --> adm_flat not needed *)
(* ------------------------------------------------------------------------ *)
(* some properties of flat *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flatI" thy [flat_def] "!x y::'a.x<<y-->x=UU|x=y==>flat(x::'a)"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "flatE" thy [flat_def] "flat(x::'a)==>!x y::'a.x<<y-->x=UU|x=y"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "flat_flat" thy [flat_def] "flat(x::'a::flat)"
-(fn prems => [rtac ax_flat 1]);
-
-qed_goalw "flatdom2monofun" thy [flat_def]
- "[| flat(x::'a::pcpo); f UU = UU |] ==> monofun (f::'a=>'b::pcpo)"
+qed_goalw "flatdom2monofun" thy [monofun]
+ "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)"
(fn prems =>
[
cut_facts_tac prems 1,
- fast_tac ((HOL_cs addss !simpset) addSIs [monofunI]) 1
+ strip_tac 1,
+ dtac (ax_flat RS spec RS spec RS mp) 1,
+ fast_tac ((HOL_cs addss !simpset)) 1
]);
-
-qed_goalw "flat_eq" thy [flat_def]
- "[| flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
- (cut_facts_tac prems 1),
- (fast_tac (HOL_cs addIs [refl_less]) 1)]);
+qed_goal "flat_eq" thy "(a::'a::flat) ~= UU ==> a << b = (a = b)"
+(fn prems=>
+ [
+ cut_facts_tac prems 1,
+ safe_tac (HOL_cs addSIs [refl_less]),
+ dtac (ax_flat RS spec RS spec RS mp) 1,
+ fast_tac (HOL_cs addSIs [refl_less,ax_flat RS spec RS spec RS mp]) 1
+ ]);
(* ------------------------------------------------------------------------ *)
(* some lemmata for functions with flat/chain_finite domain/range types *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chfinI" thy [chain_finite_def]
- "!Y::nat=>'a.is_chain Y-->(? n.max_in_chain n Y)==>chain_finite(x::'a)"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "chfinE" Fix.thy [chain_finite_def]
- "chain_finite(x::'a)==>!Y::nat=>'a.is_chain Y-->(? n.max_in_chain n Y)"
-(fn prems => [rtac (hd(prems)) 1]);
-
-qed_goalw "chfin_chfin" thy [chain_finite_def] "chain_finite(x::'a::chfin)"
-(fn prems => [rtac ax_chfin 1]);
-
qed_goal "chfin2finch" thy
- "[| is_chain (Y::nat=>'a); chain_finite(x::'a) |] ==> finite_chain Y"
-(fn prems =>
+ "is_chain (Y::nat=>'a::chfin) ==> finite_chain Y"
+ (fn prems =>
[
cut_facts_tac prems 1,
fast_tac (HOL_cs addss
- (!simpset addsimps [chain_finite_def,finite_chain_def])) 1
+ (!simpset addsimps [chfin,finite_chain_def])) 1
]);
-bind_thm("flat_subclass_chfin",flat_flat RS flat_imp_chain_finite RS chfinE);
-
-qed_goal "chfindom_monofun2cont" thy
- "[| chain_finite(x::'a::pcpo); monofun f |] ==> cont (f::'a=>'b::pcpo)"
+qed_goal "chfindom_monofun2cont" thy "monofun f ==> cont(f::'a::chfin=>'b::pcpo)"
(fn prems =>
[
cut_facts_tac prems 1,
@@ -665,55 +622,42 @@
atac 1,
rtac contlubI 1,
strip_tac 1,
- dtac (chfin2finch COMP swap_prems_rl) 1,
- atac 1,
+ forward_tac [chfin2finch] 1,
rtac antisym_less 1,
fast_tac ((HOL_cs addIs [is_ub_thelub,ch2ch_monofun])
addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1,
dtac (monofun_finch2finch COMP swap_prems_rl) 1,
atac 1,
- fast_tac ((HOL_cs
- addIs [is_ub_thelub,(monofunE RS spec RS spec RS mp)])
- addss (HOL_ss addsimps [finite_chain_def,maxinch_is_thelub])) 1
+ asm_full_simp_tac (HOL_ss addsimps [finite_chain_def]) 1,
+ etac conjE 1, etac exE 1,
+ asm_full_simp_tac (HOL_ss addsimps [maxinch_is_thelub]) 1,
+ etac (monofunE RS spec RS spec RS mp) 1,
+ etac is_ub_thelub 1
]);
-bind_thm("flatdom_monofun2cont",flat_imp_chain_finite RS chfindom_monofun2cont);
-(* [| flat ?x; monofun ?f |] ==> cont ?f *)
-qed_goal "flatdom_strict2cont" thy
- "[| flat(x::'a::pcpo); f UU = UU |] ==> cont (f::'a=>'b::pcpo)"
-(fn prems =>
- [
- cut_facts_tac prems 1,
- fast_tac ((HOL_cs addSIs [flatdom2monofun,
- flat_imp_chain_finite RS chfindom_monofun2cont])) 1
- ]);
+bind_thm ("flatdom_strict2cont",flatdom2monofun RS chfindom_monofun2cont);
+(* f UU = UU ==> cont (f::'a=>'b::pcpo)" *)
qed_goal "chfin_fappR" thy
- "[| is_chain (Y::nat => 'a::cpo->'b); chain_finite(x::'b) |] ==> \
-\ !s. ? n. lub(range(Y))`s = Y n`s"
+ "is_chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s"
(fn prems =>
[
cut_facts_tac prems 1,
rtac allI 1,
rtac (contlub_cfun_fun RS ssubst) 1,
atac 1,
- fast_tac (HOL_cs addSIs [thelubI,lub_finch2,chfin2finch,ch2ch_fappL])1
+ fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
]);
-qed_goalw "adm_chfindom" thy [adm_def]
- "chain_finite (x::'b) ==> adm (%(u::'a::cpo->'b). P(u`s))"
- (fn prems => [
- cut_facts_tac prems 1,
+qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
+ (fn _ => [
strip_tac 1,
dtac chfin_fappR 1,
- atac 1,
eres_inst_tac [("x","s")] allE 1,
- fast_tac (HOL_cs addss !simpset) 1]);
+ fast_tac (HOL_cs addss (!simpset addsimps [chfin])) 1]);
-bind_thm("adm_flatdom",flat_imp_chain_finite RS adm_chfindom);
-(* flat ?x ==> adm (%u. ?P (u`?s)) *)
-
+(* adm_flat not needed any more, since it is a special case of adm_chfindom *)
(* ------------------------------------------------------------------------ *)
(* lemmata for improved admissibility introdution rule *)
@@ -809,9 +753,9 @@
(* propagation of flatness and chainfiniteness by continuous isomorphisms *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chfin2chfin" thy [chain_finite_def]
-"!!f g.[|chain_finite(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
-\ ==> chain_finite(y::'b)"
+qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. is_chain Y --> (? n. max_in_chain n Y); \
+\ !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a::chfin) |] \
+\ ==> ! Y::nat=>'b. is_chain Y --> (? n. max_in_chain n Y)"
(fn prems =>
[
(rewtac max_in_chain_def),
@@ -832,9 +776,9 @@
(atac 1)
]);
-qed_goalw "flat2flat" thy [flat_def]
-"!!f g.[|flat(x::'a); !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
-\ ==> flat(y::'b)"
+
+qed_goal "flat2flat" thy "!!f g.[|!x y::'a.x<<y --> x=UU | x=y; \
+\ !y.f`(g`y)=(y::'b); !x.g`(f`x)=(x::'a)|] ==> !x y::'b.x<<y --> x=UU | x=y"
(fn prems =>
[
(strip_tac 1),
@@ -863,8 +807,8 @@
(* a result about functions with flat codomain *)
(* ------------------------------------------------------------------------- *)
-qed_goalw "flat_codom" thy [flat_def]
-"[|flat(y::'b);f`(x::'a)=(c::'b)|] ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
+qed_goal "flat_codom" thy
+"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -878,23 +822,15 @@
(etac disjI1 1),
(rtac disjI2 1),
(rtac allI 1),
- (res_inst_tac [("s","f`x"),("t","c")] subst 1),
- (atac 1),
+ (hyp_subst_tac 1),
(res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1),
- (etac allE 1),(etac allE 1),
- (dtac mp 1),
- (res_inst_tac [("fo","f")] (minimal RS monofun_cfun_arg) 1),
- (etac disjE 1),
- (contr_tac 1),
- (atac 1),
- (etac allE 1),
- (etac allE 1),
- (dtac mp 1),
- (res_inst_tac [("fo","f")] (minimal RS monofun_cfun_arg) 1),
- (etac disjE 1),
- (contr_tac 1),
- (atac 1)
- ]);
+ (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS
+ (ax_flat RS spec RS spec RS mp) RS disjE) 1),
+ (contr_tac 1),(atac 1),
+ (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS
+ (ax_flat RS spec RS spec RS mp) RS disjE) 1),
+ (contr_tac 1),(atac 1)
+]);
(* ------------------------------------------------------------------------ *)
(* admissibility of special formulae and propagation *)
--- a/src/HOLCF/Fix.thy Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Fix.thy Sun May 25 16:17:09 1997 +0200
@@ -17,8 +17,6 @@
fix :: "('a->'a)->'a"
adm :: "('a::cpo=>bool)=>bool"
admw :: "('a=>bool)=>bool"
-chain_finite :: "'a::cpo=>bool"
-flat :: "'a=>bool"
defs
@@ -32,16 +30,11 @@
admw_def "admw P == !F. (!n.P (iterate n F UU)) -->
P (lub(range (%i. iterate i F UU)))"
-chain_finite_def "chain_finite (x::'a::cpo)==
- !Y. is_chain (Y::nat=>'a::cpo) --> (? n.max_in_chain n Y)"
-
-flat_def "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"
-
(* further useful class for HOLCF *)
axclass chfin<pcpo
-ax_chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
+chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)"
axclass flat<pcpo
--- a/src/HOLCF/IMP/Denotational.ML Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.ML Sun May 25 16:17:09 1997 +0200
@@ -37,7 +37,7 @@
by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
by (Simp_tac 1);
br fix_ind 1;
- by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_flatdom,flat_lift])) 1);
+ by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,flat_lift])) 1);
by (Simp_tac 1);
by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
by (safe_tac HOL_cs);
--- a/src/HOLCF/IsaMakefile Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/IsaMakefile Sun May 25 16:17:09 1997 +0200
@@ -17,9 +17,9 @@
Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
One.thy Tr.thy\
Discrete0.thy Discrete1.thy Discrete.thy\
- Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
+ Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
-ONLYTHYS = Lift.thy
+ONLYTHYS =
FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Lift.ML Sun May 25 16:17:09 1997 +0200
@@ -0,0 +1,100 @@
+open Lift;
+
+(* ---------------------------------------------------------- *)
+ section"Continuity Proofs for flift1, flift2, if";
+(* need the instance into flat *)
+(* ---------------------------------------------------------- *)
+
+
+(* flift1 is continuous in its argument itself*)
+goal thy "cont (lift_case UU f)";
+br flatdom_strict2cont 1;
+by (Simp_tac 1);
+qed"cont_flift1_arg";
+
+(* flift1 is continuous in a variable that occurs only
+ in the Def branch *)
+
+goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
+\ cont (%y. lift_case UU (f y))";
+br cont2cont_CF1L_rev 1;
+by (strip_tac 1);
+by (res_inst_tac [("x","y")] Lift_cases 1);
+by (Asm_simp_tac 1);
+by (fast_tac (HOL_cs addss !simpset) 1);
+qed"cont_flift1_not_arg";
+
+(* flift1 is continuous in a variable that occurs either
+ in the Def branch or in the argument *)
+
+goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
+\ cont (%y. lift_case UU (f y) (g y))";
+br cont2cont_app 1;
+back();
+by (safe_tac set_cs);
+br cont_flift1_not_arg 1;
+auto();
+br cont_flift1_arg 1;
+qed"cont_flift1_arg_and_not_arg";
+
+(* flift2 is continuous in its argument itself *)
+
+goal thy "cont (lift_case UU (%y. Def (f y)))";
+br flatdom_strict2cont 1;
+by (Simp_tac 1);
+qed"cont_flift2_arg";
+
+
+(* ---------------------------------------------------------- *)
+(* Extension of cont_tac and installation of simplifier *)
+(* ---------------------------------------------------------- *)
+
+bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev);
+
+val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
+ cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2,
+ cont_fapp_app,cont_fapp_app_app,cont_if];
+
+val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext;
+
+Addsimps cont_lemmas_ext;
+
+fun cont_tac i = resolve_tac cont_lemmas2 i;
+fun cont_tacR i = REPEAT (cont_tac i);
+
+fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
+ REPEAT (cont_tac i);
+
+
+simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
+
+(* ---------------------------------------------------------- *)
+ section"flift1, flift2";
+(* ---------------------------------------------------------- *)
+
+
+goal thy "flift1 f`(Def x) = (f x)";
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"flift1_Def";
+
+goal thy "flift2 f`(Def x) = Def (f x)";
+by (simp_tac (!simpset addsimps [flift2_def]) 1);
+qed"flift2_Def";
+
+goal thy "flift1 f`UU = UU";
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"flift1_UU";
+
+goal thy "flift2 f`UU = UU";
+by (simp_tac (!simpset addsimps [flift2_def]) 1);
+qed"flift2_UU";
+
+Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
+
+goal thy "!!x. x~=UU ==> (flift2 f)`x~=UU";
+by (def_tac 1);
+qed"flift2_nUU";
+
+Addsimps [flift2_nUU];
+
+
--- a/src/HOLCF/Lift3.ML Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Lift3.ML Sun May 25 16:17:09 1997 +0200
@@ -139,58 +139,9 @@
section"Lift is flat";
(* ---------------------------------------------------------- *)
-goalw thy [flat_def] "flat (x::'a lift)";
+goal thy "! x y::'a lift. x << y --> x = UU | x = y";
by (simp_tac (!simpset addsimps [less_lift]) 1);
-qed"flat_lift";
-
-bind_thm("ax_flat_lift",flat_lift RS flatE);
-
-
-(* ---------------------------------------------------------- *)
- section"Continuity Proofs for flift1, flift2, if";
-(* ---------------------------------------------------------- *)
-
-
-(* flift1 is continuous in its argument itself*)
-
-goal thy "cont (lift_case UU f)";
-br flatdom_strict2cont 1;
-br flat_lift 1;
-by (Simp_tac 1);
-qed"cont_flift1_arg";
-
-(* flift1 is continuous in a variable that occurs only
- in the Def branch *)
-
-goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
-\ cont (%y. lift_case UU (f y))";
-br cont2cont_CF1L_rev 1;
-by (strip_tac 1);
-by (res_inst_tac [("x","y")] Lift_cases 1);
-by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addss !simpset) 1);
-qed"cont_flift1_not_arg";
-
-(* flift1 is continuous in a variable that occurs either
- in the Def branch or in the argument *)
-
-goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
-\ cont (%y. lift_case UU (f y) (g y))";
-br cont2cont_app 1;
-back();
-by (safe_tac set_cs);
-br cont_flift1_not_arg 1;
-auto();
-br cont_flift1_arg 1;
-qed"cont_flift1_arg_and_not_arg";
-
-(* flift2 is continuous in its argument itself *)
-
-goal thy "cont (lift_case UU (%y. Def (f y)))";
-br flatdom_strict2cont 1;
-br flat_lift 1;
-by (Simp_tac 1);
-qed"cont_flift2_arg";
+qed"ax_flat_lift";
(* Two specific lemmas for the combination of LCF and HOL terms *)
@@ -208,7 +159,6 @@
(* continuity of if then else *)
-
val prems = goal thy "[| cont f1; cont f2 |] ==> \
\ cont (%x. if b then f1 x else f2 x)";
by (cut_facts_tac prems 1);
@@ -216,57 +166,3 @@
by (TRYALL (fast_tac (HOL_cs addss HOL_ss)));
qed"cont_if";
-
-(* ---------------------------------------------------------- *)
-(* Extension of cont_tac and installation of simplifier *)
-(* ---------------------------------------------------------- *)
-
-bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev);
-
-val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
- cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2,
- cont_fapp_app,cont_fapp_app_app,cont_if];
-
-val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext;
-
-Addsimps cont_lemmas_ext;
-
-fun cont_tac i = resolve_tac cont_lemmas2 i;
-fun cont_tacR i = REPEAT (cont_tac i);
-
-fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
- REPEAT (cont_tac i);
-
-
-simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));
-
-(* ---------------------------------------------------------- *)
- section"flift1, flift2";
-(* ---------------------------------------------------------- *)
-
-
-goal thy "flift1 f`(Def x) = (f x)";
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
-qed"flift1_Def";
-
-goal thy "flift2 f`(Def x) = Def (f x)";
-by (simp_tac (!simpset addsimps [flift2_def]) 1);
-qed"flift2_Def";
-
-goal thy "flift1 f`UU = UU";
-by (simp_tac (!simpset addsimps [flift1_def]) 1);
-qed"flift1_UU";
-
-goal thy "flift2 f`UU = UU";
-by (simp_tac (!simpset addsimps [flift2_def]) 1);
-qed"flift2_UU";
-
-Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU];
-
-goal thy "!!x. x~=UU ==> (flift2 f)`x~=UU";
-by (def_tac 1);
-qed"flift2_nUU";
-
-Addsimps [flift2_nUU];
-
-
--- a/src/HOLCF/Makefile Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/Makefile Sun May 25 16:17:09 1997 +0200
@@ -29,9 +29,9 @@
Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \
One.thy Tr.thy \
- Lift1.thy Lift2.thy Lift3.thy HOLCF.thy
+ Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
-ONLYTHYS = Lift.thy
+ONLYTHYS =
FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
--- a/src/HOLCF/ccc1.thy Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ccc1.thy Sun May 25 16:17:09 1997 +0200
@@ -9,7 +9,7 @@
ccc1 = Cprod3 + Sprod3 + Ssum3 + Up3 + Fix +
-instance flat<chfin (flat_subclass_chfin)
+instance flat<chfin (flat_imp_chain_finite)
consts
ID :: "('a::cpo) -> 'a"
--- a/src/HOLCF/ex/Dnat.ML Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Dnat.ML Sun May 25 16:17:09 1997 +0200
@@ -47,7 +47,8 @@
val iterator_rews =
[iterator1, iterator2, iterator3];
-val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(x::dnat)" (fn _ => [
+val dnat_flat = prove_goal Dnat.thy "!x y::dnat.x<<y --> x=UU | x=y"
+(fn _ => [
(rtac allI 1),
(res_inst_tac [("x","x")] dnat.ind 1),
(fast_tac HOL_cs 1),
--- a/src/HOLCF/ex/Hoare.ML Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Hoare.ML Sun May 25 16:17:09 1997 +0200
@@ -95,7 +95,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (etac (flat_flat RS flat_codom RS disjE) 1),
+ (etac (flat_codom RS disjE) 1),
(atac 1),
(etac spec 1)
]);
@@ -323,7 +323,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (flat_flat RS flat_codom) 1),
+ (rtac (flat_codom) 1),
(res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
(etac spec 1)
]);
--- a/src/HOLCF/ex/Loop.ML Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Loop.ML Sun May 25 16:17:09 1997 +0200
@@ -57,7 +57,7 @@
(asm_simp_tac HOLCF_ss 1),
(stac while_unfold 1),
(res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
- (etac (flat_flat RS flat_codom RS disjE) 1),
+ (etac (flat_codom RS disjE) 1),
(atac 1),
(etac spec 1),
(simp_tac HOLCF_ss 1),
@@ -92,7 +92,7 @@
(rtac step_def2 1),
(asm_simp_tac HOLCF_ss 1),
(etac exE 1),
- (etac (flat_flat RS flat_codom RS disjE) 1),
+ (etac (flat_codom RS disjE) 1),
(asm_simp_tac HOLCF_ss 1),
(asm_simp_tac HOLCF_ss 1)
]);
--- a/src/HOLCF/ex/Stream.ML Sun May 25 11:07:52 1997 +0200
+++ b/src/HOLCF/ex/Stream.ML Sun May 25 16:17:09 1997 +0200
@@ -44,14 +44,15 @@
fast_tac (HOL_cs addDs stream.inverts) 1]);
qed_goal "stream_flat_prefix" thy
-"[| x && xs << y && ys; (x::'a) ~= UU; flat (z::'a) |] ==> x = y & xs << ys"(fn prems=>[
+"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
+(fn prems=>[
cut_facts_tac prems 1,
+ (cut_facts_tac [read_instantiate[("x1","x::'a::flat"),("x","y::'a::flat")]
+ (ax_flat RS spec RS spec)] 1),
(forward_tac stream.inverts 1),
(safe_tac HOL_cs),
(dtac (hd stream.con_rews RS subst) 1),
- (fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1),
- (rewtac flat_def),
- (fast_tac HOL_cs 1)]);
+ (fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1)]);
qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \
\(x = UU | (? a y. x = a && y & a ~= UU & a << b & y << z))" (fn prems => [