src/ZF/WF.ML
changeset 760 f0200e91b272
parent 494 3686157a5a51
child 782 200a16083201
--- a/src/ZF/WF.ML	Wed Dec 07 12:34:47 1994 +0100
+++ b/src/ZF/WF.ML	Wed Dec 07 13:12:04 1994 +0100
@@ -26,23 +26,23 @@
 
 goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
 by (fast_tac ZF_cs 1);
-val wf_imp_wf_on = result();
+qed "wf_imp_wf_on";
 
 goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
 by (fast_tac ZF_cs 1);
-val wf_on_field_imp_wf = result();
+qed "wf_on_field_imp_wf";
 
 goal WF.thy "wf(r) <-> wf[field(r)](r)";
 by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
-val wf_iff_wf_on_field = result();
+qed "wf_iff_wf_on_field";
 
 goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r);  B<=A |] ==> wf[B](r)";
 by (fast_tac ZF_cs 1);
-val wf_on_subset_A = result();
+qed "wf_on_subset_A";
 
 goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r);  s<=r |] ==> wf[A](s)";
 by (fast_tac ZF_cs 1);
-val wf_on_subset_r = result();
+qed "wf_on_subset_r";
 
 (** Introduction rules for wf_on **)
 
@@ -53,7 +53,7 @@
 by (rtac (equals0I RS disjCI RS allI) 1);
 by (res_inst_tac [ ("Z", "Z") ] prem 1);
 by (ALLGOALS (fast_tac ZF_cs));
-val wf_onI = result();
+qed "wf_onI";
 
 (*If r allows well-founded induction over A then wf[A](r)
   Premise is equivalent to 
@@ -67,7 +67,7 @@
 by (contr_tac 3);
 by (fast_tac ZF_cs 2);
 by (fast_tac ZF_cs 1);
-val wf_onI2 = result();
+qed "wf_onI2";
 
 
 (** Well-founded Induction **)
@@ -84,7 +84,7 @@
 by (etac bexE 1);
 by (dtac minor 1);
 by (fast_tac ZF_cs 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 = 
@@ -102,11 +102,11 @@
 by (rtac impI 1);
 by (eresolve_tac prems 1);
 by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1);
-val wf_induct2 = result();
+qed "wf_induct2";
 
 goal ZF.thy "!!r A. field(r Int A*A) <= A";
 by (fast_tac ZF_cs 1);
-val field_Int_square = result();
+qed "field_Int_square";
 
 val wfr::amem::prems = goalw WF.thy [wf_on_def]
     "[| wf[A](r);  a:A;  					\
@@ -115,7 +115,7 @@
 by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
 by (REPEAT (ares_tac prems 1));
 by (fast_tac ZF_cs 1);
-val wf_on_induct = result();
+qed "wf_on_induct";
 
 fun wf_on_ind_tac a prems i = 
     EVERY [res_inst_tac [("a",a)] wf_on_induct i,
@@ -130,7 +130,7 @@
 \    ==>  wf(r)";
 by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
 by (REPEAT (ares_tac [indhyp] 1));
-val wfI = result();
+qed "wfI";
 
 
 (*** Properties of well-founded relations ***)
@@ -138,26 +138,26 @@
 goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
 by (wf_ind_tac "a" [] 1);
 by (fast_tac ZF_cs 1);
-val wf_not_refl = result();
+qed "wf_not_refl";
 
 goal WF.thy "!!r. [| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
 by (wf_ind_tac "a" [] 2);
 by (fast_tac ZF_cs 2);
 by (fast_tac FOL_cs 1);
-val wf_asym = result();
+qed "wf_asym";
 
 goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
 by (wf_on_ind_tac "a" [] 1);
 by (fast_tac ZF_cs 1);
-val wf_on_not_refl = result();
+qed "wf_on_not_refl";
 
 goal WF.thy "!!r. [| wf[A](r);  <a,b>:r;  <b,a>:r;  a:A;  b:A |] ==> P";
 by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
 by (wf_on_ind_tac "a" [] 2);
 by (fast_tac ZF_cs 2);
 by (fast_tac ZF_cs 1);
-val wf_on_asym = result();
+qed "wf_on_asym";
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
@@ -168,7 +168,7 @@
 by (wf_on_ind_tac "a" [] 2);
 by (fast_tac ZF_cs 2);
 by (fast_tac ZF_cs 1);
-val wf_on_chain3 = result();
+qed "wf_on_chain3";
 
 
 (*retains the universal formula for later use!*)
@@ -187,14 +187,14 @@
 by (cut_facts_tac [subs] 1);
 (*astar_tac is slightly faster*)
 by (best_tac ZF_cs 1);
-val wf_on_trancl = result();
+qed "wf_on_trancl";
 
 goal WF.thy "!!r. wf(r) ==> wf(r^+)";
 by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
 by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1);
 by (etac wf_on_trancl 1);
 by (fast_tac ZF_cs 1);
-val wf_trancl = result();
+qed "wf_trancl";
 
 
 
@@ -210,13 +210,13 @@
 by (rtac (major RS ssubst) 1);
 by (rtac (lamI RS rangeI RS lam_type) 1);
 by (assume_tac 1);
-val is_recfun_type = result();
+qed "is_recfun_type";
 
 val [isrec,rel] = goalw WF.thy [is_recfun_def]
     "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))";
 by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1);
 by (rtac (rel RS underI RS beta) 1);
-val apply_recfun = result();
+qed "apply_recfun";
 
 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
   spec RS mp  instantiates induction hypotheses*)
@@ -237,7 +237,7 @@
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (rewtac restrict_def);
 by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 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);
 
 val prems as [wfr,transr,recf,recg,_] = goal WF.thy
@@ -250,7 +250,7 @@
 by (ALLGOALS
     (asm_simp_tac (wf_super_ss addsimps
 		   [ [wfr,transr,recf,recg] MRS is_recfun_equal ])));
-val is_recfun_cut = result();
+qed "is_recfun_cut";
 
 (*** Main Existence Lemma ***)
 
@@ -260,7 +260,7 @@
 by (rtac fun_extension 1);
 by (REPEAT (ares_tac [is_recfun_equal] 1
      ORELSE eresolve_tac [is_recfun_type,underD] 1));
-val is_recfun_functional = result();
+qed "is_recfun_functional";
 
 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
 val prems = goalw WF.thy [the_recfun_def]
@@ -268,7 +268,7 @@
 \    ==> is_recfun(r, a, H, the_recfun(r,a,H))";
 by (rtac (ex1I RS theI) 1);
 by (REPEAT (ares_tac (prems@[is_recfun_functional]) 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))";
@@ -285,7 +285,7 @@
 by (ALLGOALS
     (asm_simp_tac
      (wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut])));
-val unfold_the_recfun = result();
+qed "unfold_the_recfun";
 
 
 (*** Unfolding wftrec ***)
@@ -294,7 +294,7 @@
     "[| wf(r);  trans(r);  <b,a>:r |] ==> \
 \    restrict(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";
 
 (*NOT SUITABLE FOR REWRITING since it is recursive!*)
 goalw WF.thy [wftrec_def]
@@ -303,7 +303,7 @@
 by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
 by (ALLGOALS (asm_simp_tac
 	(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
-val wftrec = result();
+qed "wftrec";
 
 (** Removal of the premise trans(r) **)
 
@@ -315,7 +315,7 @@
 by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
 by (etac r_into_trancl 1);
 by (rtac subset_refl 1);
-val wfrec = result();
+qed "wfrec";
 
 (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
 val rew::prems = goal WF.thy
@@ -323,7 +323,7 @@
 \    h(a) = H(a, lam x: r-``{a}. h(x))";
 by (rewtac rew);
 by (REPEAT (resolve_tac (prems@[wfrec]) 1));
-val def_wfrec = result();
+qed "def_wfrec";
 
 val prems = goal WF.thy
     "[| wf(r);  a:A;  field(r)<=A;  \
@@ -333,7 +333,7 @@
 by (rtac (wfrec RS ssubst) 4);
 by (REPEAT (ares_tac (prems@[lam_type]) 1
      ORELSE eresolve_tac [spec RS mp, underD] 1));
-val wfrec_type = result();
+qed "wfrec_type";
 
 
 goalw WF.thy [wf_on_def, wfrec_on_def]
@@ -341,5 +341,5 @@
 \        wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))";
 by (etac (wfrec RS trans) 1);
 by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1);
-val wfrec_on = result();
+qed "wfrec_on";