Indexed Sums and Products in GST
Overview
 Introduction A new "gst-rec" theory is created as a child of "gst-fun". Probably Sums
 Products Proof Context Listing of Theory gst-sumprod
Introduction
 A new "gst-rec" theory is created as a child of "gst-fun". Probably
The Theory gst-sumprod
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-sumprod"; force_new_pc "gst-sumprod"; merge_pcs ["xl_cs_∃_conv"] "gst-sumprod"; set_merge_pcs ["basic_hol", "gst-ax", "gst-fun", "gst-sumprod"];

Sums
Defining Dependent Sums
The symbol ⌜Σ⌝ is used for the dependent product or existential type constructor, which is a generalisation of a labelled disjoint union. It takes a set which must be a function and which is interpreted as an indexed collection of sets. It returns a set of ordered pairs the first of which is some value (the index) in the domain of the function, and the second is a value in the set which the function maps that index. The function is interpreted as assigning to each element in the index set a "type", and the result is the labelled disjoint union of all these types, the labels being the indexes.
 xl-sml set_goal([],⌜∃ Σ• ∀f• fun f ⇒ (∀e• e ∈g (Σ f) ≡ ∃i v• e = i ↦g v ∧ i ∈g dom f ∧ v ∈g f g i) ⌝); a (∃_tac ⌜λf• ⋃g ( Imagep (λi• Imagep (λv• i ↦g v) (f g i)) (dom f))⌝ THEN rewrite_tac[]); a (REPEAT strip_tac); (* *** Goal "1" *** *) a (asm_ante_tac ⌜e ∈g e'⌝ THEN asm_rewrite_tac[] THEN (REPEAT strip_tac)); a (∃_tac ⌜e''⌝ THEN ∃_tac ⌜e'''⌝ THEN asm_prove_tac[]); (* *** Goal "2" *** *) a (∃_tac ⌜Imagep (λ v• i ↦g v) (f g i)⌝ THEN asm_prove_tac[]); xl_set_cs_∃_thm (pop_thm ());

 xl-holconstΣ : GS → GS ∀f• fun f ⇒ (∀e• e ∈g (Σ f) ≡ ∃i v• e = i ↦g v ∧ i ∈g dom f ∧ v ∈g f g i)
Products
Defining Dependent Function Spaces
The symbol ⌜Π⌝ is used for the dependent function space constructor, which is a generalisation of a labelled product or record type constructor. It takes a set which must be a function and which is interpreted as an indexed collection of sets. It returns a set of functions. The domain of each function is the set of indexes, i.e. the domain of the indexed set. Each of the functions maps each of the indexes into a member of the set with that index in the indexed set. Each function is therefore a subset of the dependent produce space (or existential type), and this is used in the definition. The function is interpreted as assigning to each element in the index set a "type", and the result is the dependent function space.
 xl-sml (* set_goal([],⌜∃ Π• ∀f• fun f ⇒ (∀e• e ∈g (Π f) ≡ dom e = dom f ∧ e ⊆g Σ f) ⌝); a (∃_tac ⌜λf• Sep (℘ (Σ f)) (λs• fun s ∧ dom s = dom f)⌝ THEN rewrite_tac[]); type_of ⌜Imagep⌝; delete_const ⌜Σ⌝; y *)

 xl-holconstΠ : GS → GS ∀f• fun f ⇒ (∀e• e ∈g (Π f) ≡ dom e = dom f ∧ e ⊆g Σ f)
Proof Context
Proof Context

 xl-sml commit_pc "gst-sumprod";