# HG changeset patch
# User paulson
# Date 1025080006 -7200
# Node ID ae66c22ed52ebff3de8ea773f9eb79d4c5233c1f
# Parent  e3c289f0724b7d43722255a2a9e982f52df11b08
new theorems

diff -r e3c289f0724b -r ae66c22ed52e src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Wed Jun 26 10:25:36 2002 +0200
+++ b/src/ZF/Trancl.thy	Wed Jun 26 10:26:46 2002 +0200
@@ -84,12 +84,15 @@
 lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
 by (unfold trans_def trans_on_def, blast)
 
+lemma trans_on_imp_trans: "[|trans[A](r); r <= A*A|] ==> trans(r)";
+by (simp add: trans_on_def trans_def, blast)
+
+
 subsection{*Transitive closure of a relation*}
 
 lemma rtrancl_bnd_mono:
      "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))"
-apply (rule bnd_monoI, blast+)
-done
+by (rule bnd_monoI, blast+)
 
 lemma rtrancl_mono: "r<=s ==> r^* <= s^*"
 apply (unfold rtrancl_def)
@@ -107,6 +110,11 @@
 (*  r^* <= field(r) * field(r)  *)
 lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard]
 
+lemma relation_rtrancl: "relation(r^*)"
+apply (simp add: relation_def) 
+apply (blast dest: rtrancl_type [THEN subsetD]) 
+done
+
 (*Reflexivity of rtrancl*)
 lemma rtrancl_refl: "[| a: field(r) |] ==> <a,a> : r^*"
 apply (rule rtrancl_unfold [THEN ssubst])
@@ -125,8 +133,8 @@
 by (rule rtrancl_refl [THEN rtrancl_into_rtrancl], blast+)
 
 (*The premise ensures that r consists entirely of pairs*)
-lemma r_subset_rtrancl: "r <= Sigma(A,B) ==> r <= r^*"
-by (blast intro: r_into_rtrancl)
+lemma r_subset_rtrancl: "relation(r) ==> r <= r^*"
+by (simp add: relation_def, blast intro: r_into_rtrancl)
 
 lemma rtrancl_field: "field(r^*) = field(r)"
 by (blast intro: r_into_rtrancl dest!: rtrancl_type [THEN subsetD])
@@ -139,8 +147,7 @@
       !!x. x: field(r) ==> P(<x,x>);  
       !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |]  ==>  P(<x,z>) |]  
    ==>  P(<a,b>)"
-apply (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast) 
-done
+by (erule def_induct [OF rtrancl_def rtrancl_bnd_mono], blast) 
 
 (*nice induction rule.
   Tried adding the typing hypotheses y,z:field(r), but these
@@ -207,8 +214,9 @@
 done
 
 (*The premise ensures that r consists entirely of pairs*)
-lemma r_subset_trancl: "r <= Sigma(A,B) ==> r <= r^+"
-by (blast intro: r_into_trancl)
+lemma r_subset_trancl: "relation(r) ==> r <= r^+"
+by (simp add: relation_def, blast intro: r_into_trancl)
+
 
 (*intro rule by definition: from r^* and r  *)
 lemma rtrancl_into_trancl1: "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+"
@@ -257,12 +265,25 @@
 apply (blast elim: rtrancl_type [THEN subsetD, THEN SigmaE2])
 done
 
+lemma relation_trancl: "relation(r^+)"
+apply (simp add: relation_def) 
+apply (blast dest: trancl_type [THEN subsetD]) 
+done
+
 lemma trancl_subset_times: "r \<subseteq> A * A ==> r^+ \<subseteq> A * A"
 by (insert trancl_type [of r], blast)
 
 lemma trancl_mono: "r<=s ==> r^+ <= s^+"
 by (unfold trancl_def, intro comp_mono rtrancl_mono)
 
+lemma trancl_eq_r: "[|relation(r); trans(r)|] ==> r^+ = r"
+apply (rule equalityI)
+ prefer 2 apply (erule r_subset_trancl, clarify) 
+apply (frule trancl_type [THEN subsetD], clarify) 
+apply (erule trancl_induct, assumption)
+apply (blast dest: transD) 
+done
+
 
 (** Suggested by Sidi Ould Ehmety **)
 
@@ -285,7 +306,7 @@
 done
 
 lemma rtrancl_Un_rtrancl:
-     "[| r<= Sigma(A,B); s<=Sigma(C,D) |] ==> (r^* Un s^*)^* = (r Un s)^*"
+     "[| relation(r); relation(s) |] ==> (r^* Un s^*)^* = (r Un s)^*"
 apply (rule rtrancl_subset)
 apply (blast dest: r_subset_rtrancl)
 apply (blast intro: rtrancl_mono [THEN subsetD])
@@ -392,7 +413,6 @@
 val trancl_mono = thm "trancl_mono";
 val rtrancl_idemp = thm "rtrancl_idemp";
 val rtrancl_subset = thm "rtrancl_subset";
-val rtrancl_Un_rtrancl = thm "rtrancl_Un_rtrancl";
 val rtrancl_converseD = thm "rtrancl_converseD";
 val rtrancl_converseI = thm "rtrancl_converseI";
 val rtrancl_converse = thm "rtrancl_converse";
diff -r e3c289f0724b -r ae66c22ed52e src/ZF/WF.thy
--- a/src/ZF/WF.thy	Wed Jun 26 10:25:36 2002 +0200
+++ b/src/ZF/WF.thy	Wed Jun 26 10:26:46 2002 +0200
@@ -54,6 +54,9 @@
 apply blast
 done
 
+lemma wf_on_imp_wf: "[|wf[A](r); r <= A*A|] ==> wf(r)";
+by (simp add: wf_on_def subset_Int_iff)
+
 lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
 by (unfold wf_def wf_on_def, fast)
 
@@ -273,14 +276,17 @@
      "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
 by (blast intro: fun_extension is_recfun_type is_recfun_equal)
 
+lemma the_recfun_eq:
+    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |] ==> the_recfun(r,a,H) = f"
+apply (unfold the_recfun_def)
+apply (blast intro: is_recfun_functional)
+done
+
 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
 lemma is_the_recfun:
     "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]
      ==> is_recfun(r, a, H, the_recfun(r,a,H))"
-apply (unfold the_recfun_def)
-apply (rule ex1I [THEN theI], assumption)
-apply (blast intro: is_recfun_functional)
-done
+by (simp add: the_recfun_eq)
 
 lemma unfold_the_recfun:
      "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"
diff -r e3c289f0724b -r ae66c22ed52e src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Wed Jun 26 10:25:36 2002 +0200
+++ b/src/ZF/equalities.thy	Wed Jun 26 10:26:46 2002 +0200
@@ -126,8 +126,7 @@
      "[| a : field(r);   
          !!x. <a,x>: r ==> P;   
          !!x. <x,a>: r ==> P        |] ==> P"
-apply (unfold field_def, blast)
-done
+by (unfold field_def, blast)
 
 lemma field_subset: "field(A*B) <= A Un B"
 by blast
@@ -148,6 +147,9 @@
 lemma field_times_field: "r <= Sigma(A,B) ==> r <= field(r)*field(r)"
 by blast
 
+lemma relation_field_times_field: "relation(r) ==> r <= field(r)*field(r)"
+by (simp add: relation_def, blast) 
+
 
 (*** Image of a set under a function/relation ***)
 
diff -r e3c289f0724b -r ae66c22ed52e src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Wed Jun 26 10:25:36 2002 +0200
+++ b/src/ZF/ex/Commutation.thy	Wed Jun 26 10:26:46 2002 +0200
@@ -94,8 +94,8 @@
 done
 
 lemma confluent_Un: 
- "[| confluent(r); confluent(s); commute(r^*, s^*);  
-     r \<subseteq> Sigma(A,B); s \<subseteq> Sigma(C,D) |] ==> confluent(r Un s)"
+ "[| confluent(r); confluent(s); commute(r^*, s^*); 
+     relation(r); relation(s) |] ==> confluent(r Un s)"
 apply (unfold confluent_def)
 apply (rule rtrancl_Un_rtrancl [THEN subst])
 apply auto
diff -r e3c289f0724b -r ae66c22ed52e src/ZF/func.thy
--- a/src/ZF/func.thy	Wed Jun 26 10:25:36 2002 +0200
+++ b/src/ZF/func.thy	Wed Jun 26 10:26:46 2002 +0200
@@ -8,6 +8,9 @@
 
 theory func = equalities:
 
+lemma subset_Sigma_imp_relation: "r <= Sigma(A,B) ==> relation(r)"
+by (simp add: relation_def, blast)
+
 lemma relation_converse_converse [simp]:
      "relation(r) ==> converse(converse(r)) = r"
 by (simp add: relation_def, blast) 
@@ -293,12 +296,6 @@
 lemma restrict_iff: "z \<in> restrict(r,A) \<longleftrightarrow> z \<in> r & (\<exists>x\<in>A. \<exists>y. z = \<langle>x, y\<rangle>)"
 by (simp add: restrict_def) 
 
-lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A Int C"
-apply (unfold restrict_def lam_def)
-apply (rule equalityI)
-apply (auto simp add: domain_iff)
-done
-
 lemma restrict_restrict [simp]:
      "restrict(restrict(r,A),B) = restrict(r, A Int B)"
 by (unfold restrict_def, blast)
@@ -308,9 +305,21 @@
 apply (auto simp add: domain_def)
 done
 
-lemma restrict_idem [simp]: "f <= Sigma(A,B) ==> restrict(f,A) = f"
+lemma restrict_idem: "f <= Sigma(A,B) ==> restrict(f,A) = f"
 by (simp add: restrict_def, blast)
 
+
+(*converse probably holds too*)
+lemma domain_restrict_idem:
+     "[| domain(r) <= A; relation(r) |] ==> restrict(r,A) = r"
+by (simp add: restrict_def relation_def, blast)
+
+lemma domain_restrict_lam [simp]: "domain(restrict(Lambda(A,f),C)) = A Int C"
+apply (unfold restrict_def lam_def)
+apply (rule equalityI)
+apply (auto simp add: domain_iff)
+done
+
 lemma restrict_if [simp]: "restrict(f,A) ` a = (if a : A then f`a else 0)"
 by (simp add: restrict apply_0)
 
@@ -321,7 +330,7 @@
 lemma fun_cons_restrict_eq:
      "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))"
 apply (rule equalityI)
-prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD])
+ prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD])
 apply (auto dest!: Pi_memberD simp add: restrict_def lam_def)
 done