WF.ML

--- a/WF.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/WF.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -21,7 +21,7 @@
 by (rtac allE 1);
 by (assume_tac 1);
 by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
-val wfI = result();
+qed "wfI";
 
 val major::prems = goalw WF.thy [wf_def]
     "[| wf(r);          \
@@ -29,7 +29,7 @@
 \    |]  ==>  P(a)";
 by (rtac (major RS spec RS mp RS spec) 1);
 by (fast_tac (HOL_cs addEs prems) 1);
-val wf_induct = result();
+qed "wf_induct";
 
 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
 fun wf_ind_tac a prems i = 
@@ -42,12 +42,12 @@
 by (fast_tac (HOL_cs addIs prems) 1);
 by (wf_ind_tac "a" prems 1);
 by (fast_tac set_cs 1);
-val wf_asym = result();
+qed "wf_asym";
 
 val prems = goal WF.thy "[| wf(r);  <a,a>: r |] ==> P";
 by (rtac wf_asym 1);
 by (REPEAT (resolve_tac prems 1));
-val wf_anti_refl = result();
+qed "wf_anti_refl";
 
 (*transitive closure of a WF relation is WF!*)
 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)";
@@ -61,7 +61,7 @@
 by (etac tranclE 1);
 by (fast_tac HOL_cs 1);
 by (fast_tac HOL_cs 1);
-val wf_trancl = result();
+qed "wf_trancl";
 
 
 (** cut **)
@@ -72,11 +72,11 @@
     "(cut(f,r,x) = cut(g,r,x)) = (!y. <y,x>:r --> f(y)=g(y))";
 by(simp_tac (HOL_ss addsimps [expand_fun_eq]
                     setloop (split_tac [expand_if])) 1);
-val cut_cut_eq = result();
+qed "cut_cut_eq";
 
 goalw WF.thy [cut_def] "!!x. <x,a>:r ==> cut(f,r,a)(x) = f(x)";
 by(asm_simp_tac HOL_ss 1);
-val cut_apply = result();
+qed "cut_apply";
 
 
 (*** is_recfun ***)
@@ -85,7 +85,7 @@
     "!!f. [| is_recfun(r,a,H,f);  ~<b,a>:r |] ==> f(b) = (@z.True)";
 by (etac ssubst 1);
 by(asm_simp_tac HOL_ss 1);
-val is_recfun_undef = result();
+qed "is_recfun_undef";
 
 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   mp amd allE  instantiate induction hypotheses*)
@@ -110,7 +110,7 @@
 by (etac wf_induct 1);
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
-val is_recfun_equal_lemma = result();
+qed "is_recfun_equal_lemma";
 val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
 
 
@@ -124,7 +124,7 @@
 by (rtac ext 1);
 by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
                               setloop (split_tac [expand_if])) 1);
-val is_recfun_cut = result();
+qed "is_recfun_cut";
 
 (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
 
@@ -132,7 +132,7 @@
     "is_recfun(r,a,H,f) ==> is_recfun(r, a, H, the_recfun(r,a,H))";
 by (res_inst_tac [("P", "is_recfun(r,a,H)")] selectI 1);
 by (resolve_tac prems 1);
-val is_the_recfun = result();
+qed "is_the_recfun";
 
 val prems = goal WF.thy
     "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))";
@@ -146,7 +146,7 @@
             etac (mp RS ssubst), atac]);
 by (fold_tac [is_recfun_def]);
 by (asm_simp_tac (wf_super_ss addsimps[cut_apply,is_recfun_cut,cut_cut_eq]) 1);
-val unfold_the_recfun = result();
+qed "unfold_the_recfun";
 
 
 (*Beware incompleteness of unification!*)
@@ -154,13 +154,13 @@
     "[| wf(r);  trans(r);  <c,a>:r;  <c,b>:r |] \
 \    ==> the_recfun(r,a,H,c) = the_recfun(r,b,H,c)";
 by (DEPTH_SOLVE (ares_tac (prems@[is_recfun_equal,unfold_the_recfun]) 1));
-val the_recfun_equal = result();
+qed "the_recfun_equal";
 
 val prems = goal WF.thy
     "[| wf(r); trans(r); <b,a>:r |] \
 \    ==> cut(the_recfun(r,a,H),r,b) = the_recfun(r,b,H)";
 by (REPEAT (ares_tac (prems@[is_recfun_cut,unfold_the_recfun]) 1));
-val the_recfun_cut = result();
+qed "the_recfun_cut";
 
 (*** Unfolding wftrec ***)
 
@@ -170,7 +170,7 @@
 by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun),
 	    REPEAT o atac, rtac H_cong1]);
 by (asm_simp_tac (HOL_ss addsimps [cut_cut_eq,the_recfun_cut]) 1);
-val wftrec = result();
+qed "wftrec";
 
 (*Unused but perhaps interesting*)
 val prems = goal WF.thy
@@ -178,7 +178,7 @@
 \		wftrec(r,a,H) = H(a, %x.wftrec(r,x,H))";
 by (rtac (wftrec RS trans) 1);
 by (REPEAT (resolve_tac prems 1));
-val wftrec2 = result();
+qed "wftrec2";
 
 (** Removal of the premise trans(r) **)
 
@@ -188,11 +188,11 @@
 by (rtac trans_trancl 1);
 by (rtac (refl RS H_cong) 1);    (*expose the equality of cuts*)
 by (simp_tac (HOL_ss addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
-val wfrec = result();
+qed "wfrec";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
 val rew::prems = goal WF.thy
     "[| !!x. f(x)==wfrec(r,x,H);  wf(r) |] ==> f(a) = H(a, cut(%x.f(x),r,a))";
 by (rewtac rew);
 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
-val def_wfrec = result();
+qed "def_wfrec";