Indexed Sums and Products in GST
Overview
A new "gst-rec" theory is created as a child of "gst-fun". Probably
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";


up quick index © RBJ

$Id: SumsAndProducts.xml,v 1.1.1.1 2000/12/04 17:23:39 rbjones Exp $