src/CCL/ex/Flag.thy
author wenzelm
Sat, 25 May 2013 17:40:44 +0200
changeset 52147 9943f8067f11
parent 42155 ffe99b07c9c0
child 58889 5b7a9633cfa8
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     1
(*  Title:      CCL/ex/Flag.thy
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 1149
diff changeset
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     6
header {* Dutch national flag program -- except that the point of Dijkstra's example was to use
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     7
  arrays and this uses lists. *}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     8
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
     9
theory Flag
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    10
imports List
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    11
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    31
      flagx l be lcase(l,<[],<[],[]>>,
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    32
                       %h t. split(flagx(t),%lr p. split(p,%lw lb.
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    33
                            ccase(h, <red$lr,<lw,lb>>,
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    34
                                     <lr,<white$lw,lb>>,
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    35
                                     <lr,<lw,blue$lb>>))))
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    36
      in flagx(l)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    47
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    48
lemmas flag_defs = Colour_def red_def white_def blue_def ccase_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    49
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    50
lemma ColourXH: "a : Colour <-> (a=red | a=white | a=blue)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    51
  unfolding simp_type_defs flag_defs by blast
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    52
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    53
lemma redT: "red : Colour"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    54
  and whiteT: "white : Colour"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    55
  and blueT: "blue : Colour"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    56
  unfolding ColourXH by blast+
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    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
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    62
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    63
lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    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
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    68
  apply (erule ListPRI [THEN ListPR_wf [THEN wfI]])
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    69
  apply assumption
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    70
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    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
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    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
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 17456
diff changeset
    76
  oops
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 3837
diff changeset
    78
end