src/ZF/pair.thy
changeset 46841 49b91b716cbe
parent 46821 ff6b0c1087f2
child 46953 2b6e55924af3
     1.1 --- a/src/ZF/pair.thy	Tue Mar 06 17:01:37 2012 +0000
     1.2 +++ b/src/ZF/pair.thy	Thu Mar 08 16:43:29 2012 +0000
     1.3 @@ -58,18 +58,22 @@
     1.4  declare sym [THEN Pair_neq_0, elim!]
     1.5  
     1.6  lemma Pair_neq_fst: "<a,b>=a ==> P"
     1.7 -apply (unfold Pair_def)
     1.8 -apply (rule consI1 [THEN mem_asym, THEN FalseE])
     1.9 -apply (erule subst)
    1.10 -apply (rule consI1)
    1.11 -done
    1.12 +proof (unfold Pair_def)
    1.13 +  assume eq: "{{a, a}, {a, b}} = a"
    1.14 +  have  "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1)
    1.15 +  hence "{a, a} \<in> a" by (simp add: eq)
    1.16 +  moreover have "a \<in> {a, a}" by (rule consI1)
    1.17 +  ultimately show "P" by (rule mem_asym) 
    1.18 +qed
    1.19  
    1.20  lemma Pair_neq_snd: "<a,b>=b ==> P"
    1.21 -apply (unfold Pair_def)
    1.22 -apply (rule consI1 [THEN consI2, THEN mem_asym, THEN FalseE])
    1.23 -apply (erule subst)
    1.24 -apply (rule consI1 [THEN consI2])
    1.25 -done
    1.26 +proof (unfold Pair_def)
    1.27 +  assume eq: "{{a, a}, {a, b}} = b"
    1.28 +  have  "{a, b} \<in> {{a, a}, {a, b}}" by blast
    1.29 +  hence "{a, b} \<in> b" by (simp add: eq)
    1.30 +  moreover have "b \<in> {a, b}" by blast
    1.31 +  ultimately show "P" by (rule mem_asym) 
    1.32 +qed
    1.33  
    1.34  
    1.35  subsection{*Sigma: Disjoint Union of a Family of Sets*}
    1.36 @@ -145,15 +149,12 @@
    1.37      "[|  p:Sigma(A,B);    
    1.38           !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>)  
    1.39       |] ==> split(%x y. c(x,y), p) \<in> C(p)"
    1.40 -apply (erule SigmaE, auto) 
    1.41 -done
    1.42 +by (erule SigmaE, auto) 
    1.43  
    1.44  lemma expand_split: 
    1.45    "u: A*B ==>    
    1.46          R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))"
    1.47 -apply (simp add: split_def)
    1.48 -apply auto
    1.49 -done
    1.50 +by (auto simp add: split_def)
    1.51  
    1.52  
    1.53  subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
    1.54 @@ -165,9 +166,7 @@
    1.55      "[| split(R,z);  z:Sigma(A,B);                       
    1.56          !!x y. [| z = <x,y>;  R(x,y) |] ==> P            
    1.57       |] ==> P"
    1.58 -apply (simp add: split_def)
    1.59 -apply (erule SigmaE, force) 
    1.60 -done
    1.61 +by (auto simp add: split_def)
    1.62  
    1.63  lemma splitD: "split(R,<a,b>) ==> R(a,b)"
    1.64  by (simp add: split_def)