src/ZF/OrderArith.ML

--- a/src/ZF/OrderArith.ML	Wed Dec 07 12:34:47 1994 +0100
+++ b/src/ZF/OrderArith.ML	Wed Dec 07 13:12:04 1994 +0100
@@ -16,22 +16,22 @@
 goalw OrderArith.thy [radd_def] 
     "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B";
 by (fast_tac sum_cs 1);
-val radd_Inl_Inr_iff = result();
+qed "radd_Inl_Inr_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  <a',a>:r & a':A & a:A";
 by (fast_tac sum_cs 1);
-val radd_Inl_iff = result();
+qed "radd_Inl_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  <b',b>:s & b':B & b:B";
 by (fast_tac sum_cs 1);
-val radd_Inr_iff = result();
+qed "radd_Inr_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False";
 by (fast_tac sum_cs 1);
-val radd_Inr_Inl_iff = result();
+qed "radd_Inr_Inl_iff";
 
 (** Elimination Rule **)
 
@@ -50,13 +50,13 @@
 by (EVERY (map (fn prem => 
 		EVERY1 [rtac prem, assume_tac, REPEAT o fast_tac sum_cs])
 	   prems));
-val raddE = result();
+qed "raddE";
 
 (** Type checking **)
 
 goalw OrderArith.thy [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)";
 by (rtac Collect_subset 1);
-val radd_type = result();
+qed "radd_type";
 
 val field_radd = standard (radd_type RS field_rel_subset);
 
@@ -72,7 +72,7 @@
     "!!r s. [| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
 by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE));
 by (ALLGOALS (asm_simp_tac radd_ss));
-val linear_radd = result();
+qed "linear_radd";
 
 
 (** Well-foundedness **)
@@ -95,14 +95,14 @@
 by (etac (bspec RS mp) 1);
 by (fast_tac sum_cs 1);
 by (best_tac (sum_cs addSEs [raddE]) 1);
-val wf_on_radd = result();
+qed "wf_on_radd";
 
 goal OrderArith.thy
      "!!r s. [| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
 by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
 by (rtac (field_radd RSN (2, wf_on_subset_A)) 1);
 by (REPEAT (ares_tac [wf_on_radd] 1));
-val wf_radd = result();
+qed "wf_radd";
 
 goal OrderArith.thy 
     "!!r s. [| well_ord(A,r);  well_ord(B,s) |] ==> \
@@ -111,7 +111,7 @@
 by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_radd]) 1);
 by (asm_full_simp_tac 
     (ZF_ss addsimps [well_ord_def, tot_ord_def, linear_radd]) 1);
-val well_ord_radd = result();
+qed "well_ord_radd";
 
 
 (**** Multiplication of relations -- lexicographic product ****)
@@ -123,7 +123,7 @@
 \           (<a',a>: r  & a':A & a:A & b': B & b: B) | 	\
 \           (<b',b>: s  & a'=a & a:A & b': B & b: B)";
 by (fast_tac ZF_cs 1);
-val rmult_iff = result();
+qed "rmult_iff";
 
 val major::prems = goal OrderArith.thy
     "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);		\
@@ -132,13 +132,13 @@
 \    |] ==> Q";
 by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1);
 by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1));
-val rmultE = result();
+qed "rmultE";
 
 (** Type checking **)
 
 goalw OrderArith.thy [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)";
 by (rtac Collect_subset 1);
-val rmult_type = result();
+qed "rmult_type";
 
 val field_rmult = standard (rmult_type RS field_rel_subset);
 
@@ -152,7 +152,7 @@
 by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1);
 by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4);
 by (REPEAT_SOME (fast_tac ZF_cs));
-val linear_rmult = result();
+qed "linear_rmult";
 
 
 (** Well-foundedness **)
@@ -170,7 +170,7 @@
 by (etac (bspec RS mp) 1);
 by (fast_tac ZF_cs 1);
 by (best_tac (ZF_cs addSEs [rmultE]) 1);
-val wf_on_rmult = result();
+qed "wf_on_rmult";
 
 
 goal OrderArith.thy
@@ -178,7 +178,7 @@
 by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1);
 by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1);
 by (REPEAT (ares_tac [wf_on_rmult] 1));
-val wf_rmult = result();
+qed "wf_rmult";
 
 goal OrderArith.thy 
     "!!r s. [| well_ord(A,r);  well_ord(B,s) |] ==> \
@@ -187,7 +187,7 @@
 by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_rmult]) 1);
 by (asm_full_simp_tac 
     (ZF_ss addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1);
-val well_ord_rmult = result();
+qed "well_ord_rmult";
 
 
 (**** Inverse image of a relation ****)
@@ -197,13 +197,13 @@
 goalw OrderArith.thy [rvimage_def] 
     "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
 by (fast_tac ZF_cs 1);
-val rvimage_iff = result();
+qed "rvimage_iff";
 
 (** Type checking **)
 
 goalw OrderArith.thy [rvimage_def] "rvimage(A,f,r) <= A*A";
 by (rtac Collect_subset 1);
-val rvimage_type = result();
+qed "rvimage_type";
 
 val field_rvimage = standard (rvimage_type RS field_rel_subset);
 
@@ -218,7 +218,7 @@
 by (cut_facts_tac [finj] 1);
 by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
 by (REPEAT_SOME (fast_tac (ZF_cs addSIs [apply_type])));
-val linear_rvimage = result();
+qed "linear_rvimage";
 
 
 (** Well-foundedness **)
@@ -231,7 +231,7 @@
 by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
 by (fast_tac (ZF_cs addSIs [apply_type]) 1);
 by (best_tac (ZF_cs addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1);
-val wf_on_rvimage = result();
+qed "wf_on_rvimage";
 
 goal OrderArith.thy 
     "!!r. [| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
@@ -239,4 +239,4 @@
 by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
 by (fast_tac (ZF_cs addSIs [wf_on_rvimage, inj_is_fun]) 1);
 by (fast_tac (ZF_cs addSIs [linear_rvimage]) 1);
-val well_ord_rvimage = result();
+qed "well_ord_rvimage";