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