src/ZF/ex/Term.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 529 f0d16216e394
child 760 f0200e91b272
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp@486
     1
(*  Title: 	ZF/ex/Term.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@486
     4
    Copyright   1994  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
lcp@515
    10
open Term;
clasohm@0
    11
lcp@434
    12
goal Term.thy "term(A) = A * list(term(A))";
lcp@529
    13
let open term;  val rew = rewrite_rule con_defs in  
lcp@529
    14
by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
lcp@529
    15
                     addEs [rew elim]) 1)
lcp@529
    16
end;
lcp@434
    17
val term_unfold = result();
lcp@434
    18
clasohm@0
    19
(*Induction on term(A) followed by induction on List *)
clasohm@0
    20
val major::prems = goal Term.thy
clasohm@0
    21
    "[| t: term(A);  \
clasohm@0
    22
\       !!x.      [| x: A |] ==> P(Apply(x,Nil));  \
clasohm@0
    23
\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  P(Apply(x,zs))  \
clasohm@0
    24
\                 |] ==> P(Apply(x, Cons(z,zs)))  \
clasohm@0
    25
\    |] ==> P(t)";
lcp@515
    26
by (rtac (major RS term.induct) 1);
lcp@515
    27
by (etac list.induct 1);
clasohm@0
    28
by (etac CollectE 2);
clasohm@0
    29
by (REPEAT (ares_tac (prems@[list_CollectD]) 1));
clasohm@0
    30
val term_induct2 = result();
clasohm@0
    31
clasohm@0
    32
(*Induction on term(A) to prove an equation*)
lcp@515
    33
val major::prems = goal Term.thy
clasohm@0
    34
    "[| t: term(A);  \
clasohm@0
    35
\       !!x zs. [| x: A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==> \
clasohm@0
    36
\               f(Apply(x,zs)) = g(Apply(x,zs))  \
clasohm@0
    37
\    |] ==> f(t)=g(t)";
lcp@515
    38
by (rtac (major RS term.induct) 1);
clasohm@0
    39
by (resolve_tac prems 1);
clasohm@0
    40
by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1));
clasohm@0
    41
val term_induct_eqn = result();
clasohm@0
    42
clasohm@0
    43
(**  Lemmas to justify using "term" in other recursive type definitions **)
clasohm@0
    44
lcp@515
    45
goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
clasohm@0
    46
by (rtac lfp_mono 1);
lcp@515
    47
by (REPEAT (rtac term.bnd_mono 1));
clasohm@0
    48
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
clasohm@0
    49
val term_mono = result();
clasohm@0
    50
clasohm@0
    51
(*Easily provable by induction also*)
lcp@515
    52
goalw Term.thy (term.defs@term.con_defs) "term(univ(A)) <= univ(A)";
clasohm@0
    53
by (rtac lfp_lowerbound 1);
clasohm@0
    54
by (rtac (A_subset_univ RS univ_mono) 2);
clasohm@0
    55
by (safe_tac ZF_cs);
clasohm@0
    56
by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1));
clasohm@0
    57
val term_univ = result();
clasohm@0
    58
lcp@434
    59
val term_subset_univ = 
lcp@434
    60
    term_mono RS (term_univ RSN (2,subset_trans)) |> standard;
clasohm@0
    61
lcp@434
    62
goal Term.thy "!!t A B. [| t: term(A);  A <= univ(B) |] ==> t: univ(B)";
lcp@434
    63
by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1));
lcp@434
    64
val term_into_univ = result();
lcp@515
    65
lcp@515
    66
lcp@515
    67
(*** term_rec -- by Vset recursion ***)
lcp@515
    68
lcp@515
    69
(*Lemma: map works correctly on the underlying list of terms*)
lcp@515
    70
val [major,ordi] = goal list.thy
lcp@515
    71
    "[| l: list(A);  Ord(i) |] ==>  \
lcp@515
    72
\    rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
lcp@515
    73
by (rtac (major RS list.induct) 1);
lcp@515
    74
by (simp_tac list_ss 1);
lcp@515
    75
by (rtac impI 1);
lcp@515
    76
by (forward_tac [rank_Cons1 RS lt_trans] 1);
lcp@515
    77
by (dtac (rank_Cons2 RS lt_trans) 1);
lcp@515
    78
by (asm_simp_tac (list_ss addsimps [ordi, VsetI]) 1);
lcp@515
    79
val map_lemma = result();
lcp@515
    80
lcp@515
    81
(*Typing premise is necessary to invoke map_lemma*)
lcp@515
    82
val [prem] = goal Term.thy
lcp@515
    83
    "ts: list(A) ==> \
lcp@515
    84
\    term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
lcp@515
    85
by (rtac (term_rec_def RS def_Vrec RS trans) 1);
lcp@515
    86
by (rewrite_goals_tac term.con_defs);
lcp@515
    87
val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma];
lcp@515
    88
by (simp_tac term_rec_ss 1);
lcp@515
    89
val term_rec = result();
lcp@515
    90
lcp@515
    91
(*Slightly odd typing condition on r in the second premise!*)
lcp@515
    92
val major::prems = goal Term.thy
lcp@515
    93
    "[| t: term(A);					\
lcp@515
    94
\       !!x zs r. [| x: A;  zs: list(term(A)); 		\
lcp@515
    95
\                    r: list(UN t:term(A). C(t)) |]	\
lcp@515
    96
\                 ==> d(x, zs, r): C(Apply(x,zs))  	\
lcp@515
    97
\    |] ==> term_rec(t,d) : C(t)";
lcp@515
    98
by (rtac (major RS term.induct) 1);
lcp@515
    99
by (forward_tac [list_CollectD] 1);
lcp@515
   100
by (rtac (term_rec RS ssubst) 1);
lcp@515
   101
by (REPEAT (ares_tac prems 1));
lcp@515
   102
by (etac list.induct 1);
lcp@515
   103
by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
lcp@515
   104
by (etac CollectE 1);
lcp@515
   105
by (REPEAT (ares_tac [list.Cons_I, UN_I] 1));
lcp@515
   106
val term_rec_type = result();
lcp@515
   107
lcp@515
   108
val [rew,tslist] = goal Term.thy
lcp@515
   109
    "[| !!t. j(t)==term_rec(t,d);  ts: list(A) |] ==> \
lcp@515
   110
\    j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
lcp@515
   111
by (rewtac rew);
lcp@515
   112
by (rtac (tslist RS term_rec) 1);
lcp@515
   113
val def_term_rec = result();
lcp@515
   114
lcp@515
   115
val prems = goal Term.thy
lcp@515
   116
    "[| t: term(A);					     \
lcp@515
   117
\       !!x zs r. [| x: A;  zs: list(term(A));  r: list(C) |]  \
lcp@515
   118
\                 ==> d(x, zs, r): C  		     \
lcp@515
   119
\    |] ==> term_rec(t,d) : C";
lcp@515
   120
by (REPEAT (ares_tac (term_rec_type::prems) 1));
lcp@515
   121
by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
lcp@515
   122
val term_rec_simple_type = result();
lcp@515
   123
lcp@515
   124
lcp@515
   125
(** term_map **)
lcp@515
   126
lcp@515
   127
val term_map = standard (term_map_def RS def_term_rec);
lcp@515
   128
lcp@515
   129
val prems = goalw Term.thy [term_map_def]
lcp@515
   130
    "[| t: term(A);  !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
lcp@515
   131
by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1));
lcp@515
   132
val term_map_type = result();
lcp@515
   133
lcp@515
   134
val [major] = goal Term.thy
lcp@515
   135
    "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
lcp@515
   136
by (rtac (major RS term_map_type) 1);
lcp@515
   137
by (etac RepFunI 1);
lcp@515
   138
val term_map_type2 = result();
lcp@515
   139
lcp@515
   140
lcp@515
   141
(** term_size **)
lcp@515
   142
lcp@515
   143
val term_size = standard (term_size_def RS def_term_rec);
lcp@515
   144
lcp@515
   145
goalw Term.thy [term_size_def] "!!t A. t: term(A) ==> term_size(t) : nat";
lcp@515
   146
by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
lcp@515
   147
val term_size_type = result();
lcp@515
   148
lcp@515
   149
lcp@515
   150
(** reflect **)
lcp@515
   151
lcp@515
   152
val reflect = standard (reflect_def RS def_term_rec);
lcp@515
   153
lcp@515
   154
goalw Term.thy [reflect_def] "!!t A. t: term(A) ==> reflect(t) : term(A)";
lcp@515
   155
by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
lcp@515
   156
val reflect_type = result();
lcp@515
   157
lcp@515
   158
(** preorder **)
lcp@515
   159
lcp@515
   160
val preorder = standard (preorder_def RS def_term_rec);
lcp@515
   161
lcp@515
   162
goalw Term.thy [preorder_def]
lcp@515
   163
    "!!t A. t: term(A) ==> preorder(t) : list(A)";
lcp@515
   164
by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
lcp@515
   165
val preorder_type = result();
lcp@515
   166
lcp@515
   167
lcp@515
   168
(** Term simplification **)
lcp@515
   169
lcp@515
   170
val term_typechecks =
lcp@515
   171
    [term.Apply_I, term_map_type, term_map_type2, term_size_type, 
lcp@515
   172
     reflect_type, preorder_type];
lcp@515
   173
lcp@515
   174
(*map_type2 and term_map_type2 instantiate variables*)
lcp@515
   175
val term_ss = list_ss 
lcp@515
   176
      addsimps [term_rec, term_map, term_size, reflect, preorder]
lcp@515
   177
      setsolver type_auto_tac (list_typechecks@term_typechecks);
lcp@515
   178
lcp@515
   179
lcp@515
   180
(** theorems about term_map **)
lcp@515
   181
lcp@515
   182
goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
lcp@515
   183
by (etac term_induct_eqn 1);
lcp@515
   184
by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
lcp@515
   185
val term_map_ident = result();
lcp@515
   186
lcp@515
   187
goal Term.thy
lcp@515
   188
  "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
lcp@515
   189
by (etac term_induct_eqn 1);
lcp@515
   190
by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
lcp@515
   191
val term_map_compose = result();
lcp@515
   192
lcp@515
   193
goal Term.thy
lcp@515
   194
    "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
lcp@515
   195
by (etac term_induct_eqn 1);
lcp@515
   196
by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
lcp@515
   197
val term_map_reflect = result();
lcp@515
   198
lcp@515
   199
lcp@515
   200
(** theorems about term_size **)
lcp@515
   201
lcp@515
   202
goal Term.thy
lcp@515
   203
    "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
lcp@515
   204
by (etac term_induct_eqn 1);
lcp@515
   205
by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
lcp@515
   206
val term_size_term_map = result();
lcp@515
   207
lcp@515
   208
goal Term.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
lcp@515
   209
by (etac term_induct_eqn 1);
lcp@515
   210
by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
lcp@515
   211
				    list_add_rev]) 1);
lcp@515
   212
val term_size_reflect = result();
lcp@515
   213
lcp@515
   214
goal Term.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
lcp@515
   215
by (etac term_induct_eqn 1);
lcp@515
   216
by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
lcp@515
   217
val term_size_length = result();
lcp@515
   218
lcp@515
   219
lcp@515
   220
(** theorems about reflect **)
lcp@515
   221
lcp@515
   222
goal Term.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
lcp@515
   223
by (etac term_induct_eqn 1);
lcp@515
   224
by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
lcp@515
   225
				    map_ident, rev_rev_ident]) 1);
lcp@515
   226
val reflect_reflect_ident = result();
lcp@515
   227
lcp@515
   228
lcp@515
   229
(** theorems about preorder **)
lcp@515
   230
lcp@515
   231
goal Term.thy
lcp@515
   232
    "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
lcp@515
   233
by (etac term_induct_eqn 1);
lcp@515
   234
by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
lcp@515
   235
val preorder_term_map = result();
lcp@515
   236
lcp@515
   237
(** preorder(reflect(t)) = rev(postorder(t)) **)
lcp@515
   238
lcp@515
   239
writeln"Reached end of file.";