1(*  Title:      CCL/ex/Flag.thy
2    Author:     Martin Coen, Cambridge University Computer Laboratory
3    Copyright   1993  University of Cambridge
4*)
5
6section \<open>Dutch national flag program -- except that the point of Dijkstra's example was to use
7  arrays and this uses lists.\<close>
8
9theory Flag
10imports List
11begin
12
13definition Colour :: "i set"
14  where "Colour == Unit + Unit + Unit"
15
16definition red :: "i"
17  where "red == inl(one)"
18
19definition white :: "i"
20  where "white == inr(inl(one))"
21
22definition blue :: "i"
23  where "blue == inr(inr(one))"
24
25definition ccase :: "[i,i,i,i]\<Rightarrow>i"
26  where "ccase(c,r,w,b) == when(c, \<lambda>x. r, \<lambda>wb. when(wb, \<lambda>x. w, \<lambda>x. b))"
27
28definition flag :: "i"
29  where
30    "flag == lam l. letrec
31      flagx l be lcase(l,<[],<[],[]>>,
32                       \<lambda>h t. split(flagx(t), \<lambda>lr p. split(p, \<lambda>lw lb.
33                            ccase(h, <red$lr,<lw,lb>>,
34                                     <lr,<white$lw,lb>>,
35                                     <lr,<lw,blue$lb>>))))
36      in flagx(l)"
37
38axiomatization Perm :: "i \<Rightarrow> i \<Rightarrow> o"
39definition Flag :: "i \<Rightarrow> i \<Rightarrow> o" where
40  "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour).
41                x = <lr,<lw,lb>> \<longrightarrow>
42              (ALL c:Colour.(c mem lr = true \<longrightarrow> c=red) \<and>
43                            (c mem lw = true \<longrightarrow> c=white) \<and>
44                            (c mem lb = true \<longrightarrow> c=blue)) \<and>
45              Perm(l,lr @ lw @ lb)"
46
47
48lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def
49
50lemma ColourXH: "a : Colour \<longleftrightarrow> (a=red | a=white | a=blue)"
51  unfolding simp_type_defs flag_defs by blast
52
53lemma redT: "red : Colour"
54  and whiteT: "white : Colour"
55  and blueT: "blue : Colour"
56  unfolding ColourXH by blast+
57
58lemma ccaseT:
59  "\<lbrakk>c:Colour; c=red \<Longrightarrow> r : C(red); c=white \<Longrightarrow> w : C(white); c=blue \<Longrightarrow> b : C(blue)\<rbrakk>
60    \<Longrightarrow> ccase(c,r,w,b) : C(c)"
61  unfolding flag_defs by ncanT
62
63lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
64  apply (unfold flag_def)
65  apply (typechk redT whiteT blueT ccaseT)
66  apply clean_ccs
67  apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
68  apply assumption
69  done
70
71lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}"
72  apply (unfold flag_def)
73  apply (gen_ccs redT whiteT blueT ccaseT)
74  oops
75
76end
77