A new "gst-fixp" theory is created as a child of "gst-fun". Probably

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

The concepts fixed point, least closed, and a function yielding an intersection of closures are defined.

In this section lemmas are proven following Paulson's proof as closely as possible.

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"];

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.

The property of being a bounded monotonic function. The first argument is the set whose powerset is the relevant lattice.

xl-holconst bnd_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)

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

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)

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

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)

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.

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";

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";

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";

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";

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";

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 ();

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 ();

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";

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";

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";

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";

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";

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";

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";

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";

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-holconst lfp: 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

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 ⌝); *)

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";

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";

xl-sml commit_pc "gst-fixp";