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"];
|
|
|
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.
|
|
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.
|
|
|
Proof Context
xl-sml
commit_pc "gst-sumprod";
|
|
|