src/CCL/ex/Flag.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 42155 ffe99b07c9c0
child 58971 8c9a319821b3
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      CCL/ex/Flag.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 section {* 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
    12 
    13 definition Colour :: "i set"
    14   where "Colour == Unit + Unit + Unit"
    15 
    16 definition red :: "i"
    17   where "red == inl(one)"
    18 
    19 definition white :: "i"
    20   where "white == inr(inl(one))"
    21 
    22 definition blue :: "i"
    23   where "blue == inr(inr(one))"
    24 
    25 definition ccase :: "[i,i,i,i]=>i"
    26   where "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
    27 
    28 definition flag :: "i"
    29   where
    30     "flag == lam l. letrec
    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)"
    37 
    38 axiomatization Perm :: "i => i => o"
    39 definition Flag :: "i => i => o" where
    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)) &
    45               Perm(l,lr @ lw @ lb)"
    46 
    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 lemma ccaseT:
    59   "[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |]
    60     ==> ccase(c,r,w,b) : C(c)"
    61   unfolding flag_defs by ncanT
    62 
    63 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
    64   apply (unfold flag_def)
    65   apply (tactic {* typechk_tac @{context}
    66     [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
    67   apply (tactic "clean_ccs_tac @{context}")
    68   apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
    69   apply assumption
    70   done
    71 
    72 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}"
    73   apply (unfold flag_def)
    74   apply (tactic {* gen_ccs_tac @{context}
    75     [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
    76   oops
    77 
    78 end