# HG changeset patch
# User paulson
# Date 1022088841 -7200
# Node ID 85d3c0981a1678157f6bf58e4828261a6725d198
# Parent  8f4680be79cc22b3a1e005fd8d1b8b68fe99742f
more tidying

diff -r 8f4680be79cc -r 85d3c0981a16 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Wed May 22 18:55:47 2002 +0200
+++ b/src/ZF/Nat.thy	Wed May 22 19:34:01 2002 +0200
@@ -199,10 +199,10 @@
 (** nat_case **)
 
 lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
-by (simp add: nat_case_def, blast)
+by (simp add: nat_case_def)
 
 lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)" 
-by (simp add: nat_case_def, blast)
+by (simp add: nat_case_def)
 
 lemma nat_case_type [TC]:
     "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |] 
@@ -212,10 +212,10 @@
 (** nat_case3 **)
 
 lemma nat_case3_0 [simp]: "nat_case3(a,b,0) = a"
-by (simp add: nat_case3_def, blast)
+by (simp add: nat_case3_def)
 
 lemma nat_case3_succ [simp]: "n\<in>nat \<Longrightarrow> nat_case3(a,b,succ(n)) = b(n)"
-by (simp add: nat_case3_def, blast)
+by (simp add: nat_case3_def)
 
 lemma non_nat_case3: "x\<notin>nat \<Longrightarrow> nat_case3(a,b,x) = 0"
 apply (simp add: nat_case3_def) 
diff -r 8f4680be79cc -r 85d3c0981a16 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Wed May 22 18:55:47 2002 +0200
+++ b/src/ZF/OrdQuant.thy	Wed May 22 19:34:01 2002 +0200
@@ -60,10 +60,6 @@
 
 (** Now some very basic ZF theorems **)
 
-(*FIXME: move to ZF.thy or even to FOL.thy??*)
-lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
-by blast
-
 (*FIXME: move to Rel.thy*)
 lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
 by (unfold trans_def trans_on_def, blast)
diff -r 8f4680be79cc -r 85d3c0981a16 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Wed May 22 18:55:47 2002 +0200
+++ b/src/ZF/equalities.thy	Wed May 22 19:34:01 2002 +0200
@@ -11,6 +11,20 @@
 
 theory equalities = pair + subset:
 
+(*FIXME: move to ZF.thy or even to FOL.thy??*)
+lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
+by blast
+
+(*FIXME: move to ZF.thy or even to FOL.thy??*)
+lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
+by blast
+
+(*FIXME: move to upair once it's Isar format*)
+lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
+by blast
+
+lemma the_eq_0 [simp]: "(THE x. False) = 0"
+by (blast intro: the_0)
 
 (*** converse ***)
 
@@ -27,8 +41,7 @@
     "[| yx : converse(r);   
         !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P |]
      ==> P"
-apply (unfold converse_def, blast) 
-done
+by (unfold converse_def, blast) 
 
 lemma converse_converse: "r<=Sigma(A,B) ==> converse(converse(r)) = r"
 by blast
@@ -42,7 +55,8 @@
 lemma converse_empty [simp]: "converse(0) = 0"
 by blast
 
-lemma converse_subset_iff: "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
+lemma converse_subset_iff:
+     "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
 by blast
 
 
@@ -56,8 +70,7 @@
 
 lemma domainE [elim!]:
     "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
-apply (unfold domain_def, blast)
-done
+by (unfold domain_def, blast)
 
 lemma domain_subset: "domain(Sigma(A,B)) <= A"
 by blast
diff -r 8f4680be79cc -r 85d3c0981a16 src/ZF/func.thy
--- a/src/ZF/func.thy	Wed May 22 18:55:47 2002 +0200
+++ b/src/ZF/func.thy	Wed May 22 19:34:01 2002 +0200
@@ -233,9 +233,13 @@
 lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"
 by (unfold lam_def, blast)
 
+lemma image_function:
+     "[| function(f);  C <= domain(f) |] ==> f``C = {f`x. x:C}";
+by (blast dest: function_apply_equality intro: function_apply_Pair) 
+
 lemma image_fun: "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}"
-apply (erule eta [THEN subst])
-apply (simp add: image_lam subset_iff)
+apply (simp add: Pi_iff) 
+apply (blast intro: image_function) 
 done
 
 lemma Pi_image_cons:
@@ -323,6 +327,10 @@
 apply (blast intro!: rel_Union function_Union)
 done
 
+lemma gen_relation_Union [rule_format]:
+     "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(Union(F))"
+by (simp add: relation_def) 
+
 
 (** The Union of 2 disjoint functions is a function **)