src/HOL/ex/set.thy
changeset 15488 7c638a46dcbb
parent 15481 fc075ae929e4
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/ex/set.thy	Wed Feb 02 18:06:00 2005 +0100
     1.2 +++ b/src/HOL/ex/set.thy	Wed Feb 02 18:06:25 2005 +0100
     1.3 @@ -103,21 +103,18 @@
     1.4  theorem Schroeder_Bernstein:
     1.5    "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> 'a)
     1.6      \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
     1.7 -  apply (rule decomposition [THEN exE])
     1.8 -  apply (rule exI)
     1.9 +  apply (rule decomposition [where f=f and g=g, THEN exE])
    1.10 +  apply (rule_tac x = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI) 
    1.11 +    --{*The term above can be synthesized by a sufficiently detailed proof.*}
    1.12    apply (rule bij_if_then_else)
    1.13       apply (rule_tac [4] refl)
    1.14      apply (rule_tac [2] inj_on_inv)
    1.15      apply (erule subset_inj_on [OF _ subset_UNIV])
    1.16 -   txt {* Tricky variable instantiations! *}
    1.17 -   apply (erule ssubst, simplesubst double_complement)
    1.18 -   apply (rule subsetI, erule imageE, erule ssubst, rule rangeI)
    1.19 -  apply (erule ssubst, simplesubst double_complement, erule inv_image_comp [symmetric])
    1.20 +   apply blast
    1.21 +  apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])
    1.22    done
    1.23  
    1.24  
    1.25 -subsection {* Set variable instantiation examples *}
    1.26 -
    1.27  text {*
    1.28    From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
    1.29    293-314.