--- a/src/HOL/WF_Rel.ML Tue Jul 25 01:27:36 2000 +0200
+++ b/src/HOL/WF_Rel.ML Tue Jul 25 09:48:39 2000 +0200
@@ -208,3 +208,19 @@
by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
qed "weak_decr_stable";
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of same_fst
+ *---------------------------------------------------------------------------*)
+
+val prems = goalw thy [same_fst_def]
+ "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
+by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
+by(strip_tac 1);
+by(rename_tac "a b" 1);
+by(case_tac "wf(R a)" 1);
+ by (eres_inst_tac [("a","b")] wf_induct 1);
+ by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
+ by(Blast_tac 1);
+by(blast_tac (claset() addIs prems) 1);
+qed "wf_same_fstI";