60 ==> ccase(c,r,w,b) : C(c)" |
60 ==> ccase(c,r,w,b) : C(c)" |
61 unfolding flag_defs by ncanT |
61 unfolding flag_defs by ncanT |
62 |
62 |
63 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" |
63 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" |
64 apply (unfold flag_def) |
64 apply (unfold flag_def) |
65 apply (tactic {* typechk_tac @{context} |
65 apply (typechk redT whiteT blueT ccaseT) |
66 [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) |
66 apply clean_ccs |
67 apply (tactic "clean_ccs_tac @{context}") |
|
68 apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) |
67 apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) |
69 apply assumption |
68 apply assumption |
70 done |
69 done |
71 |
70 |
72 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}" |
71 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).Flag(x,l)}" |
73 apply (unfold flag_def) |
72 apply (unfold flag_def) |
74 apply (tactic {* gen_ccs_tac @{context} |
73 apply (gen_ccs redT whiteT blueT ccaseT) |
75 [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) |
|
76 oops |
74 oops |
77 |
75 |
78 end |
76 end |