The theory of fixed points in GST
Overview
 In this document I am investigating how hard it is to prove the Knaster-Tarski fixedpoint theorem in GST. I am following Larry Paulson's paper, to whatever extent that is possible with ProofPower.
 Introduction A new "gst-fixp" theory is created as a child of "gst-fun". Probably Monotonicity and Closure Definitions Definitions of the notion of a bounded monotonic function, and of the closure of a set under such a function. Least Closure and Fixed Point Definitions The concepts fixed point, least closed, and a function yielding an intersection of closures are defined. Monotonicity and Closure Lemmas In this section lemmas are proven following Paulson's proof as closely as possible.
 Least Fixed Point Lemmas Least Fixed Point Theorem and Definition Induction Listing of Theory gst-fixp
Introduction
 A new "gst-fixp" theory is created as a child of "gst-fun". Probably
The Theory gst-fixp
The new theory is first created, together with a proof context which we will build up as we develop the theory.
 xl-sml open_theory "gst-fun"; force_new_theory "gst-fixp"; force_new_pc "gst-fixp"; merge_pcs ["xl_cs_∃_conv"] "gst-fixp"; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun", "gst-fixp"];

Monotonicity and Closure Definitions
 Definitions of the notion of a bounded monotonic function, and of the closure of a set under such a function.
Introduction

Larry Paulson does his fixed-point theory in Isabelle using "meta-level functions" rather than functional sets. I am guessing that in GST the closest analogy is a HOL function over sets. Certainly the transcription is entirely mechanical. I am also following Paulson in proving the theorem relative to the lattice of subsets of some set, rather than an arbitrary complete lattice. It would also be possible to do this relative to a HOL property and its subproperties and this might be thought more general, since it would then be applicable to arbitrary HOL types. I think the pseudo-urelements in GST will mean that the results proven in set theory are easy to apply to other types, and this avoids having to do the set theory used in the proofs for properties as well as for sets.

bnd_mono
The property of being a bounded monotonic function. The first argument is the set whose powerset is the relevant lattice.
 xl-holconstbnd_mono : GS → (GS → GS) → BOOL ∀D h• bnd_mono D h ⇔ h(D) ⊆g D ∧ ∀x y• x ⊆g y ∧ y ⊆g D ⇒ h(x) ⊆g h(y)
Closures

I have some reservations about the terminology used in Paulson's paper (though this may well be standard), so I am making some adjustments which have very little impact on the proofs. There are two problems.

The first is that he defines "lfp" to mean something which he later proves is the least fixed point. I would prefer the definition of "lfp" to more directly state that the thing yielded us the least fixed point.

The second is that while he talks about fixed points, some of his formal material is really about closures.

So I'm going to talk about closures until I have proven the "fixed point" theorem, and then define "lfp" (actually as yielding a fixed point which is the least closure, since this is slightly "stronger" than least fixed point).

Here you should first think of forming closures under certain operations. This is hard to formalise in a general way because the signatures of the operations may vary. So we suppose that we are doing an iterative process (like the iterative construction of the heirarchy of sets except that that particular one never yields a closed). At each step in this process new objects are formed from an existing set using the operations under which we are aiming for closure, and these are added to the old objects to form a new set. For the function doing this we usually use the name "h". If we ever find a set closed under the operations then we find that the result of applying "h" to it is contained in the original (no new objects result), and that is what the following definition of closed states:

 xl-holconst closed : GS → (GS → GS) → BOOL ∀A h• closed A h ⇔ h(A) ⊆g A
Least Closure and Fixed Point Definitions
 The concepts fixed point, least closed, and a function yielding an intersection of closures are defined.
Fixed Point
A fixed point of "h" is a set which h maps onto itself. This is also a closed.
 xl-holconst fixed_point : GS → (GS → GS) → BOOL ∀A h• fixed_point A h ⇔ A = h(A)
Least closed
We define here the property of being a least closed set under some function.
 xl-holconst least_closed : GS → GS → (GS → GS) → BOOL ∀D A h• least_closed D A h ⇔ A ⊆g D ∧ closed A h ∧ ∀ B• B ⊆g D ∧ closed B h ⇒ A ⊆g B
Intersection of closures
This is what Paulson defines as the least fixed point. I'm going to call it "iclosed" for "intersection of closed sets", and then the proof shows that it is also the least fixed point and justifies the subsequent definition of least fixed point.
 xl-holconst iclosed : GS → (GS → GS) → GS ∀D h• iclosed D h = ⋂g (Sep (℘g D) λX• h(X) ⊆g X)
Monotonicity and Closure Lemmas
 In this section lemmas are proven following Paulson's proof as closely as possible.
Motivation

I'm following Paulson's proof to get a feel for how much harder it is with ProofPower's less powerful proof automation (and my limited competence driving it). Also, I have no reason to be original, so far as I know.

bnd_monoI
This is an introduction rule for bnd_mono.
 xl-sml set_goal([],⌜∀ D h • h D ⊆g D ∧ (∀W X• W ⊆g D ∧ X ⊆g D ∧ W ⊆g X ⇒ (h W) ⊆g (h X)) ⇒ bnd_mono D h⌝); a (rewrite_tac[get_spec ⌜bnd_mono⌝] THEN REPEAT strip_tac); a (lemma_tac ⌜x ⊆g D⌝ THEN1 ( fc_tac [⊆g_trans_thm] THEN (asm_fc_tac[]))); a (REPEAT (asm_fc_tac[])); val bnd_monoI = save_pop_thm "bnd_monoI";

bnd_monoD1

 xl-sml set_goal([],⌜∀ D h • bnd_mono D h ⇒ (h D) ⊆g D⌝); a (rewrite_tac[get_spec ⌜bnd_mono⌝] THEN REPEAT strip_tac); val bnd_monoD1 = save_pop_thm "bnd_monoD1";

bnd_monoD2

 xl-sml set_goal([],⌜∀ D h • bnd_mono D h ∧ W ⊆g X ∧ X ⊆g D ⇒ (h W) ⊆g (h X)⌝); a (rewrite_tac[get_spec ⌜bnd_mono⌝] THEN REPEAT strip_tac); a (asm_fc_tac[]); val bnd_monoD2 = save_pop_thm "bnd_monoD2";

bnd_mono_subset

 xl-sml set_goal([],⌜∀ D h • bnd_mono D h ∧ X ⊆g D ⇒ (h X) ⊆g D⌝); a (rewrite_tac[get_spec ⌜bnd_mono⌝] THEN REPEAT strip_tac); a (lemma_tac ⌜h X ⊆g h D⌝ THEN1 ASM_FC_T (MAP_EVERY (strip_asm_tac o (rewrite_rule [⊆g_refl_thm]))) []); a (fc_tac[⊆g_trans_thm] THEN asm_fc_tac[]); val bnd_mono_subset = save_pop_thm "bnd_mono_subset";

bnd_mono_

 xl-sml set_goal([],⌜∀ D A B h • bnd_mono D h ∧ A ⊆g D ∧ B ⊆g D ⇒ (h A) ∪g (h B) ⊆g h (A ∪g B)⌝); a (rewrite_tac[get_spec ⌜bnd_mono⌝] THEN REPEAT strip_tac); a (bc_thm_tac ∪g⊆g_thm1 THEN strip_tac THEN (GET_NTH_ASM_T 3 bc_thm_tac) THEN (rewrite_tac [⊆g∪g_thm]) THEN (bc_thm_tac ∪g⊆g_thm1) THEN contr_tac); val bnd_mono_∪g = save_pop_thm "bnd_mono_∪g";

Least Fixed Point Lemmas
lfp_lowerbound

 xl-sml set_goal([],⌜∀ D h A• h A ⊆g A ∧ A ⊆g D ⇒ iclosed D h ⊆g A⌝); a (rewrite_tac[get_spec ⌜iclosed⌝] THEN REPEAT strip_tac); a (once_rewrite_tac[gst_relext_clauses]); a (REPEAT strip_tac); a (lemma_tac ⌜⋂g (Sep (℘g D) (λ X• h X ⊆g X)) ⊆g A⌝); (* *** Goal "1" *** *) a (LEMMA_T ⌜A ∈g Sep (℘g D) (λ X• h X ⊆g X)⌝ (fn x=> accept_tac (⇒_match_mp_rule ⋂g⊆g_thm x)) THEN1 asm_rewrite_tac[]); (* *** Goal "2" *** *) a (fc_tac [∈g⊆g_thm]); a (asm_fc_tac[]); val lfp_lowerbound = pop_thm ();

lfp_subset

 xl-sml set_goal([],⌜∀ D h• iclosed D h ⊆g D⌝); a (once_rewrite_tac[gst_relext_clauses]); a (rewrite_tac[get_spec ⌜iclosed⌝, get_spec ⌜⋂g⌝]); a (REPEAT strip_tac); a (fc_tac [∈g⊆g_thm]); a (asm_fc_tac[]); val lfp_subset = pop_thm ();

def_lfp_subset

 xl-sml set_goal([],⌜∀ A D h• A = iclosed D h ⇒ A ⊆g D⌝); a (REPEAT strip_tac THEN asm_rewrite_tac[lfp_subset]); val def_lfp_subset = save_pop_thm "def_lfp_subset";

lfp_greatest

 xl-sml set_goal([],⌜∀ A D h• h D ⊆g D ∧ (∀X• h X ⊆g X ∧ X ⊆g D ⇒ A ⊆g X) ⇒ A ⊆g iclosed D h⌝); a (REPEAT strip_tac); a (rewrite_tac [get_spec⌜iclosed⌝]); a (LEMMA_T ⌜D ∈g Sep (℘g D) (λ X• h X ⊆g X)⌝ (fn x=> asm_tac(⇒_match_mp_rule ⊆g⋂g_thm x)) THEN1 (asm_rewrite_tac[⊆g_refl_thm])); a (lemma_tac ⌜∀ D'• D' ∈g Sep (℘g D) (λ X• h X ⊆g X) ⇒ A ⊆g D'⌝); (* *** Goal "1" *** *) a (rewrite_tac[]); a (asm_prove_tac[]); (* *** Goal "2" *** *) a (REPEAT (asm_fc_tac[])); val lfp_greatest = save_pop_thm "lfp_greatest";

lfp_lemma1

 xl-sml set_goal([],⌜∀ A D h• bnd_mono D h ∧ h A ⊆g A ∧ A ⊆g D ⇒ h(iclosed D h) ⊆g A⌝); a (REPEAT strip_tac); a (lemma_tac ⌜h(iclosed D h) ⊆g h A⌝); a (bc_thm_tac bnd_monoD2 THEN ∃_tac ⌜D⌝ THEN asm_rewrite_tac[]); a (fc_tac[lfp_lowerbound] THEN REPEAT (asm_fc_tac[])); a (fc_tac[⊆g_trans_thm] THEN REPEAT (asm_fc_tac[])); val lfp_lemma1 = save_pop_thm "lfp_lemma1";

lfp_lemma2

 xl-sml set_goal([],⌜∀ A D h• bnd_mono D h ⇒ h(iclosed D h) ⊆g iclosed D h⌝); a (REPEAT strip_tac); a (lemma_tac ⌜∀ X• h X ⊆g X ∧ X ⊆g D ⇒ h (iclosed D h) ⊆g X⌝); (* *** Goal "1" *** *) a (REPEAT strip_tac); a (fc_tac [lfp_lemma1]); a (REPEAT (asm_fc_tac[])); (* *** Goal "2" *** *) a (lemma_tac ⌜h D ⊆g D⌝ THEN1 (fc_tac[bnd_monoD1])); a (fc_tac[lfp_greatest]); a (asm_fc_tac[]); val lfp_lemma2 = save_pop_thm "lfp_lemma2";

lfp_lemma3

 xl-sml set_goal([],⌜∀ A D h• bnd_mono D h ⇒ iclosed D h ⊆g h(iclosed D h)⌝); a (REPEAT strip_tac); a (lemma_tac ⌜h (h (iclosed D h)) ⊆g h (iclosed D h) ∧ h (iclosed D h) ⊆g D⌝); (* *** Goal "1" *** *) a strip_tac; (* *** Goal "1.1" *** *) a (lemma_tac ⌜h (iclosed D h) ⊆g iclosed D h ∧ iclosed D h ⊆g D⌝); (* *** Goal "1.1.1" *** *) a strip_tac; (* *** Goal "1.1.1.1" *** *) a (fc_tac [lfp_lemma2]); (* *** Goal "1.1.1.2" *** *) a (lemma_tac ⌜D ⊆g D⌝ THEN1 (rewrite_tac [⊆g_refl_thm])); a (lemma_tac ⌜h D ⊆g D⌝); (* *** Goal "1.1.1.2.1" *** *) a (fc_tac [bnd_mono_subset]); a (spec_asm_tac ⌜∀ X• X ⊆g D ⇒ h X ⊆g D⌝ ⌜D⌝ ); a (POP_ASM_T ante_tac THEN rewrite_tac[]); (* *** Goal "1.1.1.2.2" *** *) a (rewrite_tac [lfp_subset]); (* *** Goal "1.1.2" *** *) a (fc_tac [bnd_monoD2]); a (REPEAT (asm_fc_tac[])); (* *** Goal "1.2" *** *) a (lemma_tac ⌜iclosed D h ⊆g D⌝ THEN1 (rewrite_tac [lfp_subset])); a (fc_tac[bnd_mono_subset]); a (REPEAT (asm_fc_tac[])); (* *** Goal "2" *** *) a (all_fc_tac [lfp_lowerbound]); val lfp_lemma3 = save_pop_thm "lfp_lemma3";

Least Fixed Point Theorem and Definition
lfp_Tarski
This is Paulson's version of Tarski's theorem, apart from my using the name "iclosed" instead of "lfp".
 xl-sml set_goal([],⌜∀ A D h• bnd_mono D h ⇒ iclosed D h = h(iclosed D h)⌝); a (REPEAT strip_tac THEN (rewrite_tac[⊆g_eq_thm])); a (fc_tac[lfp_lemma2, lfp_lemma3] THEN REPEAT strip_tac); val lfp_Tarski = save_pop_thm "lfp_Tarski";

least_closed iclosed
Now we take a brief excursion from Paulson's path resulting from my eccentricities on the specificaton.
 xl-sml set_goal([],⌜∀ D h • bnd_mono D h ⇒ least_closed D (iclosed D h) h⌝); a (REPEAT strip_tac); a (rewrite_tac[ get_spec ⌜closed⌝, get_spec ⌜least_closed⌝]); a (rewrite_tac[lfp_subset]); a (fc_tac[lfp_Tarski, lfp_lemma2] THEN REPEAT strip_tac); a (lemma_tac ⌜h (iclosed D h) ⊆g B⌝); (* *** Goal "1" *** *) a (fc_tac[lfp_lemma1]); a (REPEAT (asm_fc_tac[])); (* *** Goal "2" *** *) a (asm_ante_tac ⌜h (iclosed D h) ⊆g B⌝ THEN GET_NTH_ASM_T 3 (fn x=> once_rewrite_tac[eq_sym_rule x]) THEN REPEAT strip_tac); val lemp_lemma = save_pop_thm "lemp_lemma";

Fixed Point Theorem

 xl-sml set_goal([],⌜∀ D h • bnd_mono D h ⇒ ∃A• A ⊆g D ∧ fixed_point A h ∧ least_closed D A h⌝); a (REPEAT strip_tac); a (∃_tac ⌜iclosed D h⌝ THEN rewrite_tac[ get_spec ⌜fixed_point⌝, get_spec ⌜closed⌝]); a (rewrite_tac[lfp_subset]); a (fc_tac[lfp_Tarski, lfp_lemma2, lemp_lemma] THEN REPEAT strip_tac); val Tarski_thm = save_pop_thm "Tarski_thm";

Least Fixed Point Function
This asserts the existence of a function delivering least fixed points.
 xl-sml set_goal([],⌜∃lfp• ∀ D h • bnd_mono D h ⇒ (lfp D h) ⊆g D ∧ fixed_point (lfp D h) h ∧ least_closed D (lfp D h) h⌝); a (∃_tac ⌜iclosed⌝ THEN rewrite_tac[ get_spec ⌜fixed_point⌝, get_spec ⌜closed⌝]); a (rewrite_tac[lfp_subset]); a (REPEAT strip_tac THEN fc_tac[lfp_Tarski, lfp_lemma2, lemp_lemma] THEN REPEAT strip_tac); xl_set_cs_∃_thm (pop_thm ());

 xl-holconstlfp: GS → (GS → GS) → GS ∀ D h • bnd_mono D h ⇒ (lfp D h) ⊆g D ∧ fixed_point (lfp D h) h ∧ least_closed D (lfp D h) h
Least Fixed Point Clauses
We now need to carry forward some of the useful results about "iclosed" to "lfp".
 xl-sml set_goal([],⌜∀ D h• bnd_mono D h ⇒ lfp D h ⊆g D⌝); a (REPEAT strip_tac THEN fc_tac [get_spec ⌜lfp⌝]); val lfp_subset = save_pop_thm "lfp_subset"; set_goal([],⌜∀ D h• bnd_mono D h ⇒ h(lfp D h) = lfp D h⌝); a (REPEAT strip_tac THEN fc_tac [get_spec ⌜lfp⌝]); a (GET_NTH_ASM_T 2 (fn x=> rewrite_tac[eq_sym_rule(rewrite_rule[get_spec ⌜fixed_point⌝] x)]) THEN rewrite_tac[⊆g_refl_thm]); val lfp_fixp = save_pop_thm "lfp_fixp"; set_goal([],⌜∀ D h• bnd_mono D h ⇒ ∀A X• h A ⊆g A ∧ A ⊆g D ⇒ lfp D h ⊆g A ⌝); a (REPEAT strip_tac THEN fc_tac [get_spec ⌜lfp⌝]); a (asm_ante_tac ⌜least_closed D (lfp D h) h⌝ THEN (rewrite_tac [ get_spec ⌜least_closed⌝, get_spec ⌜closed⌝]) THEN REPEAT strip_tac); a (REPEAT (asm_fc_tac[])); val lfp_lowerbound = save_pop_thm "lfp_lowerbound"; (* set_goal([],⌜∀ D h• bnd_mono D h ⇒ ∀A X• h D ⊆g D ∧ (∀X• h X ⊆g X ∧ X ⊆g D ⇒ A ⊆g X) ⇒ A ⊆g lfp D h ⌝); *)

Induction
Set is Closed
This lemma states that the induction hypothesis (couched in terms of h) imply that the set of elements having the property is closed under h.
 xl-sml set_goal([],⌜∀D h p• bnd_mono D h ∧ (∀x• x ∈g h(Sep (lfp D h) p) ⇒ p x) ⇒ closed (Sep (lfp D h) p) h⌝); a (prove_tac [get_spec ⌜closed⌝]); a (once_rewrite_tac [gst_relext_clauses]); a (asm_prove_tac[]); a (lemma_tac ⌜h (Sep (lfp D h) p) ⊆g h (lfp D h)⌝); a (lemma_tac ⌜Sep (lfp D h) p ⊆g lfp D h⌝); a (prove_tac [gst_relext_clauses]); a (lemma_tac ⌜lfp D h ⊆g D⌝ THEN1 (fc_tac[get_spec ⌜lfp⌝])); a (fc_tac [bnd_monoD2]); a (REPEAT (asm_fc_tac[])); a (lemma_tac ⌜h (lfp D h) ⊆g lfp D h⌝); a (fc_tac [ rewrite_rule [ get_spec ⌜least_closed⌝, get_spec ⌜closed⌝] (get_spec ⌜lfp⌝)]); a (lemma_tac ⌜h (Sep (lfp D h) p) ⊆g lfp D h⌝ THEN1 (fc_tac[⊆g_trans_thm] THEN REPEAT (asm_fc_tac[]))); a (asm_ante_tac ⌜h (Sep (lfp D h) p) ⊆g lfp D h⌝ THEN asm_prove_tac [gst_relext_clauses]); val Collect_is_pre_fixedpt = save_pop_thm "Collect_is_pre_fixedpt";

Induction

 xl-sml set_goal([],⌜∀D h p a• bnd_mono D h ∧ (∀x• x ∈g h(Sep (lfp D h) p) ⇒ p x) ∧ a ∈g lfp D h ⇒ p a⌝); a (REPEAT strip_tac); a (fc_tac [Collect_is_pre_fixedpt]); a (asm_fc_tac[]); a (asm_ante_tac ⌜closed (Sep (lfp D h) p) h⌝ THEN (rewrite_tac [get_spec ⌜closed⌝]) THEN strip_tac); a (lemma_tac ⌜Sep (lfp D h) p ⊆g D⌝ THEN1 (fc_tac[lfp_subset] THEN asm_prove_tac[gst_relext_clauses])); a (fc_tac [lfp_lowerbound]); a (LEMMA_T ⌜lfp D h ⊆g Sep (lfp D h) p⌝ ante_tac THEN1 (REPEAT (asm_fc_tac[]))); a (rewrite_tac[gst_relext_clauses] THEN (REPEAT strip_tac)); a (REPEAT (asm_fc_tac[])); val induct = save_pop_thm "induct";

Proof Context
 In this section I will create a decent proof context for fixedpoints, eventually.
Proof Context

 xl-sml commit_pc "gst-fixp";