src/HOLCF/Porder.ML

--- a/src/HOLCF/Porder.ML	Wed Jul 05 14:26:58 2000 +0200
+++ b/src/HOLCF/Porder.ML	Wed Jul 05 16:37:52 2000 +0200
@@ -11,46 +11,25 @@
 (* ------------------------------------------------------------------------ *)
 
 
-val prems = goalw thy [is_lub, is_ub] 
+Goalw [is_lub, is_ub] 
         "[| S <<| x ; S <<| y |] ==> x=y";
-by (cut_facts_tac prems 1);
-by (etac conjE 1);
-by (etac conjE 1);
-by (rtac antisym_less 1);
-by (rtac mp 1);
-by ((etac allE 1) THEN (atac 1) THEN (atac 1));
-by (rtac mp 1);
-by ((etac allE 1) THEN (atac 1) THEN (atac 1));
+by (blast_tac (claset() addIs [antisym_less]) 1);
 qed "unique_lub";
 
 (* ------------------------------------------------------------------------ *)
 (* chains are monotone functions                                            *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = goalw thy [chain] "chain F ==> x<y --> F x<<F y";
-by (cut_facts_tac prems 1);
+Goalw [chain] "chain F ==> x<y --> F x<<F y";
 by (induct_tac "y" 1);
-by (rtac impI 1);
-by (etac less_zeroE 1);
-by (stac less_Suc_eq 1);
-by (strip_tac 1);
-by (etac disjE 1);
-by (rtac trans_less 1);
-by (etac allE 2);
-by (atac 2);
-by (fast_tac HOL_cs 1);
-by (hyp_subst_tac 1);
-by (etac allE 1);
-by (atac 1);
-qed "chain_mono";
+by Auto_tac;  
+by (blast_tac (claset() addIs [trans_less]) 2);
+by (blast_tac (claset() addSEs [less_SucE]) 1);
+qed_spec_mp "chain_mono";
 
 Goal "[| chain F; x <= y |] ==> F x << F y";
-by (rtac (le_imp_less_or_eq RS disjE) 1);
-by (atac 1);
-by (etac (chain_mono RS mp) 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (rtac refl_less 1);
+by (dtac le_imp_less_or_eq 1);
+by (blast_tac (claset() addIs [chain_mono]) 1);
 qed "chain_mono3";
 
 
@@ -58,11 +37,10 @@
 (* The range of a chain is a totally ordered     <<                         *)
 (* ------------------------------------------------------------------------ *)
 
-val _ = goalw thy [tord] 
-"!!F. chain(F) ==> tord(range(F))";
+Goalw [tord] "chain(F) ==> tord(range(F))";
 by (Safe_tac);
 by (rtac nat_less_cases 1);
-by (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])));
+by (ALLGOALS (fast_tac (claset() addIs [chain_mono])));
 qed "chain_tord";
 
 
@@ -71,21 +49,9 @@
 (* ------------------------------------------------------------------------ *)
 bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
 
-Goal "? x. M <<| x ==> M <<| lub(M)";
-by (stac lub 1);
-by (etac (select_eq_Ex RS iffD2) 1);
-qed "lubI";
-
-Goal "M <<| lub(M) ==> ? x. M <<| x";
-by (etac exI 1);
-qed "lubE";
-
-Goal "(? x. M <<| x)  = M <<| lub(M)";
-by (stac lub 1);
-by (rtac (select_eq_Ex RS subst) 1);
-by (rtac refl 1);
-qed "lub_eq";
-
+Goal "EX x. M <<| x ==> M <<| lub(M)";
+by (asm_full_simp_tac (simpset() addsimps [lub, Ex_def]) 1);
+bind_thm ("lubI", exI RS result());
 
 Goal "M <<| l ==> lub(M) = l";
 by (rtac unique_lub 1);
@@ -96,8 +62,7 @@
 
 
 Goal "lub{x} = x";
-by (rtac thelubI 1);
-by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
+by (simp_tac (simpset() addsimps [thelubI,is_lub,is_ub]) 1);
 qed "lub_singleton";
 Addsimps [lub_singleton];
 
@@ -105,65 +70,51 @@
 (* access to some definition as inference rule                              *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = goalw thy [is_lub]
-        "S <<| x  ==> S <| x & (! u. S <| u  --> x << u)";
-by (cut_facts_tac prems 1);
-by (atac 1);
-qed "is_lubE";
+Goalw [is_lub] "S <<| x ==> S <| x";
+by Auto_tac;
+qed "is_lubD1";
 
-val prems = goalw thy [is_lub]
-        "S <| x & (! u. S <| u  --> x << u) ==> S <<| x";
-by (cut_facts_tac prems 1);
-by (atac 1);
+Goalw [is_lub] "[| S <<| x; S <| u |] ==> x << u";
+by Auto_tac;
+qed "is_lub_lub";
+
+val prems = Goalw [is_lub]
+        "[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x";
+by (blast_tac (claset() addIs prems) 1);
 qed "is_lubI";
 
-val prems = goalw thy [chain] "chain F ==> !i. F(i) << F(Suc(i))";
-by (cut_facts_tac prems 1);
-by (atac 1);
+Goalw [chain] "chain F ==> F(i) << F(Suc(i))";
+by Auto_tac;
 qed "chainE";
 
-val prems = goalw thy [chain] "!i. F i << F(Suc i) ==> chain F";
-by (cut_facts_tac prems 1);
-by (atac 1);
+val prems = Goalw [chain] "(!!i. F i << F(Suc i)) ==> chain F";
+by (blast_tac (claset() addIs prems) 1);
 qed "chainI";
 
 (* ------------------------------------------------------------------------ *)
 (* technical lemmas about (least) upper bounds of chains                    *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = goalw thy [is_ub] "range S <| x  ==> !i. S(i) << x";
-by (cut_facts_tac prems 1);
-by (strip_tac 1);
-by (rtac mp 1);
-by (etac spec 1);
-by (rtac rangeI 1);
-qed "ub_rangeE";
+Goalw [is_ub] "range S <| x  ==> S(i) << x";
+by (Blast_tac 1);
+qed "ub_rangeD";
 
-val prems = goalw thy [is_ub] "!i. S i << x  ==> range S <| x";
-by (cut_facts_tac prems 1);
-by (strip_tac 1);
-by (etac rangeE 1);
-by (hyp_subst_tac 1);
-by (etac spec 1);
+val prems = Goalw [is_ub] "(!!i. S i << x) ==> range S <| x";
+by (blast_tac (claset() addIs prems) 1);
 qed "ub_rangeI";
 
-bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
+bind_thm ("is_ub_lub", is_lubD1 RS ub_rangeD);
 (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
 
-bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
-(* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1                             *)
 
 (* ------------------------------------------------------------------------ *)
 (* results about finite chains                                              *)
 (* ------------------------------------------------------------------------ *)
 
-val prems = goalw thy [max_in_chain_def]
+Goalw [max_in_chain_def]
         "[| chain C; max_in_chain i C|] ==> range C <<| C i";
-by (cut_facts_tac prems 1);
 by (rtac is_lubI 1);
-by (rtac conjI 1);
 by (rtac ub_rangeI 1);
-by (rtac allI 1);
 by (res_inst_tac [("m","i")] nat_less_cases 1);
 by (rtac (antisym_less_inverse RS conjunct2) 1);
 by (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1);
@@ -171,37 +122,30 @@
 by (rtac (antisym_less_inverse RS conjunct2) 1);
 by (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1);
 by (etac spec 1);
-by (etac (chain_mono RS mp) 1);
+by (etac chain_mono 1);
 by (atac 1);
-by (strip_tac 1);
-by (etac (ub_rangeE RS spec) 1);
+by (etac (ub_rangeD) 1);
 qed "lub_finch1";     
 
-val prems= goalw thy [finite_chain_def]
+Goalw [finite_chain_def]
         "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
-by (cut_facts_tac prems 1);
 by (rtac lub_finch1 1);
-by (etac conjunct1 1);
-by (rtac (select_eq_Ex RS iffD2) 1);
-by (etac conjunct2 1);
+by (best_tac (claset() addIs [selectI]) 2);
+by (Blast_tac 1);
 qed "lub_finch2";
 
 
 Goal "x<<y ==> chain (%i. if i=0 then x else y)";
 by (rtac chainI 1);
-by (rtac allI 1);
 by (induct_tac "i" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac;  
 qed "bin_chain";
 
-val prems = goalw thy [max_in_chain_def,le_def]
+Goalw [max_in_chain_def,le_def]
         "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)";
-by (cut_facts_tac prems 1);
 by (rtac allI 1);
 by (induct_tac "j" 1);
-by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
+by Auto_tac; 
 qed "bin_chainmax";
 
 Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y";
@@ -209,22 +153,16 @@
     THEN rtac lub_finch1 2);
 by (etac bin_chain 2);
 by (etac bin_chainmax 2);
-by (Simp_tac  1);
+by (Simp_tac 1);
 qed "lub_bin_chain";
 
 (* ------------------------------------------------------------------------ *)
 (* the maximal element in a chain is its lub                                *)
 (* ------------------------------------------------------------------------ *)
 
-Goal "[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c";
-by (rtac thelubI 1);
-by (rtac is_lubI 1);
-by (rtac conjI 1);
-by (etac ub_rangeI 1);
-by (strip_tac 1);
-by (etac exE 1);
-by (hyp_subst_tac 1);
-by (etac (ub_rangeE RS spec) 1);
+Goal "[| Y i = c;  ALL i. Y i<<c |] ==> lub(range Y) = c";
+by (blast_tac (claset()  addDs [ub_rangeD] 
+                         addIs [thelubI, is_lubI, ub_rangeI]) 1);
 qed "lub_chain_maxelem";
 
 (* ------------------------------------------------------------------------ *)
@@ -232,13 +170,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goal "range(%x. c) <<| c";
-by (rtac is_lubI 1);
-by (rtac conjI 1);
-by (rtac ub_rangeI 1);
-by (strip_tac 1);
-by (rtac refl_less 1);
-by (strip_tac 1);
-by (etac (ub_rangeE RS spec) 1);
+by (blast_tac (claset()  addDs [ub_rangeD] addIs [is_lubI, ub_rangeI]) 1);
 qed "lub_const";