--- 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";
--- 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))"
--- 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 ***)
--- 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
--- 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