17456
|
1 |
(* Title: CCL/ex/Flag.ML
|
0
|
2 |
ID: $Id$
|
1459
|
3 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
0
|
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 |
|
17456
|
13 |
val ColourXH = mk_XH_tac (the_context ()) (simp_type_defs @flag_defs) []
|
0
|
14 |
"a : Colour <-> (a=red | a=white | a=blue)";
|
|
15 |
|
|
16 |
val Colour_case = XH_to_E ColourXH;
|
|
17 |
|
17456
|
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";
|
0
|
21 |
|
|
22 |
|
17456
|
23 |
val ccaseT = mk_ncanT_tac (the_context ()) flag_defs case_rls case_rls
|
0
|
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 |
|
17456
|
30 |
val prems = goalw (the_context ()) [flag_def]
|
0
|
31 |
"flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)";
|
|
32 |
by (typechk_tac [redT,whiteT,blueT,ccaseT] 1);
|
|
33 |
by clean_ccs_tac;
|
1459
|
34 |
by (etac (ListPRI RS (ListPR_wf RS wfI)) 1);
|
|
35 |
by (assume_tac 1);
|
0
|
36 |
result();
|
|
37 |
|
|
38 |
|
17456
|
39 |
val prems = goalw (the_context ()) [flag_def]
|
0
|
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)]));
|