A theory of fixed points
Overview
In this document I prove the Knaster-Tarski fixedpoint theorem in a general formulation for HOL.
A new "fixp" theory is created as a child of "hol".
Definition of the notion of a bounded monotonic function and of least and greatest fixed points.
Proofs that "lfp" gives a fixed point and that it is the least fixed point.
Proofs that "gfp" gives a fixed point and that it is the greatest fixed point.
Taking a closure of constructors for an inductive datatype definition.
Introduction
A new "fixp" theory is created as a child of "hol".
The Theory 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 "hol";


xl-sml
force_new_theory "fixp";
force_new_pc "fixp";
merge_pcs ["xl_cs_∃_conv"] "fixp";
set_merge_pcs ["hol", "fixp"];

Definitions
Definition of the notion of a bounded monotonic function and of least and greatest fixed points.
Introduction

monotonic
The property of being a monotonic function.
xl-holconst
monotonic : ('a SET → 'b SET) → BOOL
∀f• monotonic f ≡ ∀x y• x ⊆ y ⇒ f(x) ⊆ f(y)

xl-holconst
lfp : ('a SET → 'a SET) → 'a SET
∀f• lfp f = ⋂{X | f X ⊆ X}

xl-holconst
gfp : ('a SET → 'a SET) → 'a SET
∀f• gfp f = ⋃{X | X ⊆ f X}
Least Fixed Points
Proofs that "lfp" gives a fixed point and that it is the least fixed point.
Introduction

lfp Gives Fixed Points

xl-sml
set_goal([],⌜∀h• monotonic h ⇒ h (lfp h) = lfp h⌝);
a (rewrite_tac [get_spec ⌜lfp⌝] THEN REPEAT strip_tac);
a (lemma_tac ⌜h(⋂{X|h X ⊆ X}) ⊆ ⋂{X|h X ⊆ X}⌝);
(* *** Goal "1" *** *)
a (once_rewrite_tac[sets_ext_clauses] THEN REPEAT strip_tac);
a (lemma_tac ⌜(⋂{X|h X ⊆ X}) ⊆ s⌝);
(* *** Goal "1.1" *** *)
a (once_rewrite_tac[sets_ext_clauses] THEN REPEAT strip_tac);
a (spec_nth_asm_tac 1 ⌜s⌝);
(* *** Goal "1.2" *** *)
a (all_asm_fc_tac [get_spec ⌜monotonic⌝]);
a (all_fc_tac[get_spec ⌜$⊆⌝]);
a (all_fc_tac[get_spec ⌜$⊆⌝]);
(* *** Goal "2" *** *)
a (lemma_tac ⌜⋂{X|h X ⊆ X} ⊆ h(⋂{X|h X ⊆ X})⌝);
(* *** Goal "2.1" *** *)
a (once_rewrite_tac[sets_ext_clauses]);
a (REPEAT strip_tac);
a (spec_asm_tac ⌜∀ s• s ∈ {X|h X ⊆ X} ⇒ x ∈ s⌝ ⌜h (⋂ {X|h X ⊆ X})⌝);
a (fc_tac [get_spec ⌜monotonic⌝]);
a (list_spec_asm_tac ⌜∀ x y• x ⊆ y ⇒ h x ⊆ h y⌝ [⌜h(⋂ {X|h X ⊆ X})⌝, ⌜⋂ {X|h X ⊆ X}⌝]);
(* *** Goal "2.2" *** *)
a (all_asm_fc_tac [pc_rule "sets_ext" (prove_rule []) ⌜∀A B• A ⊆ B ∧ B ⊆ A ⇒ A = B⌝]);
val least_fixpoint_thm = save_pop_thm "least_fixpoint_thm";

lfp Gives the Least Fixed Point

xl-sml
set_goal([],⌜∀h• monotonic h ⇒ ∀g• h g = g ⇒ (lfp h) ⊆ g⌝);
a (rewrite_tac [get_spec ⌜lfp⌝] THEN REPEAT strip_tac);
a (once_rewrite_tac [sets_ext_clauses]
fttabTHEN REPEAT strip_tac);
a (spec_asm_tac ⌜∀ s• s ∈ {X|h X ⊆ X} ⇒ x ∈ s⌝ ⌜g⌝);
a (DROP_ASM_T ⌜¬ h g ⊆ g⌝ ante_tac THEN asm_rewrite_tac []);
val lfp_min_thm = save_pop_thm "lfp_min_thm";

Induction
I'm not whether the following really counts as an induction principle, but I expect it will help in deriving induction principles. It may be read as saying that if the functional preserves some property then that property holds everywhere in the least fixed point.
xl-sml
set_goal([],⌜∀h• monotonic h ⇒ ∀s• h s ⊆ s ⇒ (lfp h) ⊆ s⌝);
a (rewrite_tac [get_spec ⌜lfp⌝] THEN REPEAT strip_tac);
a (once_rewrite_tac [sets_ext_clauses] THEN REPEAT strip_tac);
a (asm_fc_tac[]);
val lfp_induction_thm = save_pop_thm "lfp_induction_thm";

Greatest Fixed Points
Proofs that "gfp" gives a fixed point and that it is the greatest fixed point.
Introduction

gfp Gives Fixed Points

xl-sml
set_goal([],⌜∀h• monotonic h ⇒ h (gfp h) = gfp h⌝);
a (rewrite_tac [get_spec ⌜gfp⌝] THEN REPEAT strip_tac);
a (lemma_tac ⌜⋃ {X|X ⊆ h X} ⊆ h (⋃ {X|X ⊆ h X})⌝);
(* *** Goal "1" *** *)
a (once_rewrite_tac[sets_ext_clauses] THEN REPEAT strip_tac);
a (lemma_tac ⌜s ⊆ ⋃ {X|X ⊆ h X}⌝);
(* *** Goal "1.1" *** *)
a (once_rewrite_tac[sets_ext_clauses] THEN REPEAT strip_tac);
a (∃_tac ⌜s⌝ THEN REPEAT strip_tac);
(* *** Goal "1.2" *** *)
a (lemma_tac ⌜s ∈ {X|X ⊆ h X}⌝);
(* *** Goal "1.1" *** *)
a (once_rewrite_tac[sets_ext_clauses] THEN REPEAT strip_tac);
a (all_asm_fc_tac [get_spec ⌜monotonic⌝]);
a (all_asm_fc_tac [get_spec ⌜$⊆⌝]);
a (all_asm_fc_tac [get_spec ⌜$⊆⌝]);
(* *** Goal "2" *** *)
a (lemma_tac ⌜h (⋃ {X|X ⊆ h X}) ∈ {X|X ⊆ h X}⌝);
(* *** Goal "2.1" *** *)
a (all_asm_fc_tac [get_spec ⌜monotonic⌝]);
a (asm_rewrite_tac [∈_in_clauses]);
(* *** Goal "2.2" *** *)
a (lemma_tac ⌜h (⋃ {X|X ⊆ h X}) ⊆ ⋃ {X|X ⊆ h X}⌝);
(* *** Goal "2.2.1" *** *)
a (once_rewrite_tac [sets_ext_clauses]);
a (REPEAT strip_tac);
a (∃_tac ⌜h (⋃ {X|X ⊆ h X})⌝);
a (REPEAT strip_tac);
(* *** Goal "2.2.2" *** *)
a (rewrite_tac [pc_rule "sets_ext" (prove_rule []) ⌜∀A B• A = B ≡ B ⊆ A ∧ A ⊆ B⌝]
fttabTHEN asm_rewrite_tac[]);
val greatest_fixpoint_thm = save_pop_thm "greatest_fixpoint_thm";

gfp Gives the Greatest Fixed Point

xl-sml
set_goal([],⌜∀h• monotonic h ⇒ ∀g• h g = g ⇒ g ⊆ (gfp h)⌝);
a (rewrite_tac [get_spec ⌜gfp⌝] THEN REPEAT strip_tac);
a (once_rewrite_tac [sets_ext_clauses]
fttabTHEN REPEAT strip_tac);
a (∃_tac ⌜g⌝ THEN asm_rewrite_tac[]);
val gfp_max_thm = save_pop_thm "gfp_max_thm";

C0-Induction
This is the corresponding theorem for greatest fixed point to the "induction" principle for least fixed points. I don't know whether its any use and am including it for the sake of symmetry!
xl-sml
set_goal([],⌜∀h• monotonic h ⇒ ∀s• s ⊆ h s ⇒ s ⊆ (gfp h)⌝);
a (rewrite_tac [get_spec ⌜gfp⌝] THEN REPEAT strip_tac);
a (once_rewrite_tac [sets_ext_clauses] THEN contr_tac);
a (asm_fc_tac[]);
val gfp_coinduction_thm = save_pop_thm "gfp_coinduction_thm";

Inductive Definitions
Taking a closure of constructors for an inductive datatype definition.
Introduction

The simplest example of interest here is the natural numbers, which can be defined (in HOL) as the smallest set of individuals which includes zero (the individual which is not in the range of the one-one function whose existence is asserted by the usual axiom of infinity) and is closed under the successor function (which is that same one-one function).

We can think of this as forming the natural numbers by starting with some set ({0}) and then adding the additional values following some prescription until no more can be added. Because we are always adding values, the operation on the set-of-values-so-far is monotonic. If the closure is supplied in a suitable manner then a completely general proof of monotonicity will suffice.

There is a little difficulty in doing this automatically because the operators under which closure is wanted (counting the starting points as 0-ary operators) will be of diverse types.

We keep the constructor exactly as it is required on the representation type. This is combined with an "immediate content" function on the domain of the constructor to give a relation which indicates which values are immediate constituents of a constructed value, and then we close up the empty set on the principle of adding a constructed value whenever its immediate constituents are available.

In addition to the constructor function and the content information we want to allow some constraint on values which are acceptable for the construction so that it need not be defined over the entire representation type. In fact this can be coded into the content function by making it reflexive for values which we wish to exclude from the domain. Actually its type doesn't allow reflexive, but mapping these to the universe of the representation type will do the trick.

Monotonicity

The following function converts such a relationship into a monotonic function. The initial "cc" in the name stands for "constructor and content (functions)".


xl-holconst
fttabcc2monof: ('a → 'b) × ('a → 'b SET) → ('b SET → 'b SET)
fttab∀tor tent• cc2monof (tor, tent) = λs• s ∪ {t | ∃u v• u = tent v ∧ u ⊆ s ∧ t = tor v}
We prove that this is the case:
xl-sml
set_goal([], ⌜∀tor tent• monotonic (cc2monof (tor, tent))⌝);
a (rewrite_tac [get_spec ⌜cc2monof⌝] THEN REPEAT strip_tac);
a (rewrite_tac [get_spec ⌜monotonic⌝]);
a (once_rewrite_tac [sets_ext_clauses] THEN REPEAT strip_tac);
(* *** Goal "1" *** *)
a (asm_fc_tac[]);
(* *** Goal "2" *** *)
a (∃_tac ⌜u⌝);
a (∃_tac ⌜v⌝ THEN REPEAT strip_tac);
a (DROP_ASM_T ⌜u ⊆ x⌝ ante_tac
fttabTHEN DROP_ASM_T ⌜∀ x'• x' ∈ x ⇒ x' ∈ y⌝ ante_tac
fttabTHEN PC_T1 "sets_ext" prove_tac []);
val mono_cc2monof_thm = save_pop_thm "mono_cc2monof_thm";

Closure
The following function defines the least fixed point of such an operator:
xl-holconst
fttabclosure: ('a → 'b) × ('a → 'b SET) → 'b SET
fttab∀tor tent• closure (tor, tent) = lfp (cc2monof (tor, tent))
We now prove that the result is indeed closed under the operations:
xl-sml
set_goal([], ⌜∀tor tent s x y•
fttab tent x = s
fttab∧ s ⊆ (closure (tor, tent))
fttab∧ y = tor x
fttab⇒ y ∈ (closure (tor, tent))⌝);
a (rewrite_tac [get_spec ⌜closure⌝] THEN REPEAT strip_tac);
a (asm_tac (list_∀_elim [⌜tor⌝, ⌜tent⌝] mono_cc2monof_thm));
a (ALL_FC_T (once_rewrite_tac o (map eq_sym_rule)) [least_fixpoint_thm]);
a (rewrite_tac[get_spec ⌜cc2monof⌝]
fttabTHEN REPEAT strip_tac);
a (∃_tac ⌜s⌝ THEN asm_rewrite_tac[]);
a (∃_tac ⌜x⌝ THEN asm_rewrite_tac[]);
a (DROP_ASM_T ⌜s ⊆ lfp (cc2monof (tor, tent))⌝ ante_tac
fttabTHEN rewrite_tac[get_spec ⌜cc2monof⌝]);
val closure_thm1 = save_pop_thm "closure_thm1";

Induction
We prove an induction theorem for sets defined as closures.
xl-sml
set_goal([], ⌜∀tor tent p•
fttab(∀x• (∃y• tor y = x ∧ tent y ⊆ p) ⇒ x ∈ p)
fttab⇒ closure (tor, tent) ⊆ p⌝);
a (rewrite_tac [get_spec ⌜closure⌝]);
a (REPEAT strip_tac);
a (asm_tac (list_∀_elim [⌜tor⌝, ⌜tent⌝] mono_cc2monof_thm));
a (fc_tac [lfp_induction_thm]);
a (spec_asm_tac ⌜∀ s• cc2monof (tor, tent) s ⊆ s ⇒ lfp (cc2monof (tor, tent)) ⊆ s⌝ ⌜p⌝);
a (swap_asm_concl_tac ⌜¬ cc2monof (tor, tent) p ⊆ p⌝);
a (rewrite_tac [get_spec ⌜cc2monof⌝]);
a (once_rewrite_tac [sets_ext_clauses]);
a (REPEAT strip_tac);
a (spec_asm_tac ⌜∀ x• (∃ y• tor y = x ∧ tent y ⊆ p) ⇒ x ∈ p⌝ ⌜x⌝);
a (spec_asm_tac ⌜∀ y• ¬ (tor y = x ∧ tent y ⊆ p)⌝ ⌜v⌝);
(* *** Goal "1" *** *)
a (DROP_ASM_T ⌜¬ tor v = x⌝ ante_tac
fttabTHEN asm_rewrite_tac[]);
(* *** Goal "2" *** *)
a (DROP_ASM_T ⌜u ⊆ p⌝ ante_tac
fttabTHEN once_asm_rewrite_tac[]
fttabTHEN strip_tac);
val closure_induction_thm = save_pop_thm "closure_induction_thm";

Coding Constructors
Definitions of constructors for products and lists, and injections for disjoint unions.
Definitions
In the following constructor definitions the first argument is expected to be an injection from a preferred indexing type for this constructor to some actual indexing type.
xl-holconst
IndPair : (BOOL → 'a) → ('a LIST → (ONE + 'b)) × ('a LIST → (ONE + 'b))
fttab→ ('a LIST → (ONE + 'b))
∀i l r h t•
fttabIndPair i (l, r) Nil = InL One
fttabIndPair i (l, r) (Cons h t) =
fttabfttabif h = i F then l t
fttabfttabelse if h = i T then r t
fttabfttabelse InL One

xl-holconst
IndInL : (BOOL → 'a) → ('a LIST → (ONE + 'b))
fttab→ ('a LIST → (ONE + 'b))
∀i j h t•
fttabIndInL i j Nil = InL One
fttabIndInL i j (Cons h t) =
fttabfttabif h = i F then j t
fttabfttabelse InL One

xl-holconst
IndInR : (BOOL → 'a) → ('a LIST → (ONE + 'b))
fttab→ ('a LIST → (ONE + 'b))
∀i j h t•
fttabIndInR i j Nil = InL One
fttabIndInR i j (Cons h t) =
fttabfttabif h = i T then j t
fttabfttabelse InL One

xl-holconst
IndSum : (BOOL → 'a) → ('a LIST → (ONE + 'b)) + ('a LIST → (ONE + 'b))
fttab→ ('a LIST → (ONE + 'b))
∀i j h t•
fttab(IndSum i j Nil = InL One)
fttab(IndSum i j (Cons h t) =
fttabfttabif IsL j
fttabfttabthenfttabif h = i F
fttabfttabfttabthen OutL j t
fttabfttabfttabelse InL One
fttabfttabelsefttabif h = i T
fttabfttabfttabthen OutR j t
fttabfttabfttabelse InL One)

xl-holconst
IndList : (ℕ → 'a) → ('a LIST → (ONE + 'b)) LIST
fttab→ ('a LIST → (ONE + 'b))
∀i ha ta hb tb•
fttabIndList i Nil tb = InL One
fttabIndList i (Cons ha ta) Nil = InL One
fttabIndList i (Cons ha ta) (Cons hb tb) =
fttabfttabif (∃j• hb = i j ∧ j < Length ta) then IndList i ta (Cons hb tb)
fttabfttabelse if hb = i (Length ta) then (ha tb)
fttabfttabelse InL One
Computing a Constructor
The following function takes a HOL type and a list of constructors and computes a compound constructor. The HOL type should have a sum of any finite number of distinct type variables as its codomain The constructors should include one for each type constructor which is involved in the recursion.
Computing a Constructor
Proof Context
In this section I will create a decent proof context for fixedpoints, eventually.
Proof Context

xl-sml
commit_pc "fixp";


up quick index © RBJ

privacy policy

Created:

$Id: x001.xml,v 1.5 2008/04/15 18:21:36 rbj01 Exp $

V