src/CCL/ex/flag.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	CCL/ex/flag
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For flag.thy.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open Flag;
clasohm@0
    10
clasohm@0
    11
(******)
clasohm@0
    12
clasohm@0
    13
val flag_defs = [Colour_def,red_def,white_def,blue_def,ccase_def];
clasohm@0
    14
clasohm@0
    15
(******)
clasohm@0
    16
clasohm@0
    17
val ColourXH = mk_XH_tac Flag.thy (simp_type_defs @flag_defs) [] 
clasohm@0
    18
          "a : Colour <-> (a=red | a=white | a=blue)";
clasohm@0
    19
clasohm@0
    20
val Colour_case = XH_to_E ColourXH;
clasohm@0
    21
clasohm@0
    22
val redT = mk_canT_tac Flag.thy [ColourXH] "red : Colour";
clasohm@0
    23
val whiteT = mk_canT_tac Flag.thy [ColourXH] "white : Colour";
clasohm@0
    24
val blueT = mk_canT_tac Flag.thy [ColourXH] "blue : Colour";
clasohm@0
    25
clasohm@0
    26
clasohm@0
    27
val ccaseT = mk_ncanT_tac Flag.thy flag_defs case_rls case_rls
clasohm@0
    28
     "[| c:Colour; \
clasohm@0
    29
\        c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> \
clasohm@0
    30
\     ccase(c,r,w,b) : C(c)";
clasohm@0
    31
clasohm@0
    32
(***)
clasohm@0
    33
clasohm@0
    34
val prems = goalw Flag.thy [flag_def]
clasohm@0
    35
    "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)";
clasohm@0
    36
by (typechk_tac [redT,whiteT,blueT,ccaseT] 1);
clasohm@0
    37
by clean_ccs_tac;
clasohm@0
    38
be (ListPRI RS (ListPR_wf RS wfI)) 1;
clasohm@0
    39
ba 1;
clasohm@0
    40
result();
clasohm@0
    41
clasohm@0
    42
clasohm@0
    43
val prems = goalw Flag.thy [flag_def]
clasohm@0
    44
    "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}";
clasohm@0
    45
by (gen_ccs_tac [redT,whiteT,blueT,ccaseT] 1);
clasohm@0
    46
by (REPEAT_SOME (ares_tac [ListPRI RS (ListPR_wf RS wfI)]));