--- a/src/HOL/WF_Rel.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/WF_Rel.ML Mon Jun 22 17:26:46 1998 +0200
@@ -13,17 +13,17 @@
* "Less than" on the natural numbers
*---------------------------------------------------------------------------*)
-goalw thy [less_than_def] "wf less_than";
+Goalw [less_than_def] "wf less_than";
by (rtac (wf_pred_nat RS wf_trancl) 1);
qed "wf_less_than";
AddIffs [wf_less_than];
-goalw thy [less_than_def] "trans less_than";
+Goalw [less_than_def] "trans less_than";
by (rtac trans_trancl 1);
qed "trans_less_than";
AddIffs [trans_less_than];
-goalw thy [less_than_def, less_def] "((x,y): less_than) = (x<y)";
+Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)";
by (Simp_tac 1);
qed "less_than_iff";
AddIffs [less_than_iff];
@@ -32,7 +32,7 @@
* The inverse image into a wellfounded relation is wellfounded.
*---------------------------------------------------------------------------*)
-goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))";
+Goal "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))";
by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
by (Clarify_tac 1);
by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
@@ -43,7 +43,7 @@
qed "wf_inv_image";
AddSIs [wf_inv_image];
-goalw thy [trans_def,inv_image_def]
+Goalw [trans_def,inv_image_def]
"!!r. trans r ==> trans (inv_image r f)";
by (Simp_tac 1);
by (Blast_tac 1);
@@ -54,7 +54,7 @@
* All measures are wellfounded.
*---------------------------------------------------------------------------*)
-goalw thy [measure_def] "wf (measure f)";
+Goalw [measure_def] "wf (measure f)";
by (rtac (wf_less_than RS wf_inv_image) 1);
qed "wf_measure";
AddIffs [wf_measure];
@@ -82,7 +82,7 @@
(*---------------------------------------------------------------------------
* Transitivity of WF combinators.
*---------------------------------------------------------------------------*)
-goalw thy [trans_def, lex_prod_def]
+Goalw [trans_def, lex_prod_def]
"!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
by (Simp_tac 1);
by (Blast_tac 1);
@@ -93,14 +93,14 @@
(*---------------------------------------------------------------------------
* Wellfoundedness of proper subset on finite sets.
*---------------------------------------------------------------------------*)
-goalw thy [finite_psubset_def] "wf(finite_psubset)";
+Goalw [finite_psubset_def] "wf(finite_psubset)";
by (rtac (wf_measure RS wf_subset) 1);
by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
symmetric less_def])1);
by (fast_tac (claset() addSIs [psubset_card]) 1);
qed "wf_finite_psubset";
-goalw thy [finite_psubset_def, trans_def] "trans finite_psubset";
+Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
by (simp_tac (simpset() addsimps [psubset_def]) 1);
by (Blast_tac 1);
qed "trans_finite_psubset";
@@ -110,7 +110,7 @@
* Cannot go into WF because it needs Finite
*---------------------------------------------------------------------------*)
-goal thy "!!r. finite r ==> acyclic r --> wf r";
+Goal "!!r. finite r ==> acyclic r --> wf r";
by (etac finite_induct 1);
by (Blast_tac 1);
by (split_all_tac 1);
@@ -122,7 +122,7 @@
etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
etac (acyclic_converse RS iffD2) 1]);
-goal thy "!!r. finite r ==> wf r = acyclic r";
+Goal "!!r. finite r ==> wf r = acyclic r";
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
qed "wf_iff_acyclic_if_finite";
@@ -131,7 +131,7 @@
* A relation is wellfounded iff it has no infinite descending chain
*---------------------------------------------------------------------------*)
-goalw thy [wf_eq_minimal RS eq_reflection]
+Goalw [wf_eq_minimal RS eq_reflection]
"wf r = (~(? f. !i. (f(Suc i),f i) : r))";
by (rtac iffI 1);
by (rtac notI 1);