src/CCL/ex/Flag.thy
author wenzelm
Sat Jun 14 23:52:51 2008 +0200 (2008-06-14)
changeset 27221 31328dc30196
parent 23894 1a4167d761ac
child 28272 ed959a0f650b
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
     1 (*  Title:      CCL/ex/Flag.thy
     2     ID:         $Id$
     3     Author:     Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 *)
     6 
     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
    13 
    14 consts
    15   Colour             :: "i set"
    16   red                :: "i"
    17   white              :: "i"
    18   blue               :: "i"
    19   ccase              :: "[i,i,i,i]=>i"
    20   flag               :: "i"
    21 
    22 axioms
    23 
    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))"
    28 
    29   ccase_def:   "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
    30 
    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)"
    38 
    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)) &
    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 ML {*
    59 bind_thm ("ccaseT", mk_ncanT_tac @{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 @{context}
    68     [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
    69   apply (tactic "clean_ccs_tac @{context}")
    70   apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
    71   apply assumption
    72   done
    73 
    74 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}"
    75   apply (unfold flag_def)
    76   apply (tactic {* gen_ccs_tac @{context}
    77     [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *})
    78   oops
    79 
    80 end