20 where "white == inr(inl(one))" |
20 where "white == inr(inl(one))" |
21 |
21 |
22 definition blue :: "i" |
22 definition blue :: "i" |
23 where "blue == inr(inr(one))" |
23 where "blue == inr(inr(one))" |
24 |
24 |
25 definition ccase :: "[i,i,i,i]=>i" |
25 definition ccase :: "[i,i,i,i]\<Rightarrow>i" |
26 where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))" |
26 where "ccase(c,r,w,b) == when(c, \<lambda>x. r, \<lambda>wb. when(wb, \<lambda>x. w, \<lambda>x. b))" |
27 |
27 |
28 definition flag :: "i" |
28 definition flag :: "i" |
29 where |
29 where |
30 "flag == lam l. letrec |
30 "flag == lam l. letrec |
31 flagx l be lcase(l,<[],<[],[]>>, |
31 flagx l be lcase(l,<[],<[],[]>>, |
32 %h t. split(flagx(t),%lr p. split(p,%lw lb. |
32 \<lambda>h t. split(flagx(t), \<lambda>lr p. split(p, \<lambda>lw lb. |
33 ccase(h, <red$lr,<lw,lb>>, |
33 ccase(h, <red$lr,<lw,lb>>, |
34 <lr,<white$lw,lb>>, |
34 <lr,<white$lw,lb>>, |
35 <lr,<lw,blue$lb>>)))) |
35 <lr,<lw,blue$lb>>)))) |
36 in flagx(l)" |
36 in flagx(l)" |
37 |
37 |
38 axiomatization Perm :: "i => i => o" |
38 axiomatization Perm :: "i \<Rightarrow> i \<Rightarrow> o" |
39 definition Flag :: "i => i => o" where |
39 definition Flag :: "i \<Rightarrow> i \<Rightarrow> o" where |
40 "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). |
40 "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). |
41 x = <lr,<lw,lb>> --> |
41 x = <lr,<lw,lb>> \<longrightarrow> |
42 (ALL c:Colour.(c mem lr = true --> c=red) & |
42 (ALL c:Colour.(c mem lr = true \<longrightarrow> c=red) \<and> |
43 (c mem lw = true --> c=white) & |
43 (c mem lw = true \<longrightarrow> c=white) \<and> |
44 (c mem lb = true --> c=blue)) & |
44 (c mem lb = true \<longrightarrow> c=blue)) \<and> |
45 Perm(l,lr @ lw @ lb)" |
45 Perm(l,lr @ lw @ lb)" |
46 |
46 |
47 |
47 |
48 lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def |
48 lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def |
49 |
49 |
50 lemma ColourXH: "a : Colour <-> (a=red | a=white | a=blue)" |
50 lemma ColourXH: "a : Colour \<longleftrightarrow> (a=red | a=white | a=blue)" |
51 unfolding simp_type_defs flag_defs by blast |
51 unfolding simp_type_defs flag_defs by blast |
52 |
52 |
53 lemma redT: "red : Colour" |
53 lemma redT: "red : Colour" |
54 and whiteT: "white : Colour" |
54 and whiteT: "white : Colour" |
55 and blueT: "blue : Colour" |
55 and blueT: "blue : Colour" |
56 unfolding ColourXH by blast+ |
56 unfolding ColourXH by blast+ |
57 |
57 |
58 lemma ccaseT: |
58 lemma ccaseT: |
59 "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] |
59 "\<lbrakk>c:Colour; c=red \<Longrightarrow> r : C(red); c=white \<Longrightarrow> w : C(white); c=blue \<Longrightarrow> b : C(blue)\<rbrakk> |
60 ==> ccase(c,r,w,b) : C(c)" |
60 \<Longrightarrow> ccase(c,r,w,b) : C(c)" |
61 unfolding flag_defs by ncanT |
61 unfolding flag_defs by ncanT |
62 |
62 |
63 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" |
63 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" |
64 apply (unfold flag_def) |
64 apply (unfold flag_def) |
65 apply (typechk redT whiteT blueT ccaseT) |
65 apply (typechk redT whiteT blueT ccaseT) |