src/ZF/ex/Term.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 16 0b033d50ca1c
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	ZF/ex/term.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Datatype definition of terms over an alphabet.
clasohm@0
     7
Illustrates the list functor (essentially the same type as in Trees & Forests)
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
structure Term = Datatype_Fun
clasohm@0
    11
 (val thy = List.thy;
clasohm@0
    12
  val rec_specs = 
clasohm@0
    13
      [("term", "univ(A)",
clasohm@0
    14
	  [(["Apply"], "[i,i]=>i")])];
clasohm@0
    15
  val rec_styp = "i=>i";
clasohm@0
    16
  val ext = None
clasohm@0
    17
  val sintrs = ["[| a: A;  l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
clasohm@0
    18
  val monos = [list_mono];
clasohm@0
    19
  val type_intrs = [SigmaI,Pair_in_univ, list_univ RS subsetD, A_into_univ];
clasohm@0
    20
  val type_elims = []);
clasohm@0
    21
clasohm@0
    22
val [ApplyI] = Term.intrs;
clasohm@0
    23
clasohm@0
    24
(*Induction on term(A) followed by induction on List *)
clasohm@0
    25
val major::prems = goal Term.thy
clasohm@0
    26
    "[| t: term(A);  \
clasohm@0
    27
\       !!x.      [| x: A |] ==> P(Apply(x,Nil));  \
clasohm@0
    28
\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  P(Apply(x,zs))  \
clasohm@0
    29
\                 |] ==> P(Apply(x, Cons(z,zs)))  \
clasohm@0
    30
\    |] ==> P(t)";
clasohm@0
    31
by (rtac (major RS Term.induct) 1);
clasohm@0
    32
by (etac List.induct 1);
clasohm@0
    33
by (etac CollectE 2);
clasohm@0
    34
by (REPEAT (ares_tac (prems@[list_CollectD]) 1));
clasohm@0
    35
val term_induct2 = result();
clasohm@0
    36
clasohm@0
    37
(*Induction on term(A) to prove an equation*)
clasohm@0
    38
val major::prems = goal (merge_theories(Term.thy,ListFn.thy))
clasohm@0
    39
    "[| t: term(A);  \
clasohm@0
    40
\       !!x zs. [| x: A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==> \
clasohm@0
    41
\               f(Apply(x,zs)) = g(Apply(x,zs))  \
clasohm@0
    42
\    |] ==> f(t)=g(t)";
clasohm@0
    43
by (rtac (major RS Term.induct) 1);
clasohm@0
    44
by (resolve_tac prems 1);
clasohm@0
    45
by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1));
clasohm@0
    46
val term_induct_eqn = result();
clasohm@0
    47
clasohm@0
    48
(**  Lemmas to justify using "term" in other recursive type definitions **)
clasohm@0
    49
clasohm@0
    50
goalw Term.thy Term.defs "!!A B. A<=B ==> term(A) <= term(B)";
clasohm@0
    51
by (rtac lfp_mono 1);
clasohm@0
    52
by (REPEAT (rtac Term.bnd_mono 1));
clasohm@0
    53
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
clasohm@0
    54
val term_mono = result();
clasohm@0
    55
clasohm@0
    56
(*Easily provable by induction also*)
clasohm@0
    57
goalw Term.thy (Term.defs@Term.con_defs) "term(univ(A)) <= univ(A)";
clasohm@0
    58
by (rtac lfp_lowerbound 1);
clasohm@0
    59
by (rtac (A_subset_univ RS univ_mono) 2);
clasohm@0
    60
by (safe_tac ZF_cs);
clasohm@0
    61
by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1));
clasohm@0
    62
val term_univ = result();
clasohm@0
    63
clasohm@0
    64
val term_subset_univ = standard
clasohm@0
    65
    (term_mono RS (term_univ RSN (2,subset_trans)));
clasohm@0
    66