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.
```