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