# HG changeset patch
# User oheimb
# Date 991320752 -7200
# Node ID 0d28bc66495526113932567621d24d272df3c5e0
# Parent  cd605c85e421080c1e99c4bcf4b8e98ce924f681
corrected ML names of definitions

diff -r cd605c85e421 -r 0d28bc664955 src/HOLCF/Discrete.ML
--- 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];
diff -r cd605c85e421 -r 0d28bc664955 src/HOLCF/Discrete1.ML
--- 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";
diff -r cd605c85e421 -r 0d28bc664955 src/HOLCF/Fix.ML
--- 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;
diff -r cd605c85e421 -r 0d28bc664955 src/HOLCF/Fun2.ML
--- 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";
 
diff -r cd605c85e421 -r 0d28bc664955 src/HOLCF/Porder.thy
--- 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)"