theory Scratch2
imports Main
begin
lemma foo:
"(\x. P x) \ (\x. P x)"
apply (rule impI)
apply (rule exI)
apply (erule allE)
by assumption
lemma "\P Q. P \ Q \ P \ Q"
by blast
lemma knaster_tarski:
fixes f :: "'a :: complete_lattice \ 'a"
assumes as1: "mono f"
shows "\A. f A = A"
proof -
define H where [simp]: "H \ {x. f x \ x}"
define F where [simp]: "F \ Inf H"
thm Inf_greatest
have s1: "f F \ F"
proof (unfold H_def F_def, rule Inf_greatest)
fix x
assume a: "x \ {x. f x \ x}"
have "Inf {x. f x \ x} \ x"
using Inf_lower a by force
then have "f (Inf {x. f x \ x}) \ f x"
using \mono f\ unfolding mono_def by auto
also have "\ \ x" using a by auto
finally show "f (Inf {x. f x \ x}) \ x" .
qed
moreover have "F \ f F"
proof -
have "f (f F) \ f F" using s1 \mono f\
unfolding mono_def by auto
then have *: "f F \ H" by auto
show ?thesis using Inf_lower[OF *] by auto
qed
ultimately show ?thesis
by (auto simp del: H_def F_def)
qed
lemma CBS:
assumes "inj_on f A" "inj_on g B"
assumes f_sub: "f ` A \ B" and g_sub: "g ` B \ A"
shows "\h. inj_on h A \ h ` A = B"
proof -
define F where [simp]: "F \ \X. A - (g ` (B - (f ` X)))"
have "mono F" unfolding mono_def
by fastforce
then obtain X where "F X = X" using knaster_tarski by blast
term the_inv_into
define g' where "g' \ the_inv_into (B - (f ` X)) g"
have "g' ` (A - X) = B - (f ` X)" sorry
define h where "h \ \x. if x \ X then f x else g' x"
have "inj_on h A" sorry
moreover have "h ` A = B" sorry
ultimately show ?thesis
by fastforce
qed