|
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)])); |