author  wenzelm 
Sun, 30 Nov 2008 14:43:29 +0100  
changeset 28917  20f43e0e0958 
parent 28272  ed959a0f650b 
child 32153  a0e57fb1b930 
permissions  rwrr 
17456  1 
(* Title: CCL/ex/Flag.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Martin Coen, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 
*) 

6 

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

9 

10 
theory Flag 

11 
imports List 

12 
begin 

0  13 

14 
consts 

15 
Colour :: "i set" 

17456  16 
red :: "i" 
17 
white :: "i" 

18 
blue :: "i" 

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

21 

17456  22 
axioms 
0  23 

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

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

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

0  28 

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

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

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

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

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

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

37 
in flagx(l)" 

0  38 

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

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

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

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

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

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

20140  47 

48 
lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def 

49 

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

51 
unfolding simp_type_defs flag_defs by blast 

52 

53 
lemma redT: "red : Colour" 

54 
and whiteT: "white : Colour" 

55 
and blueT: "blue : Colour" 

56 
unfolding ColourXH by blast+ 

57 

58 
ML {* 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

59 
bind_thm ("ccaseT", mk_ncanT_tac @{context} 
28272
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
27221
diff
changeset

60 
@{thms flag_defs} @{thms case_rls} @{thms case_rls} 
20140  61 
"[ c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) ] ==> ccase(c,r,w,b) : C(c)"); 
62 
*} 

63 

64 

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

66 
apply (unfold flag_def) 

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

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

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

69 
apply (tactic "clean_ccs_tac @{context}") 
20140  70 
apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) 
71 
apply assumption 

72 
done 

73 

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

75 
apply (unfold flag_def) 

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

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

77 
[@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) 
20140  78 
oops 
0  79 

17456  80 
end 