22 every function from $\alpha$ to its powerset, some subset is outside |
22 every function from $\alpha$ to its powerset, some subset is outside |
23 its range. The Isabelle/Isar proofs below uses HOL's set theory, |
23 its range. The Isabelle/Isar proofs below uses HOL's set theory, |
24 with the type $\alpha \ap \idt{set}$ and the operator |
24 with the type $\alpha \ap \idt{set}$ and the operator |
25 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *} |
25 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *} |
26 |
26 |
27 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
27 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
28 proof |
28 proof |
29 let ?S = "{x. x ~: f x}" |
29 let ?S = "{x. x \<notin> f x}" |
30 show "?S ~: range f" |
30 show "?S \<notin> range f" |
31 proof |
31 proof |
32 assume "?S : range f" |
32 assume "?S \<in> range f" |
33 then obtain y where "?S = f y" .. |
33 then obtain y where "?S = f y" .. |
34 then show False |
34 then show False |
35 proof (rule equalityCE) |
35 proof (rule equalityCE) |
36 assume "y : f y" |
36 assume "y \<in> f y" |
37 assume "y : ?S" then have "y ~: f y" .. |
37 assume "y \<in> ?S" |
|
38 then have "y \<notin> f y" .. |
38 with `y : f y` show ?thesis by contradiction |
39 with `y : f y` show ?thesis by contradiction |
39 next |
40 next |
40 assume "y ~: ?S" |
41 assume "y \<notin> ?S" |
41 assume "y ~: f y" then have "y : ?S" .. |
42 assume "y \<notin> f y" |
42 with `y ~: ?S` show ?thesis by contradiction |
43 then have "y \<in> ?S" .. |
|
44 with `y \<notin> ?S` show ?thesis by contradiction |
43 qed |
45 qed |
44 qed |
46 qed |
45 qed |
47 qed |
46 |
48 |
47 text {* How much creativity is required? As it happens, Isabelle can |
49 text {* How much creativity is required? As it happens, Isabelle can |
49 Depth-first search would diverge, but best-first search successfully |
51 Depth-first search would diverge, but best-first search successfully |
50 navigates through the large search space. The context of Isabelle's |
52 navigates through the large search space. The context of Isabelle's |
51 classical prover contains rules for the relevant constructs of HOL's |
53 classical prover contains rules for the relevant constructs of HOL's |
52 set theory. *} |
54 set theory. *} |
53 |
55 |
54 theorem "EX S. S ~: range (f :: 'a => 'a set)" |
56 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
55 by best |
57 by best |
56 |
58 |
57 text {* While this establishes the same theorem internally, we do not |
59 text {* While this establishes the same theorem internally, we do not |
58 get any idea of how the proof actually works. There is currently no |
60 get any idea of how the proof actually works. There is currently no |
59 way to transform internal system-level representations of Isabelle |
61 way to transform internal system-level representations of Isabelle |