src/ZF/list.ML
author lcp
Thu, 30 Sep 1993 10:10:21 +0100
changeset 14 1c0926788772
parent 6 8ce8c4d13d4d
child 30 d49df4181f0d
permissions -rw-r--r--
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/list.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Datatype definition of Lists
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
structure List = Datatype_Fun
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
 (val thy = Univ.thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
  val rec_specs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
      [("list", "univ(A)",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
	  [(["Nil"],	"i"), 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
	   (["Cons"],	"[i,i]=>i")])];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val rec_styp = "i=>i";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val ext = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val sintrs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
      ["Nil : list(A)",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
       "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  val monos = [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  val type_intrs = data_typechecks
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  val type_elims = []);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
val [NilI, ConsI] = List.intrs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
(*An elimination rule, for type-checking*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val ConsE = List.mk_cases List.con_defs "Cons(a,l) : list(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
(*Proving freeness results*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val Cons_iff     = List.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
val Nil_Cons_iff = List.mk_free "~ Nil=Cons(a,l)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*Perform induction on l, then prove the major premise using prems. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
fun list_ind_tac a prems i = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
    EVERY [res_inst_tac [("x",a)] List.induct i,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
	   rename_last_tac a ["1"] (i+2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
	   ares_tac prems i];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
(**  Lemmas to justify using "list" in other recursive type definitions **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
goalw List.thy List.defs "!!A B. A<=B ==> list(A) <= list(B)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (rtac lfp_mono 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
by (REPEAT (rtac List.bnd_mono 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
val list_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
(*There is a similar proof by list induction.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
goalw List.thy (List.defs@List.con_defs) "list(univ(A)) <= univ(A)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
by (rtac lfp_lowerbound 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (rtac (A_subset_univ RS univ_mono) 2);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
			    Pair_in_univ]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val list_univ = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val list_subset_univ = standard
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
    (list_mono RS (list_univ RSN (2,subset_trans)));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
val major::prems = goal List.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    "[| l: list(A);    \
14
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    60
\       c: C(Nil);       \
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    61
\       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    62
\    |] ==> list_case(c,h,l) : C(l)";
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    63
by (rtac (major RS List.induct) 1);
1c0926788772 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents: 6
diff changeset
    64
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.case_eqns @ prems))));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val list_case_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(** For recursion **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    71
by (simp_tac rank_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val rank_Cons1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    75
by (simp_tac rank_ss 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
val rank_Cons2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77