equal
deleted
inserted
replaced
33 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
33 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
34 qed "listn_mono"; |
34 qed "listn_mono"; |
35 |
35 |
36 Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)"; |
36 Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)"; |
37 by (etac listn.induct 1); |
37 by (etac listn.induct 1); |
38 by (ALLGOALS (asm_simp_tac (simpset() addsimps listn.intrs))); |
38 by (ftac (impOfSubs listn.dom_subset) 1); |
|
39 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs))); |
39 qed "listn_append"; |
40 qed "listn_append"; |
40 |
41 |
41 val Nil_listn_case = listn.mk_cases "<i,Nil> : listn(A)" |
42 val Nil_listn_case = listn.mk_cases "<i,Nil> : listn(A)" |
42 and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> : listn(A)"; |
43 and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> : listn(A)"; |
43 |
44 |