Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1993 University of Cambridge
6 Datatype definition of Lists
9 structure List = Datatype_Fun
14 (["Cons"], "[i,i]=>i")])];
15 val rec_styp = "i=>i";
19 "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"];
21 val type_intrs = data_typechecks
24 val [NilI, ConsI] = List.intrs;
26 (*An elimination rule, for type-checking*)
27 val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)";
29 (*Proving freeness results*)
30 val Cons_iff = List.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
31 val Nil_Cons_iff = List.mk_free "~ Nil=Cons(a,l)";
33 (*Perform induction on l, then prove the major premise using prems. *)
34 fun list_ind_tac a prems i =
35 EVERY [res_inst_tac [("x",a)] List.induct i,
36 rename_last_tac a ["1"] (i+2),
39 (** Lemmas to justify using "list" in other recursive type definitions **)
41 goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";
43 by (REPEAT (rtac List.bnd_mono 1));
44 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
45 val list_mono = result();
47 (*There is a similar proof by list induction.*)
48 goalw List.thy (List.defs@List.con_defs) "list(univ(A)) <= univ(A)";
49 by (rtac lfp_lowerbound 1);
50 by (rtac (A_subset_univ RS univ_mono) 2);
51 by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
53 val list_univ = result();
55 val list_subset_univ = standard
56 (list_mono RS (list_univ RSN (2,subset_trans)));
59 val major::prems = goal List.thy
62 \ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(<x,y>) \
63 \ |] ==> list_case(l,c,h) : C(l)";
64 by (rtac (major RS list_induct) 1);
65 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
66 ([list_case_0,list_case_Pair]@prems))));
67 val list_case_type = result();
73 goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
74 by (simp_tac rank_ss 1);
75 val rank_Cons1 = result();
77 goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
78 by (simp_tac rank_ss 1);
79 val rank_Cons2 = result();