src/HOLCF/Pcpo.ML

--- a/src/HOLCF/Pcpo.ML	Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Pcpo.ML	Wed Jul 05 16:37:52 2000 +0200
@@ -18,14 +18,14 @@
 
 bind_thm("minimal", UU_least RS spec);
 
+AddIffs [minimal];
+
 (* ------------------------------------------------------------------------ *)
 (* in cpo's everthing equal to THE lub has lub properties for every chain  *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[| chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l ";
-by (hyp_subst_tac 1);
-by (rtac lubI 1);
-by (etac cpo 1);
+Goal "[| chain(S); lub(range(S)) = (l::'a::cpo) |] ==> range(S) <<| l ";
+by (blast_tac (claset() addDs [cpo] addIs [lubI]) 1);
 qed "thelubE";
 
 (* ------------------------------------------------------------------------ *)
@@ -33,11 +33,14 @@
 (* ------------------------------------------------------------------------ *)
 
 
-bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub);
-(* chain(?S1) ==> ?S1(?x) << lub(range(?S1))                             *)
+Goal "chain (S::nat => 'a::cpo) ==> S(x) << lub(range(S))";
+by (blast_tac (claset() addDs [cpo] addIs [lubI RS is_ub_lub]) 1);
+qed "is_ub_thelub";
 
-bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
-(* [| chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
+Goal "[| chain (S::nat => 'a::cpo); range(S) <| x |] ==> lub(range S) << x";
+by (blast_tac (claset() addDs [cpo] addIs [lubI RS is_lub_lub]) 1);
+qed "is_lub_thelub";
+
 
 Goal "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))";
 by (rtac iffI 1);
@@ -58,7 +61,6 @@
 \     ==> lub(range(C1)) << lub(range(C2))";
 by (etac is_lub_thelub 1);
 by (rtac ub_rangeI 1);
-by (rtac allI 1);
 by (rtac trans_less 1);
 by (etac spec 1);
 by (etac is_ub_thelub 1);
@@ -103,7 +105,7 @@
 by (rtac is_ub_thelub 1);
 by (assume_tac 1);
 by (res_inst_tac [("y","X(Suc(j))")] trans_less 1);
-by (rtac (chain_mono RS mp) 1);
+by (rtac chain_mono 1);
 by (assume_tac 1);
 by (rtac (not_less_eq RS subst) 1);
 by (atac 1);
@@ -164,7 +166,6 @@
 
 Goal "ALL i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU";
 by (rtac lub_chain_maxelem 1);
-by (rtac exI 1);
 by (etac spec 1);
 by (rtac allI 1);
 by (rtac (antisym_less_inverse RS conjunct1) 1);
@@ -181,7 +182,7 @@
 
 Goal 
  "[|EX j. ~Y(j)=UU;chain(Y::nat=>'a::pcpo)|] ==> EX j. ALL i. j<i-->~Y(i)=UU";
-by (blast_tac (claset() addDs [notUU_I, chain_mono RS mp]) 1);
+by (blast_tac (claset() addDs [notUU_I, chain_mono]) 1);
 qed "chain_mono2";
 
 (**************************************)
@@ -192,9 +193,10 @@
 (* flat types are chfin                                              *)
 (* ------------------------------------------------------------------------ *)
 
+(*Used only in an "instance" declaration (Fun1.thy)*)
 Goalw [max_in_chain_def]
-     "ALL Y::nat=>'a::flat. chain Y-->(EX n. max_in_chain n Y)";
-by (strip_tac 1);
+     "ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)";
+by (Clarify_tac 1);
 by (case_tac "ALL i. Y(i)=UU" 1);
 by (res_inst_tac [("x","0")] exI 1);
 by (Asm_simp_tac 1);
@@ -202,11 +204,9 @@
 by (etac exE 1);
 by (res_inst_tac [("x","i")] exI 1);
 by (strip_tac 1);
-by (dres_inst_tac [("x","i"),("y","j")] chain_mono 1);
 by (etac (le_imp_less_or_eq RS disjE) 1);
 by Safe_tac;
-by (dtac (ax_flat RS spec RS spec RS mp) 1);
-by (Fast_tac 1);
+by (blast_tac (claset() addDs [chain_mono, ax_flat RS spec RS spec RS mp]) 1);
 qed "flat_imp_chfin";
 
 (* flat subclass of chfin --> adm_flat not needed *)
@@ -253,5 +253,5 @@
 by (rewtac finite_chain_def);
 by (rewtac max_in_chain_def);
 by (fast_tac (HOL_cs addIs prems
-		     addDs [le_imp_less_or_eq] addEs [chain_mono RS mp]) 1);
+		     addDs [le_imp_less_or_eq] addEs [chain_mono]) 1);
 qed "increasing_chain_adm_lemma";