author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 42155  ffe99b07c9c0 
child 58889  5b7a9633cfa8 
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 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

13 
definition Colour :: "i set" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

14 
where "Colour == Unit + Unit + Unit" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

15 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

16 
definition red :: "i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

17 
where "red == inl(one)" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

18 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

19 
definition white :: "i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

20 
where "white == inr(inl(one))" 
0  21 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

22 
definition blue :: "i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

23 
where "blue == inr(inr(one))" 
0  24 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

25 
definition ccase :: "[i,i,i,i]=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

26 
where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))" 
0  27 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

28 
definition flag :: "i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

29 
where 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

30 
"flag == lam l. letrec 
17456  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 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

38 
axiomatization Perm :: "i => i => o" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

39 
definition Flag :: "i => i => o" where 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

40 
"Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

41 
x = <lr,<lw,lb>> > 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

42 
(ALL c:Colour.(c mem lr = true > c=red) & 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

43 
(c mem lw = true > c=white) & 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

44 
(c mem lb = true > c=blue)) & 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

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 

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

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

59 
"[ 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

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

61 
unfolding flag_defs by ncanT 
20140  62 

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

64 
apply (unfold flag_def) 

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

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

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

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

70 
done 

71 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
32153
diff
changeset

72 
lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}" 
20140  73 
apply (unfold flag_def) 
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
23894
diff
changeset

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

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

17456  78 
end 