Created
September 28, 2019 04:40
-
-
Save hatsugai/236c610991844ddb3b614e95ed38ec35 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment