# HG changeset patch
# User paulson
# Date 1024415901 -7200
# Node ID 7e44aa8a276ee951818baaf441334eabbc848e31
# Parent  3732064ccbd1f22e1c391c82dfefde53d0ad3954
new lemma

diff -r 3732064ccbd1 -r 7e44aa8a276e src/ZF/WF.thy
--- 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 = 
diff -r 3732064ccbd1 -r 7e44aa8a276e src/ZF/func.thy
--- 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)