A theory of fixed points
Overview
 In this document I prove the Knaster-Tarski fixedpoint theorem in a general formulation for HOL.
 Introduction A new "fixp" theory is created as a child of "hol". Definitions Definition of the notion of a bounded monotonic function and of least and greatest fixed points. Least Fixed Points Proofs that "lfp" gives a fixed point and that it is the least fixed point.
 Greatest Fixed Points Proofs that "gfp" gives a fixed point and that it is the greatest fixed point. Inductive Definitions Taking a closure of constructors for an inductive datatype definition. Listing of Theory fixp
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-holconstmonotonic : ('a SET 'b SET) BOOL f monotonic f x y x y f(x) f(y)

 xl-holconstlfp : ('a SET 'a SET) 'a SET f lfp f = {X | f X X}

 xl-holconstgfp : ('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] THEN 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] THEN 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] THEN 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╷cc2monof: ('a 'b) ('a 'b SET) ('b SET 'b SET) ╷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 THEN DROP_ASM_T x' x' x x' y ante_tac THEN 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╷closure: ('a 'b) ('a 'b SET) 'b SET ╷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 tent x = s s (closure (tor, tent)) y = tor x 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] THEN 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 THEN 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 (x (y tor y = x tent y p) x p) 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 THEN asm_rewrite_tac[]); (* *** Goal "2" *** *) a (DROP_ASM_T u p ante_tac THEN once_asm_rewrite_tac[] THEN 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-holconstIndPair : (BOOL 'a) ('a LIST (ONE + 'b)) ('a LIST (ONE + 'b)) ('a LIST (ONE + 'b)) i l r h t IndPair i (l, r) Nil = InL One IndPair i (l, r) (Cons h t) = if h = i F then l t else if h = i T then r t else InL One

 xl-holconstIndInL : (BOOL 'a) ('a LIST (ONE + 'b)) ('a LIST (ONE + 'b)) i j h t IndInL i j Nil = InL One IndInL i j (Cons h t) = if h = i F then j t else InL One

 xl-holconstIndInR : (BOOL 'a) ('a LIST (ONE + 'b)) ('a LIST (ONE + 'b)) i j h t IndInR i j Nil = InL One IndInR i j (Cons h t) = if h = i T then j t else InL One

 xl-holconstIndSum : (BOOL 'a) ('a LIST (ONE + 'b)) + ('a LIST (ONE + 'b)) ('a LIST (ONE + 'b)) i j h t (IndSum i j Nil = InL One) (IndSum i j (Cons h t) = if IsL j thenif h = i F then OutL j t else InL One elseif h = i T then OutR j t else InL One)

 xl-holconstIndList : ( 'a) ('a LIST (ONE + 'b)) LIST ('a LIST (ONE + 'b)) i ha ta hb tb IndList i Nil tb = InL One IndList i (Cons ha ta) Nil = InL One IndList i (Cons ha ta) (Cons hb tb) = if (j hb = i j j < Length ta) then IndList i ta (Cons hb tb) else if hb = i (Length ta) then (ha tb) else 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";

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

V