--- a/src/HOLCF/Fix.ML Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/Fix.ML Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
-(* Title: HOLCF/fix.ML
+(* Title: HOLCF/Fix.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for fix.thy
+Lemmas for Fix.thy
*)
open Fix;
@@ -12,13 +12,13 @@
(* derive inductive properties of iterate from primitive recursion *)
(* ------------------------------------------------------------------------ *)
-qed_goal "iterate_0" Fix.thy "iterate 0 F x = x"
+qed_goal "iterate_0" thy "iterate 0 F x = x"
(fn prems =>
[
(resolve_tac (nat_recs iterate_def) 1)
]);
-qed_goal "iterate_Suc" Fix.thy "iterate (Suc n) F x = F`(iterate n F x)"
+qed_goal "iterate_Suc" thy "iterate (Suc n) F x = F`(iterate n F x)"
(fn prems =>
[
(resolve_tac (nat_recs iterate_def) 1)
@@ -26,7 +26,7 @@
Addsimps [iterate_0, iterate_Suc];
-qed_goal "iterate_Suc2" Fix.thy "iterate (Suc n) F x = iterate n F (F`x)"
+qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
(fn prems =>
[
(nat_ind_tac "n" 1),
@@ -42,7 +42,7 @@
(* This property is essential since monotonicity of iterate makes no sense *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "is_chain_iterate2" Fix.thy [is_chain]
+qed_goalw "is_chain_iterate2" thy [is_chain]
" x << F`x ==> is_chain (%i.iterate i F x)"
(fn prems =>
[
@@ -56,7 +56,7 @@
]);
-qed_goal "is_chain_iterate" Fix.thy
+qed_goal "is_chain_iterate" thy
"is_chain (%i.iterate i F UU)"
(fn prems =>
[
@@ -71,7 +71,7 @@
(* ------------------------------------------------------------------------ *)
-qed_goalw "Ifix_eq" Fix.thy [Ifix_def] "Ifix F =F`(Ifix F)"
+qed_goalw "Ifix_eq" thy [Ifix_def] "Ifix F =F`(Ifix F)"
(fn prems =>
[
(stac contlub_cfun_arg 1),
@@ -95,7 +95,7 @@
]);
-qed_goalw "Ifix_least" Fix.thy [Ifix_def] "F`x=x ==> Ifix(F) << x"
+qed_goalw "Ifix_least" thy [Ifix_def] "F`x=x ==> Ifix(F) << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -116,7 +116,7 @@
(* monotonicity and continuity of iterate *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_iterate" Fix.thy [monofun] "monofun(iterate(i))"
+qed_goalw "monofun_iterate" thy [monofun] "monofun(iterate(i))"
(fn prems =>
[
(strip_tac 1),
@@ -137,7 +137,7 @@
(* In this special case it is the application function fapp *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "contlub_iterate" Fix.thy [contlub] "contlub(iterate(i))"
+qed_goalw "contlub_iterate" thy [contlub] "contlub(iterate(i))"
(fn prems =>
[
(strip_tac 1),
@@ -168,7 +168,7 @@
]);
-qed_goal "cont_iterate" Fix.thy "cont(iterate(i))"
+qed_goal "cont_iterate" thy "cont(iterate(i))"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -180,7 +180,7 @@
(* a lemma about continuity of iterate in its third argument *)
(* ------------------------------------------------------------------------ *)
-qed_goal "monofun_iterate2" Fix.thy "monofun(iterate n F)"
+qed_goal "monofun_iterate2" thy "monofun(iterate n F)"
(fn prems =>
[
(rtac monofunI 1),
@@ -191,7 +191,7 @@
(etac monofun_cfun_arg 1)
]);
-qed_goal "contlub_iterate2" Fix.thy "contlub(iterate n F)"
+qed_goal "contlub_iterate2" thy "contlub(iterate n F)"
(fn prems =>
[
(rtac contlubI 1),
@@ -206,7 +206,7 @@
(etac (monofun_iterate2 RS ch2ch_monofun) 1)
]);
-qed_goal "cont_iterate2" Fix.thy "cont (iterate n F)"
+qed_goal "cont_iterate2" thy "cont (iterate n F)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -218,7 +218,7 @@
(* monotonicity and continuity of Ifix *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "monofun_Ifix" Fix.thy [monofun,Ifix_def] "monofun(Ifix)"
+qed_goalw "monofun_Ifix" thy [monofun,Ifix_def] "monofun(Ifix)"
(fn prems =>
[
(strip_tac 1),
@@ -235,7 +235,7 @@
(* be derived for lubs in this argument *)
(* ------------------------------------------------------------------------ *)
-qed_goal "is_chain_iterate_lub" Fix.thy
+qed_goal "is_chain_iterate_lub" thy
"is_chain(Y) ==> is_chain(%i. lub(range(%ia. iterate ia (Y i) UU)))"
(fn prems =>
[
@@ -256,7 +256,7 @@
(* chains is the essential argument which is usually derived from monot. *)
(* ------------------------------------------------------------------------ *)
-qed_goal "contlub_Ifix_lemma1" Fix.thy
+qed_goal "contlub_Ifix_lemma1" thy
"is_chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))"
(fn prems =>
[
@@ -271,7 +271,7 @@
]);
-qed_goal "ex_lub_iterate" Fix.thy "is_chain(Y) ==>\
+qed_goal "ex_lub_iterate" thy "is_chain(Y) ==>\
\ lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\
\ lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))"
(fn prems =>
@@ -305,7 +305,7 @@
]);
-qed_goalw "contlub_Ifix" Fix.thy [contlub,Ifix_def] "contlub(Ifix)"
+qed_goalw "contlub_Ifix" thy [contlub,Ifix_def] "contlub(Ifix)"
(fn prems =>
[
(strip_tac 1),
@@ -315,7 +315,7 @@
]);
-qed_goal "cont_Ifix" Fix.thy "cont(Ifix)"
+qed_goal "cont_Ifix" thy "cont(Ifix)"
(fn prems =>
[
(rtac monocontlub2cont 1),
@@ -327,14 +327,14 @@
(* propagate properties of Ifix to its continuous counterpart *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "fix_eq" Fix.thy [fix_def] "fix`F = F`(fix`F)"
+qed_goalw "fix_eq" thy [fix_def] "fix`F = F`(fix`F)"
(fn prems =>
[
(asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
(rtac Ifix_eq 1)
]);
-qed_goalw "fix_least" Fix.thy [fix_def] "F`x = x ==> fix`F << x"
+qed_goalw "fix_least" thy [fix_def] "F`x = x ==> fix`F << x"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -343,7 +343,7 @@
]);
-qed_goal "fix_eqI" Fix.thy
+qed_goal "fix_eqI" thy
"[| F`x = x; !z. F`z = z --> x << z |] ==> x = fix`F"
(fn prems =>
[
@@ -356,14 +356,14 @@
]);
-qed_goal "fix_eq2" Fix.thy "f == fix`F ==> f = F`f"
+qed_goal "fix_eq2" thy "f == fix`F ==> f = F`f"
(fn prems =>
[
(rewrite_goals_tac prems),
(rtac fix_eq 1)
]);
-qed_goal "fix_eq3" Fix.thy "f == fix`F ==> f`x = F`f`x"
+qed_goal "fix_eq3" thy "f == fix`F ==> f`x = F`f`x"
(fn prems =>
[
(rtac trans 1),
@@ -373,7 +373,7 @@
fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i));
-qed_goal "fix_eq4" Fix.thy "f = fix`F ==> f = F`f"
+qed_goal "fix_eq4" thy "f = fix`F ==> f = F`f"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -381,7 +381,7 @@
(rtac fix_eq 1)
]);
-qed_goal "fix_eq5" Fix.thy "f = fix`F ==> f`x = F`f`x"
+qed_goal "fix_eq5" thy "f = fix`F ==> f`x = F`f`x"
(fn prems =>
[
(rtac trans 1),
@@ -418,7 +418,7 @@
(* ------------------------------------------------------------------------ *)
-qed_goal "Ifix_def2" Fix.thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
+qed_goal "Ifix_def2" thy "Ifix=(%x. lub(range(%i. iterate i x UU)))"
(fn prems =>
[
(rtac ext 1),
@@ -430,7 +430,7 @@
(* direct connection between fix and iteration without Ifix *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "fix_def2" Fix.thy [fix_def]
+qed_goalw "fix_def2" thy [fix_def]
"fix`F = lub(range(%i. iterate i F UU))"
(fn prems =>
[
@@ -447,14 +447,14 @@
(* access to definitions *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_def2" Fix.thy [adm_def]
+qed_goalw "adm_def2" thy [adm_def]
"adm(P) = (!Y. is_chain(Y) --> (!i.P(Y(i))) --> P(lub(range(Y))))"
(fn prems =>
[
(rtac refl 1)
]);
-qed_goalw "admw_def2" Fix.thy [admw_def]
+qed_goalw "admw_def2" thy [admw_def]
"admw(P) = (!F.(!n.P(iterate n F UU)) -->\
\ P (lub(range(%i.iterate i F UU))))"
(fn prems =>
@@ -466,7 +466,7 @@
(* an admissible formula is also weak admissible *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_impl_admw" Fix.thy [admw_def] "adm(P)==>admw(P)"
+qed_goalw "adm_impl_admw" thy [admw_def] "adm(P)==>admw(P)"
(fn prems =>
[
(cut_facts_tac prems 1),
@@ -481,7 +481,7 @@
(* fixed point induction *)
(* ------------------------------------------------------------------------ *)
-qed_goal "fix_ind" Fix.thy
+qed_goal "fix_ind" thy
"[| adm(P);P(UU);!!x. P(x) ==> P(F`x)|] ==> P(fix`F)"
(fn prems =>
[
@@ -499,7 +499,7 @@
(atac 1)
]);
-qed_goal "def_fix_ind" Fix.thy "[| f == fix`F; adm(P); \
+qed_goal "def_fix_ind" thy "[| f == fix`F; adm(P); \
\ P(UU);!!x. P(x) ==> P(F`x)|] ==> P f" (fn prems => [
(cut_facts_tac prems 1),
(asm_simp_tac HOL_ss 1),
@@ -511,7 +511,7 @@
(* computational induction for weak admissible formulae *)
(* ------------------------------------------------------------------------ *)
-qed_goal "wfix_ind" Fix.thy
+qed_goal "wfix_ind" thy
"[| admw(P); !n. P(iterate n F UU)|] ==> P(fix`F)"
(fn prems =>
[
@@ -523,7 +523,7 @@
(etac spec 1)
]);
-qed_goal "def_wfix_ind" Fix.thy "[| f == fix`F; admw(P); \
+qed_goal "def_wfix_ind" thy "[| f == fix`F; admw(P); \
\ !n. P(iterate n F UU) |] ==> P f" (fn prems => [
(cut_facts_tac prems 1),
(asm_simp_tac HOL_ss 1),
@@ -534,7 +534,7 @@
(* for chain-finite (easy) types every formula is admissible *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_max_in_chain" Fix.thy [adm_def]
+qed_goalw "adm_max_in_chain" thy [adm_def]
"!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain n Y) ==> adm(P::'a=>bool)"
(fn prems =>
[
@@ -550,7 +550,7 @@
(etac spec 1)
]);
-qed_goalw "adm_chain_finite" Fix.thy [chain_finite_def]
+qed_goalw "adm_chain_finite" thy [chain_finite_def]
"chain_finite(x::'a) ==> adm(P::'a=>bool)"
(fn prems =>
[
@@ -562,7 +562,7 @@
(* flat types are chain_finite *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flat_imp_chain_finite" Fix.thy [flat_def,chain_finite_def]
+qed_goalw "flat_imp_chain_finite" thy [flat_def,chain_finite_def]
"flat(x::'a)==>chain_finite(x::'a)"
(fn prems =>
[
@@ -606,7 +606,16 @@
(* some properties of flat *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "flatdom2monofun" Fix.thy [flat_def]
+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)"
(fn prems =>
[
@@ -615,15 +624,7 @@
]);
-qed_goalw "flat_void" Fix.thy [flat_def] "flat(UU::void)"
- (fn prems =>
- [
- (strip_tac 1),
- (rtac disjI1 1),
- (rtac unique_void2 1)
- ]);
-
-qed_goalw "flat_eq" Fix.thy [flat_def]
+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)]);
@@ -633,8 +634,19 @@
(* some lemmata for functions with flat/chain_finite domain/range types *)
(* ------------------------------------------------------------------------ *)
-qed_goal "chfin2finch" Fix.thy
- "[| is_chain (Y::nat=>'a); chain_finite (x::'a) |] ==> finite_chain Y"
+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 =>
[
cut_facts_tac prems 1,
@@ -642,7 +654,9 @@
(!simpset addsimps [chain_finite_def,finite_chain_def])) 1
]);
-qed_goal "chfindom_monofun2cont" Fix.thy
+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)"
(fn prems =>
[
@@ -666,7 +680,7 @@
bind_thm("flatdom_monofun2cont",flat_imp_chain_finite RS chfindom_monofun2cont);
(* [| flat ?x; monofun ?f |] ==> cont ?f *)
-qed_goal "flatdom_strict2cont" Fix.thy
+qed_goal "flatdom_strict2cont" thy
"[| flat(x::'a::pcpo); f UU = UU |] ==> cont (f::'a=>'b::pcpo)"
(fn prems =>
[
@@ -675,7 +689,7 @@
flat_imp_chain_finite RS chfindom_monofun2cont])) 1
]);
-qed_goal "chfin_fappR" Fix.thy
+qed_goal "chfin_fappR" thy
"[| is_chain (Y::nat => 'a->'b); chain_finite(x::'b) |] ==> \
\ !s. ? n. lub(range(Y))`s = Y n`s"
(fn prems =>
@@ -687,7 +701,7 @@
fast_tac (HOL_cs addSIs [thelubI,lub_finch2,chfin2finch,ch2ch_fappL])1
]);
-qed_goalw "adm_chfindom" Fix.thy [adm_def]
+qed_goalw "adm_chfindom" thy [adm_def]
"chain_finite (x::'b) ==> adm (%(u::'a->'b). P(u`s))" (fn prems => [
cut_facts_tac prems 1,
strip_tac 1,
@@ -731,7 +745,7 @@
fast_tac (HOL_cs addDs [le_imp_less_or_eq]
addEs [chain_mono RS mp]) 1]);
-qed_goalw "admI" Fix.thy [adm_def]
+qed_goalw "admI" thy [adm_def]
"(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
\ ==> P(lub (range Y))) ==> adm P"
(fn prems => [
@@ -745,7 +759,7 @@
(* a prove for embedding projection pairs is similar *)
(* ------------------------------------------------------------------------ *)
-qed_goal "iso_strict" Fix.thy
+qed_goal "iso_strict" thy
"!!f g.[|!y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
\ ==> f`UU=UU & g`UU=UU"
(fn prems =>
@@ -762,7 +776,7 @@
]);
-qed_goal "isorep_defined" Fix.thy
+qed_goal "isorep_defined" thy
"[|!x.rep`(abs`x)=x;!y.abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
(fn prems =>
[
@@ -776,7 +790,7 @@
(atac 1)
]);
-qed_goal "isoabs_defined" Fix.thy
+qed_goal "isoabs_defined" thy
"[|!x.rep`(abs`x) = x;!y.abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
(fn prems =>
[
@@ -794,7 +808,7 @@
(* propagation of flatness and chainfiniteness by continuous isomorphisms *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chfin2chfin" Fix.thy [chain_finite_def]
+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)"
(fn prems =>
@@ -817,7 +831,7 @@
(atac 1)
]);
-qed_goalw "flat2flat" Fix.thy [flat_def]
+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)"
(fn prems =>
@@ -848,7 +862,7 @@
(* a result about functions with flat codomain *)
(* ------------------------------------------------------------------------- *)
-qed_goalw "flat_codom" Fix.thy [flat_def]
+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)"
(fn prems =>
[
@@ -885,7 +899,7 @@
(* admissibility of special formulae and propagation *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "adm_less" Fix.thy [adm_def]
+qed_goalw "adm_less" thy [adm_def]
"[|cont u;cont v|]==> adm(%x.u x << v x)"
(fn prems =>
[
@@ -905,7 +919,7 @@
(atac 1)
]);
-qed_goal "adm_conj" Fix.thy
+qed_goal "adm_conj" thy
"[| adm P; adm Q |] ==> adm(%x. P x & Q x)"
(fn prems =>
[
@@ -923,7 +937,7 @@
(fast_tac HOL_cs 1)
]);
-qed_goal "adm_cong" Fix.thy
+qed_goal "adm_cong" thy
"(!x. P x = Q x) ==> adm P = adm Q "
(fn prems =>
[
@@ -934,13 +948,13 @@
(etac spec 1)
]);
-qed_goalw "adm_not_free" Fix.thy [adm_def] "adm(%x.t)"
+qed_goalw "adm_not_free" thy [adm_def] "adm(%x.t)"
(fn prems =>
[
(fast_tac HOL_cs 1)
]);
-qed_goalw "adm_not_less" Fix.thy [adm_def]
+qed_goalw "adm_not_less" thy [adm_def]
"cont t ==> adm(%x.~ (t x) << u)"
(fn prems =>
[
@@ -955,7 +969,7 @@
(atac 1)
]);
-qed_goal "adm_all" Fix.thy
+qed_goal "adm_all" thy
" !y.adm(P y) ==> adm(%x.!y.P y x)"
(fn prems =>
[
@@ -972,7 +986,7 @@
bind_thm ("adm_all2", allI RS adm_all);
-qed_goal "adm_subst" Fix.thy
+qed_goal "adm_subst" thy
"[|cont t; adm P|] ==> adm(%x. P (t x))"
(fn prems =>
[
@@ -990,7 +1004,7 @@
(atac 1)
]);
-qed_goal "adm_UU_not_less" Fix.thy "adm(%x.~ UU << t(x))"
+qed_goal "adm_UU_not_less" thy "adm(%x.~ UU << t(x))"
(fn prems =>
[
(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
@@ -998,7 +1012,7 @@
(rtac adm_not_free 1)
]);
-qed_goalw "adm_not_UU" Fix.thy [adm_def]
+qed_goalw "adm_not_UU" thy [adm_def]
"cont(t)==> adm(%x.~ (t x) = UU)"
(fn prems =>
[
@@ -1016,7 +1030,7 @@
(atac 1)
]);
-qed_goal "adm_eq" Fix.thy
+qed_goal "adm_eq" thy
"[|cont u ; cont v|]==> adm(%x. u x = v x)"
(fn prems =>
[
@@ -1052,13 +1066,13 @@
(fast_tac HOL_cs 1)
]);
- val adm_disj_lemma2 = prove_goal Fix.thy
+ val adm_disj_lemma2 = prove_goal thy
"!!Q. [| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
\ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
(fn _ => [fast_tac (!claset addEs [adm_def2 RS iffD1 RS spec RS mp RS mp]
addss !simpset) 1]);
- val adm_disj_lemma3 = prove_goalw Fix.thy [is_chain]
+ val adm_disj_lemma3 = prove_goalw thy [is_chain]
"!!Q. is_chain(Y) ==> is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
(fn _ =>
[
@@ -1080,7 +1094,7 @@
trans_tac 1
]);
- val adm_disj_lemma5 = prove_goal Fix.thy
+ val adm_disj_lemma5 = prove_goal thy
"!!Y::nat=>'a. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
(fn prems =>
@@ -1093,7 +1107,7 @@
trans_tac 1
]);
- val adm_disj_lemma6 = prove_goal Fix.thy
+ val adm_disj_lemma6 = prove_goal thy
"[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
\ ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
(fn prems =>
@@ -1112,7 +1126,7 @@
(atac 1)
]);
- val adm_disj_lemma7 = prove_goal Fix.thy
+ val adm_disj_lemma7 = prove_goal thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
(fn prems =>
@@ -1135,7 +1149,7 @@
(atac 1)
]);
- val adm_disj_lemma8 = prove_goal Fix.thy
+ val adm_disj_lemma8 = prove_goal thy
"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
(fn prems =>
[
@@ -1146,7 +1160,7 @@
(etac (LeastI RS conjunct2) 1)
]);
- val adm_disj_lemma9 = prove_goal Fix.thy
+ val adm_disj_lemma9 = prove_goal thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
(fn prems =>
@@ -1177,7 +1191,7 @@
(rtac lessI 1)
]);
- val adm_disj_lemma10 = prove_goal Fix.thy
+ val adm_disj_lemma10 = prove_goal thy
"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
\ ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
(fn prems =>
@@ -1196,7 +1210,7 @@
(atac 1)
]);
- val adm_disj_lemma12 = prove_goal Fix.thy
+ val adm_disj_lemma12 = prove_goal thy
"[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
(fn prems =>
[
@@ -1208,7 +1222,7 @@
in
-val adm_lemma11 = prove_goal Fix.thy
+val adm_lemma11 = prove_goal thy
"[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
(fn prems =>
[
@@ -1218,7 +1232,7 @@
(atac 1)
]);
-val adm_disj = prove_goal Fix.thy
+val adm_disj = prove_goal thy
"[| adm P; adm Q |] ==> adm(%x.P x | Q x)"
(fn prems =>
[
@@ -1242,7 +1256,7 @@
bind_thm("adm_lemma11",adm_lemma11);
bind_thm("adm_disj",adm_disj);
-qed_goal "adm_imp" Fix.thy
+qed_goal "adm_imp" thy
"[| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)"
(fn prems =>
[
@@ -1254,7 +1268,7 @@
(atac 1)
]);
-qed_goal "adm_not_conj" Fix.thy
+qed_goal "adm_not_conj" thy
"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
cut_facts_tac prems 1,
subgoal_tac