author | wenzelm |
Sat, 12 Jan 2013 14:53:56 +0100 | |
changeset 50843 | 1465521b92a1 |
parent 42155 | ffe99b07c9c0 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
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 |