--- 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";