equal
deleted
inserted
replaced
62 *} |
62 *} |
63 |
63 |
64 |
64 |
65 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" |
65 lemma "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)" |
66 apply (unfold flag_def) |
66 apply (unfold flag_def) |
67 apply (tactic {* typechk_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *}) |
67 apply (tactic {* typechk_tac @{context} |
68 apply (tactic clean_ccs_tac) |
68 [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) |
|
69 apply (tactic "clean_ccs_tac @{context}") |
69 apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) |
70 apply (erule ListPRI [THEN ListPR_wf [THEN wfI]]) |
70 apply assumption |
71 apply assumption |
71 done |
72 done |
72 |
73 |
73 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}" |
74 lemma "flag : PROD l:List(Colour).{x:List(Colour)*List(Colour)*List(Colour).FLAG(x,l)}" |
74 apply (unfold flag_def) |
75 apply (unfold flag_def) |
75 apply (tactic {* gen_ccs_tac [thm "redT", thm "whiteT", thm "blueT", thm "ccaseT"] 1 *}) |
76 apply (tactic {* gen_ccs_tac @{context} |
|
77 [@{thm redT}, @{thm whiteT}, @{thm blueT}, @{thm ccaseT}] 1 *}) |
76 oops |
78 oops |
77 |
79 |
78 end |
80 end |