|
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 {*
|
|
|
59 |
bind_thm ("ccaseT", mk_ncanT_tac (the_context ())
|
|
|
60 |
(thms "flag_defs") (thms "case_rls") (thms "case_rls")
|
|
|
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)
|
|
|
67 |
apply (tactic {* typechk_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *})
|
|
|
68 |
apply (tactic clean_ccs_tac)
|
|
|
69 |
apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
|
|
|
70 |
apply assumption
|
|
|
71 |
done
|
|
|
72 |
|
|
|
73 |
lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"
|
|
|
74 |
apply (unfold flag_def)
|
|
|
75 |
apply (tactic {* gen_ccs_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *})
|
|
|
76 |
oops
|
|
0
|
77 |
|
|
17456
|
78 |
end
|