--- a/src/HOLCF/Discrete.ML Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Discrete.ML Thu May 31 16:52:32 2001 +0200
@@ -14,7 +14,7 @@
by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
qed "discr_chain_f_range0";
-Goalw [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
+Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::term)discr. f x)";
by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
qed "cont_discr";
AddIffs [cont_discr];
--- a/src/HOLCF/Discrete1.ML Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Discrete1.ML Thu May 31 16:52:32 2001 +0200
@@ -11,7 +11,7 @@
qed "discr_less_eq";
AddIffs [discr_less_eq];
-Goalw [chain]
+Goalw [chain_def]
"!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
by (induct_tac "i" 1);
by (rtac refl 1);
@@ -26,7 +26,7 @@
qed "discr_chain_range0";
Addsimps [discr_chain_range0];
-Goalw [is_lub,is_ub]
+Goalw [is_lub_def,is_ub_def]
"!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
by (Asm_simp_tac 1);
qed "discr_cpo";
--- a/src/HOLCF/Fix.ML Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Fix.ML Thu May 31 16:52:32 2001 +0200
@@ -20,7 +20,7 @@
(* This property is essential since monotonicity of iterate makes no sense *)
(* ------------------------------------------------------------------------ *)
-Goalw [chain] "x << F$x ==> chain (%i. iterate i F x)";
+Goalw [chain_def] "x << F$x ==> chain (%i. iterate i F x)";
by (strip_tac 1);
by (induct_tac "i" 1);
by Auto_tac;
@@ -28,7 +28,7 @@
qed "chain_iterate2";
-Goal "chain (%i. iterate i F UU)";
+Goal "chain (%i. iterate i F UU)";
by (rtac chain_iterate2 1);
by (rtac minimal 1);
qed "chain_iterate";
@@ -350,10 +350,15 @@
(* ------------------------------------------------------------------------ *)
val prems = Goalw [adm_def]
- "(!!Y. [| chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)";
+ "(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P";
by (blast_tac (claset() addIs prems) 1);
qed "admI";
+Goal "!x. P x ==> adm P";
+by (rtac admI 1);
+by (etac spec 1);
+qed "triv_admI";
+
Goalw [adm_def] "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))";
by (Blast_tac 1);
qed "admD";
@@ -558,7 +563,7 @@
by (force_tac (claset() addEs [admD], simpset()) 1);
qed "adm_disj_lemma2";
-Goalw [chain] "chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)";
+Goalw [chain_def]"chain Y ==> chain (%m. if m < Suc i then Y (Suc i) else Y m)";
by (Asm_simp_tac 1);
by (safe_tac HOL_cs);
by (subgoal_tac "ia = i" 1);
@@ -722,7 +727,7 @@
by (atac 1);
qed "adm_not_conj";
-bind_thms ("adm_lemmas", [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
- adm_all2,adm_not_less,adm_not_conj,adm_iff]);
+bind_thms ("adm_lemmas", [adm_not_free,adm_imp,adm_disj,adm_eq,adm_not_UU,
+ adm_UU_not_less,adm_all2,adm_not_less,adm_not_conj,adm_iff]);
Addsimps adm_lemmas;
--- a/src/HOLCF/Fun2.ML Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Fun2.ML Thu May 31 16:52:32 2001 +0200
@@ -40,7 +40,7 @@
(* chains of functions yield chains in the po range *)
(* ------------------------------------------------------------------------ *)
-Goalw [chain] "chain(S::nat=>('a=>'b::po)) ==> chain(% i. S(i)(x))";
+Goalw [chain_def] "chain (S::nat=>('a=>'b::po)) ==> chain (%i. S i x)";
by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
qed "ch2ch_fun";
--- a/src/HOLCF/Porder.thy Thu May 31 16:52:20 2001 +0200
+++ b/src/HOLCF/Porder.thy Thu May 31 16:52:32 2001 +0200
@@ -33,14 +33,14 @@
defs
(* class definitions *)
-is_ub "S <| x == ! y. y:S --> y<<x"
-is_lub "S <<| x == S <| x & (! u. S <| u --> x << u)"
+is_ub_def "S <| x == ! y. y:S --> y<<x"
+is_lub_def "S <<| x == S <| x & (!u. S <| u --> x << u)"
(* Arbitrary chains are total orders *)
-tord "tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
+tord_def "tord S == !x y. x:S & y:S --> (x<<y | y<<x)"
(* Here we use countable chains and I prefer to code them as functions! *)
-chain "chain F == (! i. F(i) << F(Suc(i)))"
+chain_def "chain F == !i. F i << F (Suc i)"
(* finite chains, needed for monotony of continouous functions *)
max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)"