A new "gst-rec" theory is created as a child of "gst-fun". Probably

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"];

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)

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)

xl-sml commit_pc "gst-sumprod";