equal
deleted
inserted
replaced
21 val type_elims = [SigmaE2]); |
21 val type_elims = [SigmaE2]); |
22 |
22 |
23 val listn_induct = standard |
23 val listn_induct = standard |
24 (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp)); |
24 (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp)); |
25 |
25 |
26 val [major] = goal ListN.thy "l:list(A) ==> <length(l),l> : listn(A)"; |
26 goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)"; |
27 by (rtac (major RS List.induct) 1); |
27 by (etac List.induct 1); |
28 by (ALLGOALS (asm_simp_tac list_ss)); |
28 by (ALLGOALS (asm_simp_tac list_ss)); |
29 by (REPEAT (ares_tac ListN.intrs 1)); |
29 by (REPEAT (ares_tac ListN.intrs 1)); |
30 val list_into_listn = result(); |
30 val list_into_listn = result(); |
31 |
31 |
32 goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n"; |
32 goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n"; |
45 by (rtac lfp_mono 1); |
45 by (rtac lfp_mono 1); |
46 by (REPEAT (rtac ListN.bnd_mono 1)); |
46 by (REPEAT (rtac ListN.bnd_mono 1)); |
47 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
47 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
48 val listn_mono = result(); |
48 val listn_mono = result(); |
49 |
49 |
|
50 goal ListN.thy |
|
51 "!!n l. [| <n,l> : listn(A); <n',l'> : listn(A) |] ==> \ |
|
52 \ <n#+n', l@l'> : listn(A)"; |
|
53 by (etac listn_induct 1); |
|
54 by (ALLGOALS (asm_simp_tac (list_ss addsimps ListN.intrs))); |
|
55 val listn_append = result(); |
|
56 |
50 val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)" |
57 val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)" |
51 and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)"; |
58 and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)"; |
52 |
|