Definitions for pure functions.
Overview
 This document defines the concept of a pure function as a preliminary to introducing the type of pure functions.
 The definition of a Pure Function Here we define and show the consistency of the concept of a "pure function".
 Application and Extensionality In this section we define function application and show that the pure functions are extensional. The Theory pf
The definition of a Pure Function
 Here we define and show the consistency of the concept of a "pure function".
The Theory pf
First we introduce for these definitions the new theory "pf", a child of zfc.
 xl-sml open_theory "zfc"; set_pc "basic_hol"; delete_theory"pf" handle _ => (); new_theory"pf";

hereditary properties
A property of sets is "pf_hered" if a function inherits this property from the sets in its field. i.e. if all functions over a field of pf_hered sets are themselves pf_hered.
 xl-holconstpf_hered : (SETzBOOL)BOOL p pf_hered p s (e e z (fieldz s) p e) funz s p s
pf_hereditary
A pure function is a function which has all the pf_hereditary properties. This is an oblique way of saying that the function can be constructed from the empty set by a process which involves only the formation of functions from functions already constructed.
 xl-holconstpure_function : SETzBOOL s pure_function s p pf_hered p p s
consistency proof
We now prove that there exists a pure function.
 xl-sml set_goal([],pure_function z); a (prove_tac [ get_spec pure_function, get_spec pf_hered ]); a (spec_nth_asm_tac 1 z THEN (asm_prove_tac [ get_spec pure_function, get_spec pf_hered, z_thm, funz_z_thm, fieldz_z_thm ])); val pure_function_z = save_pop_thm "pure_function_z";

 xl-sml set_goal([],x pure_function x); a (_tac z); a (prove_tac [pure_function_z]); val pure_function_exists = save_pop_thm "pure_function_exists"; val pf_def = new_type_defn (["PF","pf_def"],"PF",[], pure_function_exists);

Application and Extensionality
 In this section we define function application and show that the pure functions are extensional.
 Application

©

\$Id: pf-defns.xml,v 1.1.1.1 2000/12/04 17:24:45 rbjones Exp \$