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 ( f) i v e = i v i dom f v f g i) f Galaxy f ); a (_tac f ( Image (i Image (v i v) (f g i)) (dom f)) THEN rewrite_tac[]); a (prove_tac []); (* *** Goal "1" *** *) a (asm_ante_tac e e' THEN asm_rewrite_tac[] THEN (REPEAT strip_tac)); a (_tac e'' THEN _tac e''' THEN asm_prove_tac[]); (* *** Goal "2" *** *) a (_tac Image ( v i v) (f g i) THEN asm_prove_tac[]); (* *** Goal "3" *** *)

 xl-holconst : 'a GS 'a GS f fun f (e e ( f) i v e = i v i dom f v f g i) f Galaxy f
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 ( f) dom e = dom f e f) f Galaxy f ); a (_tac f Sep ( ( f)) (s fun s dom s = dom f) THEN rewrite_tac[]); type_of Image; delete_const ; y *)

 xl-holconst : 'a GS 'a GS f fun f (e e ( f) dom e = dom f e f) f Galaxy f
Proof Context
Proof Context

 xl-sml commit_pc "gst-sumprod";