--- a/src/ZF/WF.thy Tue Jun 18 10:52:08 2002 +0200
+++ b/src/ZF/WF.thy Tue Jun 18 17:58:21 2002 +0200
@@ -131,6 +131,14 @@
apply (rule field_Int_square, blast)
done
+text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
+ hypothesis by removing the restriction to @{term A}.*}
+lemma wf_on_induct2:
+ "[| wf[A](r); a:A; r \<subseteq> A*A;
+ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x)
+ |] ==> P(a)"
+by (rule wf_on_induct, assumption+, blast)
+
(*fixed up for induct method*)
lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
and wf_on_induct_rule =
--- a/src/ZF/func.thy Tue Jun 18 10:52:08 2002 +0200
+++ b/src/ZF/func.thy Tue Jun 18 17:58:21 2002 +0200
@@ -22,6 +22,10 @@
lemma fun_is_function: "f: Pi(A,B) ==> function(f)"
by (simp only: Pi_iff)
+lemma function_imp_Pi:
+ "[|function(f); relation(f)|] ==> f \<in> domain(f) -> range(f)"
+by (simp add: Pi_iff relation_def, blast)
+
lemma functionI:
"[| !!x y y'. [| <x,y>:r; <x,y'>:r |] ==> y=y' |] ==> function(r)"
by (simp add: function_def, blast)