(see section 7.1) and at the same time we must use reduction tactics in order to type check arguments of functions before reduction is conducted. Here LCF simply use rewriting which does -conversion behind the scenes.
|- !D E h x s.
h ins (cf(D,cf(seq D,E))) ==>
x ins D ==>
s ins (seq D) ==>
(Seq_when h(Cons_seq x s) = h x s)
which have been derived from its denition. The continuity theorems about Cons seq and Seq when are used to declare these functions as constructors as follows
#declare_constructor Cons_seq_CF
|- !D. cpo D ==> Cons_seq ins (cf(D,cf(seq D,seq D)))
#declare_constructor Seq_when_CF
|- !D E.
cpo D ==>
pcpo E ==>
Seq_when ins (cf(cf(D,cf(seq D,E)),cf(seq D,E)))
We also showed that we can do structural induction proofs on sequences.
|- !D P.
cpo D ==>
inclusive(P,seq D) ==>
P Bt_seq ==>
(!x s'. x ins D ==> P s' ==> P(Cons_seq x s')) ==>
(!s. s ins (seq D) ==> P s)
A structural induction tactic has been implemented on top of this theorem which uses the cpo prover and the inclusive prover behind the scenes.
Again we start up a new session and a new theory, assuming the above declarations.
Then we assume the variables D and E are cpos, binding these assumptions to ML variables for later use.
#new_theory`lcf_seq`
() : void
#cpo1
":(*1 -> bool) # (*1 -> *1 -> bool)" : type
#cpo2
":(*2 -> bool) # (*2 -> *2 -> bool)" : type
#let D_CPO = ASSUME"cpo(D:^cpo1)"
D_CPO = . |- cpo D
#let E_CPO = ASSUME"cpo(E:^cpo2)"
E_CPO = . |- cpo E
We shall use the assumptions to dene the functional for the mapping function and the mapping function Maps itself, or more precisely, to prove these functions are continuous.
The functional used to dene Maps is introduced as a constructor as follows
#new_constructor_definition`Maps_FUN_DEF``Maps_FUN_CF`D_CPOE_CPO]
#"Maps_FUNI(D:^cpo1,E:^cpo2) =
# (\g::Dom(cf(cf(D,E),cf(seq D,seq E))).
# \f::Dom(cf(D,E)).
# \s::Dom(seq D).
# Seq_when(\x::Dom D.\t::Dom(seq D). Cons_seq(f x)(g f t))s)"
|- !D E.
Maps_FUN =
(\g :: Dom(cf(cf(D,E),cf(seq D,seq E))).
\f :: Dom(cf(D,E)).
\s :: Dom(seq D).
Seq_when(\x :: Dom D. \t :: Dom(seq D). Cons_seq(f x)(g f t))s)
|- !D E.
cpo D ==>
cpo E ==>
Maps_FUN ins
(cf(cf(cf(D,E),cf(seq D,seq E)),cf(cf(D,E),cf(seq D,seq E))))
The program new constructor definition denes two constants, one for the internal level of syntax which is the one used in the term argument, and one for the external level of syntax which is the one used in the pretty-printed denition and continuity theorem output. The latter is not parameterized by cpos.
We can now use Maps FUN whenever the cpo arguments of the internal version can be calculated from the context (i.e. from the arguments of Maps FUN) and it will always occur in pretty-printed results. The mapping functional is dened as the xed point of this functional.
#new_constructor_definition`Maps_DEF``Maps_CF`D_CPOE_CPO]
#"MapsI(D:^cpo1,E:^cpo2) = Fix(Maps_FUNI(D,E))"
|- !D E. Maps = Fix Maps_FUN
|- !D E.
cpo D ==> cpo E ==> Maps ins (cf(cf(D,E),cf(seq D,seq E)))
In this denition we have a situation where we cannot determine the cpo arguments of the internal version of Maps FUN from the context (it has no arguments) and we must therefore write the cpos explicitly (hence we use Maps FUNI ).
It is not immediatelyobvious from the denition of Maps how it actually works on the dierent kinds of sequences. We have therefore proved two reduction theorems (recursion equations).
|- !D E f. f ins (cf(D,E)) ==> (Maps f Bt_seq = Bt_seq)
|- !D E f x s.
f ins (cf(D,E)) ==>
x ins D ==>
s ins (seq D) ==>
(Maps f(Cons_seq x s) = Cons_seq(f x)(Maps f s))
These are proved easily by using that Maps is a xed point of the functional Maps FUN. We can now prove that the mapping functional preserves functional composition (de-ned in section 3.7).
|- !D1 D2 D3 f g.
f ins (cf(D2,D3)) ==>
g ins (cf(D1,D2)) ==>
(Maps(Comp(f,g)) = Comp(Maps f,Maps g))
Setting this statement as a goal in the subgoal package, we rst strip the antecents and then observe that the two continuous functions are equal i they are equal for all sequences of elements in D1, i.e. i the following term holds
"!s. s ins (seq D1) ==> (Maps(Comp(f,g))s = Comp(Maps f,Maps g)s)"
This goal is obtained from a goal stating equality of the functions using the program
X CONT FUN EQ TAC, which was described in section 5.6.6.
Next, we use a structural induction tactic for sequences based directly on the structural induction theorem.
#e(SEQ_INDUCT_TAC]]]) OK..
2 subgoals
"!x s.
x ins D1 ==>
s ins (seq D1) ==>
(Maps(Comp(f,g))s = Comp(Maps f,Maps g)s) ==>
(Maps(Comp(f,g))(Scons x s) = Comp(Maps f,Maps g)(Scons x s))"
"cpo D1" ] "cpo D2" ] "cpo D3" ]
"f ins (cf(D2,D3))" ] "g ins (cf(D1,D2))" ]
"Maps(Comp(f,g))Sbt = Comp(Maps f,Maps g)Sbt"
"cpo D1" ] "cpo D2" ] "cpo D3" ]
"f ins (cf(D2,D3))" ] "g ins (cf(D1,D2))" ] () : void
This uses the inclusive prover behind the scenes so we do not have to worry about proving the above equation admits induction. Note that "seq D1" is non-empty since it is a pointed cpo. The proof is nished o using the reduction tactic with the reduction theorems for Maps and Comp.
Finally, we can dene a functional Seq of which given a continuous function f and any starting point value x generates an innite sequence of the form
"Cons_seq x(Cons_seq(f x)(Cons_seq(f(f x))...))"
or written in a more readable way x f(x) f(f(x)) :::]. This function is the xed point of a functional called Seq of FUN (the external name).
|- !D.
Seq_of_FUN =
(\sf :: Dom(cf(cf(D,D),cf(D,seq D))).
\f :: Dom(cf(D,D)). \x :: Dom D. Cons_seq x(sf f(f x)))
|- !D. Seq_of = Fix Seq_of_FUN
Both are dened using new constructor definition. The continuity theorems re-turned by this program are stated as follows
|- !D.
cpo D ==>
Seq_of_FUN ins
(cf(cf(cf(D,D),cf(D,seq D)),cf(cf(D,D),cf(D,seq D))))
|- !D. cpo D ==> Seq_of ins (cf(cf(D,D),cf(D,seq D)))
It should be apparent from the xed point denition of Seq of that it always computes an innite sequence.
We can now prove the following statement about Seq of and Maps
|- !D f.
cpo D ==>
f ins (cf(D,D)) ==>
(!x. x ins D ==> (Seq_of f(f x) = Maps f(Seq_of f x)))
Informally, the two sequences are equal since they are both equal to a term corresponding to f x f(f x) :::] . The proof of the theorem is conducted by xed point induction on both occurrences of Seq of. But rst the two rst antecedents are stripped o and a case split is performed on whether D is empty or not. If it is then an induction is not necessary since "x ins D" must be false. Otherwise, the remaining predicate is proved to be inclusive (as a function of a variable replacing Seq of ) and xed point induction is conducted. Examples of the use of xed point induction has been given above. We shall not consider the details of this induction proof here.
Again the proofs in our formalization and LCF are based on the same overall idea but tend to be longer in HOL since we do the simplications explicitly whereas LCF rewriting handles many situations. As mentioned above this probably makes LCF rewriting ine-cient at least compared to HOL rewriting but our simplications are quite ineine-cient too, since they do more than just rewriting e.g. they also do type checking.