ZF/func: tidied many proofs, using new definition of Pi(A,B)
ZF/func/PiI,PiE: removed
ZF/func/Pi_iff_old: new
ZF/func/Pi_memberD: new; simpler, replaces memberPiE
(* Title: CCL/ex/flag.thy
ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Dutch national flag program - except that the point of Dijkstra's example was to use
arrays and this uses lists.
*)
Flag = List +
consts
Colour :: "i set"
red, white, blue :: "i"
ccase :: "[i,i,i,i]=>i"
flag :: "i"
rules
Colour_def "Colour == Unit + Unit + Unit"
red_def "red == inl(one)"
white_def "white == inr(inl(one))"
blue_def "blue == inr(inr(one))"
ccase_def "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
flag_def "flag == lam l.letrec \
\ flagx l be lcase(l,<[],<[],[]>>, \
\ %h t. split(flagx(t),%lr p.split(p,%lw lb. \
\ ccase(h, <red$lr,<lw,lb>>, \
\ <lr,<white$lw,lb>>, \
\ <lr,<lw,blue$lb>>)))) \
\ in flagx(l)"
Flag_def
"Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). \
\ x = <lr,<lw,lb>> --> \
\ (ALL c:Colour.(c mem lr = true --> c=red) & \
\ (c mem lw = true --> c=white) & \
\ (c mem lb = true --> c=blue)) & \
\ Perm(l,lr @ lw @ lb)"
end