(*
  Tarski's fixed-point theorem on sets (complete lattice)
  Isabelle 2014
*)
theory Tarski imports Main begin

lemma fp1: "mono F ==> F (Inter {X. F X <= X}) <= Inter {X. F X <= X}"
apply(rule subsetI)
apply(rule InterI)
apply(simp)
apply(subgoal_tac "Inter {X. F X <= X} <= X")
apply(drule_tac x="Inter {X. F X <= X}" in monoD)
apply(auto)
done

lemma fp2: "mono F ==> Inter {X. F X <= X} <= F (Inter {X. F X <= X})"
apply(frule fp1)
apply(drule monoD)
apply(auto)
done

theorem fp: "mono F ==> Inter {X. F X <= X} = F (Inter {X. F X <= X})"
apply(rule antisym)
apply(erule fp2)
apply(erule fp1)
done