equal
deleted
inserted
replaced
4 New proofs/tactics by Brian Huffman |
4 New proofs/tactics by Brian Huffman |
5 |
5 |
6 Proof generator for domain section. |
6 Proof generator for domain section. |
7 *) |
7 *) |
8 |
8 |
|
9 val HOLCF_ss = simpset(); |
9 |
10 |
10 structure Domain_Theorems = struct |
11 structure Domain_Theorems = struct |
11 |
12 |
12 local |
13 local |
13 |
14 |
231 @(if con=c andalso ((List.nth(vns,n)) mem nlas) |
232 @(if con=c andalso ((List.nth(vns,n)) mem nlas) |
232 then[case_UU_tac (when_rews @ con_stricts) 1 |
233 then[case_UU_tac (when_rews @ con_stricts) 1 |
233 (List.nth(vns,n))] else []) |
234 (List.nth(vns,n))] else []) |
234 @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons; |
235 @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons; |
235 in List.concat(map (fn (c,args) => |
236 in List.concat(map (fn (c,args) => |
236 List.concat(List.mapPartial Id (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end; |
237 List.concat(List.mapPartial I (mapn (fn n => fn arg => Option.map (one_sel c n) (sel_of arg)) 0 args))) cons) end; |
237 val sel_defins = if length cons=1 then List.mapPartial (fn arg => Option.map (fn sel => pg [](defined(%:x_name)==> |
238 val sel_defins = if length cons=1 then List.mapPartial (fn arg => Option.map (fn sel => pg [](defined(%:x_name)==> |
238 defined(%%:sel`%x_name)) [ |
239 defined(%%:sel`%x_name)) [ |
239 rtac casedist 1, |
240 rtac casedist 1, |
240 contr_tac 1, |
241 contr_tac 1, |
241 DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac |
242 DETERM_UNTIL_SOLVED (CHANGED(asm_simp_tac |
440 (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) |
441 (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) |
441 ) o snd) cons; |
442 ) o snd) cons; |
442 fun all_rec_to ns = rec_to forall not all_rec_to ns; |
443 fun all_rec_to ns = rec_to forall not all_rec_to ns; |
443 fun warn (n,cons) = if all_rec_to [] false (n,cons) then (warning |
444 fun warn (n,cons) = if all_rec_to [] false (n,cons) then (warning |
444 ("domain "^List.nth(dnames,n)^" is empty!"); true) else false; |
445 ("domain "^List.nth(dnames,n)^" is empty!"); true) else false; |
445 fun lazy_rec_to ns = rec_to exists Id lazy_rec_to ns; |
446 fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns; |
446 |
447 |
447 in val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; |
448 in val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; |
448 val is_emptys = map warn n__eqs; |
449 val is_emptys = map warn n__eqs; |
449 val is_finite = forall (not o lazy_rec_to [] false) n__eqs; |
450 val is_finite = forall (not o lazy_rec_to [] false) n__eqs; |
450 end; |
451 end; |