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