author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 32153  a0e57fb1b930 
child 42155  ffe99b07c9c0 
permissions  rwrr 
17456  1 
(* Title: CCL/ex/Flag.thy 
1474  2 
Author: Martin Coen, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

17456  6 
header {* Dutch national flag program  except that the point of Dijkstra's example was to use 
7 
arrays and this uses lists. *} 

8 

9 
theory Flag 

10 
imports List 

11 
begin 

0  12 

13 
consts 

14 
Colour :: "i set" 

17456  15 
red :: "i" 
16 
white :: "i" 

17 
blue :: "i" 

0  18 
ccase :: "[i,i,i,i]=>i" 
19 
flag :: "i" 

20 

17456  21 
axioms 
0  22 

17456  23 
Colour_def: "Colour == Unit + Unit + Unit" 
24 
red_def: "red == inl(one)" 

25 
white_def: "white == inr(inl(one))" 

26 
blue_def: "blue == inr(inr(one))" 

0  27 

17456  28 
ccase_def: "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))" 
0  29 

17456  30 
flag_def: "flag == lam l. letrec 
31 
flagx l be lcase(l,<[],<[],[]>>, 

32 
%h t. split(flagx(t),%lr p. split(p,%lw lb. 

33 
ccase(h, <red$lr,<lw,lb>>, 

34 
<lr,<white$lw,lb>>, 

35 
<lr,<lw,blue$lb>>)))) 

36 
in flagx(l)" 

0  37 

17456  38 
Flag_def: 
39 
"Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). 

40 
x = <lr,<lw,lb>> > 

41 
(ALL c:Colour.(c mem lr = true > c=red) & 

42 
(c mem lw = true > c=white) & 

43 
(c mem lb = true > c=blue)) & 

1149  44 
Perm(l,lr @ lw @ lb)" 
0  45 

20140  46 

47 
lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def 

48 

49 
lemma ColourXH: "a : Colour <> (a=red  a=white  a=blue)" 

50 
unfolding simp_type_defs flag_defs by blast 

51 

52 
lemma redT: "red : Colour" 

53 
and whiteT: "white : Colour" 

54 
and blueT: "blue : Colour" 

55 
unfolding ColourXH by blast+ 

56 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
28272
diff
changeset

57 
lemma ccaseT: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
28272
diff
changeset

58 
"[ c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) ] 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
28272
diff
changeset

59 
==> ccase(c,r,w,b) : C(c)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
28272
diff
changeset

60 
unfolding flag_defs by ncanT 
20140  61 

62 
lemma "flag : List(Colour)>List(Colour)*List(Colour)*List(Colour)" 

63 
apply (unfold flag_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

64 
apply (tactic {* typechk_tac @{context} 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

65 
[@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

66 
apply (tactic "clean_ccs_tac @{context}") 
20140  67 
apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) 
68 
apply assumption 

69 
done 

70 

71 
lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}" 

72 
apply (unfold flag_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

73 
apply (tactic {* gen_ccs_tac @{context} 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

74 
[@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) 
20140  75 
oops 
0  76 

17456  77 
end 