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.
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.
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-holconst
bnd_mono : GS → (GS → GS) → BOOL
∀D h• bnd_mono D h ⇔
fttabh(D) ⊆g D ∧
fttab∀x y• x ⊆g y ∧ y ⊆g D
fttabfttab⇒ 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 ⇔
fttabA ⊆g D
fttab∧ closed A h
fttab∧ ∀ B•
fttabfttabB ⊆g D
fttabfttab∧ closed B h
fttabfttab⇒ 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⌝]
fttabTHEN REPEAT strip_tac);
a (lemma_tac ⌜x ⊆g D⌝
fttabTHEN1 (
fttabfc_tac [⊆g_trans_thm]
fttabTHEN (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⌝]
fttabTHEN 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⌝]
fttabTHEN 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⌝]
fttabTHEN REPEAT strip_tac);
a (lemma_tac ⌜h X ⊆g h D⌝
fttabTHEN1 ASM_FC_T (MAP_EVERY (strip_asm_tac o (rewrite_rule [⊆g_refl_thm]))) []);
a (fc_tac[⊆g_trans_thm]
fttabTHEN 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⌝]
fttabTHEN REPEAT strip_tac);
a (bc_thm_tac ∪gg_thm1
fttabTHEN strip_tac
fttabTHEN (GET_NTH_ASM_T 3 bc_thm_tac)
fttabTHEN (rewrite_tac [⊆gg_thm])
fttabTHEN (bc_thm_tac ∪gg_thm1)
fttabTHEN 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⌝]
fttabTHEN 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)⌝
fttab(fn x=> accept_tac (⇒_match_mp_rule ⋂gg_thm x))
fttabTHEN1 asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (fc_tac [∈gg_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⌝,
fttabget_spec ⌜⋂g⌝]);
a (REPEAT strip_tac);
a (fc_tac [∈gg_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
fttabTHEN 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
fttab∧ (∀X• h X ⊆g X ∧ X ⊆g D ⇒ A ⊆g X)
fttab⇒ 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)⌝
fttab(fn x=> asm_tac(⇒_match_mp_rule ⊆gg_thm x))
fttabTHEN1 (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
fttab⇒ 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
fttabTHEN ∃_tac ⌜D⌝
fttabTHEN asm_rewrite_tac[]);
a (fc_tac[lfp_lowerbound]
fttabTHEN REPEAT (asm_fc_tac[]));
a (fc_tac[⊆g_trans_thm]
fttabTHEN 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
fttab⇒ 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⌝
fttabTHEN1 (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
fttab⇒ 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)
fttab∧ 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
fttab∧ 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⌝
fttabTHEN1 (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⌝
fttabTHEN1 (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
fttab⇒ iclosed D h = h(iclosed D h)⌝);
a (REPEAT strip_tac
fttabTHEN (rewrite_tac[⊆g_eq_thm]));
a (fc_tac[lfp_lemma2, lfp_lemma3]
fttabTHEN 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[
fttabget_spec ⌜closed⌝,
fttabget_spec ⌜least_closed⌝]);
a (rewrite_tac[lfp_subset]);
a (fc_tac[lfp_Tarski, lfp_lemma2]
fttabTHEN 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⌝
fttabTHEN GET_NTH_ASM_T 3
fttab(fn x=> once_rewrite_tac[eq_sym_rule x])
fttabTHEN 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
fttab∧ fixed_point A h
fttab∧ least_closed D A h⌝);
a (REPEAT strip_tac);
a (∃_tac ⌜iclosed D h⌝ THEN rewrite_tac[
fttabget_spec ⌜fixed_point⌝,
fttabget_spec ⌜closed⌝]);
a (rewrite_tac[lfp_subset]);
a (fc_tac[lfp_Tarski, lfp_lemma2, lemp_lemma]
fttabTHEN 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
fttab∧ fixed_point (lfp D h) h
fttab∧ least_closed D (lfp D h) h⌝);
a (∃_tac ⌜iclosed⌝ THEN rewrite_tac[
fttabget_spec ⌜fixed_point⌝,
fttabget_spec ⌜closed⌝]);
a (rewrite_tac[lfp_subset]);
a (REPEAT strip_tac
fttabTHEN fc_tac[lfp_Tarski, lfp_lemma2, lemp_lemma]
fttabTHEN REPEAT strip_tac);
xl_set_cs_∃_thm (pop_thm ());


xl-holconst
lfp: GS → (GS → GS) → GS
∀ D h • bnd_mono D h ⇒
fttab(lfp D h) ⊆g D
fttab∧ fixed_point (lfp D h) h
fttab∧ 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 ⇒ fttablfp D h ⊆g D⌝);
a (REPEAT strip_tac
fttabTHEN 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
fttabTHEN fc_tac [get_spec ⌜lfp⌝]);
a (GET_NTH_ASM_T 2
fttab(fn x=> rewrite_tac[eq_sym_rule(rewrite_rule[get_spec ⌜fixed_point⌝] x)])
fttabTHEN rewrite_tac[⊆g_refl_thm]);
val lfp_fixp = save_pop_thm "lfp_fixp";

set_goal([],⌜∀ D h• bnd_mono D h ⇒
fttab∀A X• h A ⊆g A
fttab∧ A ⊆g D
fttab⇒ lfp D h ⊆g A
⌝);
a (REPEAT strip_tac
fttabTHEN fc_tac [get_spec ⌜lfp⌝]);
a (asm_ante_tac ⌜least_closed D (lfp D h) h⌝
fttabTHEN (rewrite_tac [
fttabfttabget_spec ⌜least_closed⌝,
fttabfttabget_spec ⌜closed⌝])
fttabTHEN REPEAT strip_tac);
a (REPEAT (asm_fc_tac[]));
val lfp_lowerbound = save_pop_thm "lfp_lowerbound";

(*
set_goal([],⌜∀ D h• bnd_mono D h ⇒
fttab∀A X• h D ⊆g D
fttab∧ (∀X• h X ⊆g X ∧ X ⊆g D ⇒ A ⊆g X)
fttab⇒ 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•
fttabbnd_mono D h ∧ (∀x• x ∈g h(Sep (lfp D h) p) ⇒ p x)
fttab⇒ 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⌝
fttabTHEN1 (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 [
fttabrewrite_rule [
fttabfttabget_spec ⌜least_closed⌝,
fttabfttabget_spec ⌜closed⌝]
fttab(get_spec ⌜lfp⌝)]);
a (lemma_tac ⌜h (Sep (lfp D h) p) ⊆g lfp D h⌝
fttabTHEN1 (fc_tac[⊆g_trans_thm] THEN REPEAT (asm_fc_tac[])));
a (asm_ante_tac ⌜h (Sep (lfp D h) p) ⊆g lfp D h⌝
fttabTHEN 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•
fttabbnd_mono D h ∧ (∀x• x ∈g h(Sep (lfp D h) p) ⇒ p x) ∧ a ∈g lfp D h
fttab⇒ 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⌝
fttabTHEN (rewrite_tac [get_spec ⌜closed⌝])
fttabTHEN strip_tac);
a (lemma_tac ⌜Sep (lfp D h) p ⊆g D⌝
fttabTHEN1 (fc_tac[lfp_subset] THEN
fttabfttabasm_prove_tac[gst_relext_clauses]));
a (fc_tac [lfp_lowerbound]);
a (LEMMA_T ⌜lfp D h ⊆g Sep (lfp D h) p⌝ ante_tac
fttabTHEN1 (REPEAT (asm_fc_tac[])));
a (rewrite_tac[gst_relext_clauses]
fttabTHEN (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";


up quick index © RBJ

privacy policy

Created:

$Id: gst-fixedpoints.xml,v 1.2 2011/02/20 16:11:49 rbj Exp $

V