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.

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

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}

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

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

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

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

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

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

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.

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

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

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

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)) → ('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-holconst IndInL : (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-holconst IndInR : (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-holconst IndSum : (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-holconst IndList : (ℕ → '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

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.

xl-sml commit_pc "fixp";