equal
deleted
inserted
replaced
39 goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}"; |
39 goal ListN.thy "listn(A)``{n} = {l:list(A). length(l)=n}"; |
40 by (rtac equality_iffI 1); |
40 by (rtac equality_iffI 1); |
41 by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1); |
41 by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1); |
42 val listn_image_eq = result(); |
42 val listn_image_eq = result(); |
43 |
43 |
|
44 goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)"; |
|
45 by (rtac lfp_mono 1); |
|
46 by (REPEAT (rtac ListN.bnd_mono 1)); |
|
47 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
|
48 val listn_mono = result(); |
|
49 |