Definitions for pure functions.
Overview
This document defines the concept of a pure function as a preliminary to introducing the type of pure functions.
Here we define and show the consistency of the concept of a "pure function".
In this section we define function application and show that the pure functions are extensional.
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-holconst
pf_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-holconst
pure_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

up quick index © RBJ

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