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 ⇒
fttab(∀e• e ∈g (Σ f) ≡
fttabfttab∃i v• e = i ↦g v
fttabfttab∧ i ∈g dom f
fttabfttab∧ v ∈g f g i)
⌝);
a (∃_tac ⌜λf• ⋃g (
fttabImagep
fttab(λi• Imagep (λv• i ↦g v) (f g i))
fttab(dom f))⌝
fttabTHEN rewrite_tac[]);
a (REPEAT strip_tac);
(* *** Goal "1" *** *)
a (asm_ante_tac ⌜e ∈g e'⌝
fttabTHEN asm_rewrite_tac[]
fttabTHEN (REPEAT strip_tac));
a (∃_tac ⌜e''⌝ THEN ∃_tac ⌜e'''⌝
fttabTHEN asm_prove_tac[]);
(* *** Goal "2" *** *)
a (∃_tac ⌜Imagep (λ v• i ↦g v) (f g i)⌝
fttabTHEN asm_prove_tac[]);
xl_set_cs_∃_thm (pop_thm ());


xl-holconst
Σ : GS → GS
∀f• fun f ⇒
fttab(∀e• e ∈g (Σ f) ≡
fttabfttab∃i v• e = i ↦g v
fttabfttab∧ i ∈g dom f
fttabfttab∧ 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 ⇒
fttab(∀e• e ∈g (Π f) ≡
fttabfttabdom e = dom f
fttabfttab∧ e ⊆g Σ f)
⌝);
a (∃_tac ⌜λf•
fttabfttabSep
fttabfttab(℘ (Σ f))
fttabfttab(λs• fun s ∧ dom s = dom f)⌝
fttabTHEN rewrite_tac[]);

type_of ⌜Imagep⌝;
delete_const ⌜Σ⌝;
y
*)


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

xl-sml
commit_pc "gst-sumprod";


up quick index © RBJ

privacy policy

Created:

$Id: SumsAndProducts.xml,v 1.1 2002/12/24 16:02:49 rbj Exp $

V