more tidying
authorpaulson
Wed May 22 19:34:01 2002 +0200 (2002-05-22)
changeset 1317485d3c0981a16
parent 13173 8f4680be79cc
child 13175 81082cfa5618
more tidying
src/ZF/Nat.thy
src/ZF/OrdQuant.thy
src/ZF/equalities.thy
src/ZF/func.thy
     1.1 --- a/src/ZF/Nat.thy	Wed May 22 18:55:47 2002 +0200
     1.2 +++ b/src/ZF/Nat.thy	Wed May 22 19:34:01 2002 +0200
     1.3 @@ -199,10 +199,10 @@
     1.4  (** nat_case **)
     1.5  
     1.6  lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
     1.7 -by (simp add: nat_case_def, blast)
     1.8 +by (simp add: nat_case_def)
     1.9  
    1.10  lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)" 
    1.11 -by (simp add: nat_case_def, blast)
    1.12 +by (simp add: nat_case_def)
    1.13  
    1.14  lemma nat_case_type [TC]:
    1.15      "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |] 
    1.16 @@ -212,10 +212,10 @@
    1.17  (** nat_case3 **)
    1.18  
    1.19  lemma nat_case3_0 [simp]: "nat_case3(a,b,0) = a"
    1.20 -by (simp add: nat_case3_def, blast)
    1.21 +by (simp add: nat_case3_def)
    1.22  
    1.23  lemma nat_case3_succ [simp]: "n\<in>nat \<Longrightarrow> nat_case3(a,b,succ(n)) = b(n)"
    1.24 -by (simp add: nat_case3_def, blast)
    1.25 +by (simp add: nat_case3_def)
    1.26  
    1.27  lemma non_nat_case3: "x\<notin>nat \<Longrightarrow> nat_case3(a,b,x) = 0"
    1.28  apply (simp add: nat_case3_def) 
     2.1 --- a/src/ZF/OrdQuant.thy	Wed May 22 18:55:47 2002 +0200
     2.2 +++ b/src/ZF/OrdQuant.thy	Wed May 22 19:34:01 2002 +0200
     2.3 @@ -60,10 +60,6 @@
     2.4  
     2.5  (** Now some very basic ZF theorems **)
     2.6  
     2.7 -(*FIXME: move to ZF.thy or even to FOL.thy??*)
     2.8 -lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
     2.9 -by blast
    2.10 -
    2.11  (*FIXME: move to Rel.thy*)
    2.12  lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    2.13  by (unfold trans_def trans_on_def, blast)
     3.1 --- a/src/ZF/equalities.thy	Wed May 22 18:55:47 2002 +0200
     3.2 +++ b/src/ZF/equalities.thy	Wed May 22 19:34:01 2002 +0200
     3.3 @@ -11,6 +11,20 @@
     3.4  
     3.5  theory equalities = pair + subset:
     3.6  
     3.7 +(*FIXME: move to ZF.thy or even to FOL.thy??*)
     3.8 +lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
     3.9 +by blast
    3.10 +
    3.11 +(*FIXME: move to ZF.thy or even to FOL.thy??*)
    3.12 +lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
    3.13 +by blast
    3.14 +
    3.15 +(*FIXME: move to upair once it's Isar format*)
    3.16 +lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
    3.17 +by blast
    3.18 +
    3.19 +lemma the_eq_0 [simp]: "(THE x. False) = 0"
    3.20 +by (blast intro: the_0)
    3.21  
    3.22  (*** converse ***)
    3.23  
    3.24 @@ -27,8 +41,7 @@
    3.25      "[| yx : converse(r);   
    3.26          !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P |]
    3.27       ==> P"
    3.28 -apply (unfold converse_def, blast) 
    3.29 -done
    3.30 +by (unfold converse_def, blast) 
    3.31  
    3.32  lemma converse_converse: "r<=Sigma(A,B) ==> converse(converse(r)) = r"
    3.33  by blast
    3.34 @@ -42,7 +55,8 @@
    3.35  lemma converse_empty [simp]: "converse(0) = 0"
    3.36  by blast
    3.37  
    3.38 -lemma converse_subset_iff: "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
    3.39 +lemma converse_subset_iff:
    3.40 +     "A <= Sigma(X,Y) ==> converse(A) <= converse(B) <-> A <= B"
    3.41  by blast
    3.42  
    3.43  
    3.44 @@ -56,8 +70,7 @@
    3.45  
    3.46  lemma domainE [elim!]:
    3.47      "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P"
    3.48 -apply (unfold domain_def, blast)
    3.49 -done
    3.50 +by (unfold domain_def, blast)
    3.51  
    3.52  lemma domain_subset: "domain(Sigma(A,B)) <= A"
    3.53  by blast
     4.1 --- a/src/ZF/func.thy	Wed May 22 18:55:47 2002 +0200
     4.2 +++ b/src/ZF/func.thy	Wed May 22 19:34:01 2002 +0200
     4.3 @@ -233,9 +233,13 @@
     4.4  lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"
     4.5  by (unfold lam_def, blast)
     4.6  
     4.7 +lemma image_function:
     4.8 +     "[| function(f);  C <= domain(f) |] ==> f``C = {f`x. x:C}";
     4.9 +by (blast dest: function_apply_equality intro: function_apply_Pair) 
    4.10 +
    4.11  lemma image_fun: "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}"
    4.12 -apply (erule eta [THEN subst])
    4.13 -apply (simp add: image_lam subset_iff)
    4.14 +apply (simp add: Pi_iff) 
    4.15 +apply (blast intro: image_function) 
    4.16  done
    4.17  
    4.18  lemma Pi_image_cons:
    4.19 @@ -323,6 +327,10 @@
    4.20  apply (blast intro!: rel_Union function_Union)
    4.21  done
    4.22  
    4.23 +lemma gen_relation_Union [rule_format]:
    4.24 +     "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(Union(F))"
    4.25 +by (simp add: relation_def) 
    4.26 +
    4.27  
    4.28  (** The Union of 2 disjoint functions is a function **)
    4.29