src/HOLCF/Lift2.ML

--- a/src/HOLCF/Lift2.ML	Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Lift2.ML	Wed Jul 05 16:37:52 2000 +0200
@@ -7,7 +7,7 @@
 *)
 
 (* for compatibility with old HOLCF-Version *)
-val prems = goal thy "(op <<)=(%x y. x=y|x=Undef)";
+Goal "(op <<)=(%x y. x=y|x=Undef)";
 by (fold_goals_tac [less_lift_def]);
 by (rtac refl 1);
 qed "inst_lift_po";
@@ -22,7 +22,9 @@
 
 bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
 
-val prems = goal thy "? x::'a lift.!y. x<<y";
+AddIffs [minimal_lift];
+
+Goal "EX x::'a lift. ALL y. x<<y";
 by (res_inst_tac [("x","Undef")] exI 1);
 by (rtac (minimal_lift RS allI) 1);
 qed "least_lift";
@@ -39,41 +41,37 @@
 (* Tailoring notUU_I of Pcpo.ML to Undef *)
 
 Goal "[| x<<y; ~x=Undef |] ==> ~y=Undef";
-by (etac contrapos 1);
-by (hyp_subst_tac 1);
-by (rtac antisym_less 1);
-by (atac 1);
-by (rtac minimal_lift 1);
+by (blast_tac (claset() addIs [antisym_less]) 1);
 qed"notUndef_I";
 
 
 (* Tailoring chain_mono2 of Pcpo.ML to Undef *)
 
-Goal "[| ? j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] \
-\        ==> ? j.!i. j<i-->~Y(i)=Undef";
+Goal "[| EX j.~Y(j)=Undef; chain(Y::nat=>('a)lift) |] \
+\        ==> EX j. ALL i. j<i-->~Y(i)=Undef";
 by Safe_tac;
 by (Step_tac 1);
 by (strip_tac 1);
 by (rtac notUndef_I 1);
 by (atac 2);
-by (etac (chain_mono RS mp) 1);
+by (etac (chain_mono) 1);
 by (atac 1);
 qed"chain_mono2_po";
 
 
 (* Tailoring flat_imp_chfin of Fix.ML to lift *)
 
-Goal "(! Y. chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
+Goal "(ALL Y. chain(Y::nat=>('a)lift)-->(EX n. max_in_chain n Y))";
 by (rewtac max_in_chain_def);  
 by (strip_tac 1);
-by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm  1);
+by (res_inst_tac [("P","ALL i. Y(i)=Undef")] case_split_thm  1);
 by (res_inst_tac [("x","0")] exI 1);
 by (strip_tac 1);
 by (rtac trans 1);
 by (etac spec 1);
 by (rtac sym 1);
 by (etac spec 1); 
-by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
+by (subgoal_tac "ALL x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
 by (simp_tac (simpset() addsimps [inst_lift_po]) 2);
 by (rtac (chain_mono2_po RS exE) 1); 
 by (Fast_tac 1); 
@@ -86,29 +84,16 @@
 by (dtac spec 1);
 by (etac spec 1); 
 by (etac (le_imp_less_or_eq RS disjE) 1); 
-by (etac (chain_mono RS mp) 1); 
-by (atac 1); 
-by (hyp_subst_tac 1); 
-by (rtac refl_less 1); 
-by (res_inst_tac [("P","Y(Suc(x)) = Undef")] notE 1); 
-by (atac 2); 
-by (rtac mp 1); 
-by (etac spec 1); 
-by (Asm_simp_tac 1);
+by (etac (chain_mono) 1);
+by Auto_tac;   
 qed"flat_imp_chfin_poo";
 
 
 (* Main Lemma: cpo_lift *)
 
-Goal "chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
+Goal "chain(Y::nat=>('a)lift) ==> EX x. range(Y) <<|x";
 by (cut_inst_tac [] flat_imp_chfin_poo 1);
-by (Step_tac 1);
-by Safe_tac;
-by (Step_tac 1); 
-by (rtac exI 1);
-by (rtac lub_finch1 1);
-by (atac 1);
-by (atac 1);
+by (blast_tac (claset() addIs [lub_finch1]) 1);
 qed"cpo_lift";