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