src/ZF/ex/TermFn.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	ZF/ex/term
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Terms over a given alphabet -- function applications; illustrates list functor
clasohm@0
     7
  (essentially the same type as in Trees & Forests)
clasohm@0
     8
*)
clasohm@0
     9
clasohm@0
    10
writeln"File ZF/ex/term-fn.";
clasohm@0
    11
clasohm@0
    12
open TermFn;
clasohm@0
    13
clasohm@0
    14
(*** term_rec -- by Vset recursion ***)
clasohm@0
    15
clasohm@0
    16
(*Lemma: map works correctly on the underlying list of terms*)
clasohm@0
    17
val [major,ordi] = goal ListFn.thy
clasohm@0
    18
    "[| l: list(A);  Ord(i) |] ==>  \
clasohm@0
    19
\    rank(l): i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
clasohm@0
    20
by (rtac (major RS List.induct) 1);
clasohm@0
    21
by (SIMP_TAC list_ss 1);
clasohm@0
    22
by (rtac impI 1);
clasohm@0
    23
by (forward_tac [rank_Cons1 RS Ord_trans] 1);
clasohm@0
    24
by (dtac (rank_Cons2 RS Ord_trans) 2);
clasohm@0
    25
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [ordi, VsetI])));
clasohm@0
    26
val map_lemma = result();
clasohm@0
    27
clasohm@0
    28
(*Typing premise is necessary to invoke map_lemma*)
clasohm@0
    29
val [prem] = goal TermFn.thy
clasohm@0
    30
    "ts: list(A) ==> \
clasohm@0
    31
\    term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
clasohm@0
    32
by (rtac (term_rec_def RS def_Vrec RS trans) 1);
clasohm@0
    33
by (rewrite_goals_tac Term.con_defs);
clasohm@0
    34
val term_rec_ss = ZF_ss 
clasohm@0
    35
      addcongs (mk_typed_congs TermFn.thy [("d", "[i,i,i]=>i")])
clasohm@0
    36
      addrews [Ord_rank, rank_pair2, prem RS map_lemma];
clasohm@0
    37
by (SIMP_TAC term_rec_ss 1);
clasohm@0
    38
val term_rec = result();
clasohm@0
    39
clasohm@0
    40
(*Slightly odd typing condition on r in the second premise!*)
clasohm@0
    41
val major::prems = goal TermFn.thy
clasohm@0
    42
    "[| t: term(A);					\
clasohm@0
    43
\       !!x zs r. [| x: A;  zs: list(term(A)); 		\
clasohm@0
    44
\                    r: list(UN t:term(A). C(t)) |]	\
clasohm@0
    45
\                 ==> d(x, zs, r): C(Apply(x,zs))  	\
clasohm@0
    46
\    |] ==> term_rec(t,d) : C(t)";
clasohm@0
    47
by (rtac (major RS Term.induct) 1);
clasohm@0
    48
by (forward_tac [list_CollectD] 1);
clasohm@0
    49
by (rtac (term_rec RS ssubst) 1);
clasohm@0
    50
by (REPEAT (ares_tac prems 1));
clasohm@0
    51
by (etac List.induct 1);
clasohm@0
    52
by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [term_rec])));
clasohm@0
    53
by (etac CollectE 1);
clasohm@0
    54
by (REPEAT (ares_tac [ConsI, UN_I] 1));
clasohm@0
    55
val term_rec_type = result();
clasohm@0
    56
clasohm@0
    57
val [rew,tslist] = goal TermFn.thy
clasohm@0
    58
    "[| !!t. j(t)==term_rec(t,d);  ts: list(A) |] ==> \
clasohm@0
    59
\    j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
clasohm@0
    60
by (rewtac rew);
clasohm@0
    61
by (rtac (tslist RS term_rec) 1);
clasohm@0
    62
val def_term_rec = result();
clasohm@0
    63
clasohm@0
    64
val prems = goal TermFn.thy
clasohm@0
    65
    "[| t: term(A);					     \
clasohm@0
    66
\       !!x zs r. [| x: A;  zs: list(term(A));  r: list(C) |]  \
clasohm@0
    67
\                 ==> d(x, zs, r): C  		     \
clasohm@0
    68
\    |] ==> term_rec(t,d) : C";
clasohm@0
    69
by (REPEAT (ares_tac (term_rec_type::prems) 1));
clasohm@0
    70
by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
clasohm@0
    71
val term_rec_simple_type = result();
clasohm@0
    72
clasohm@0
    73
clasohm@0
    74
(** term_map **)
clasohm@0
    75
clasohm@0
    76
val term_map = standard (term_map_def RS def_term_rec);
clasohm@0
    77
clasohm@0
    78
val prems = goalw TermFn.thy [term_map_def]
clasohm@0
    79
    "[| t: term(A);  !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
clasohm@0
    80
by (REPEAT (ares_tac ([term_rec_simple_type, ApplyI] @ prems) 1));
clasohm@0
    81
val term_map_type = result();
clasohm@0
    82
clasohm@0
    83
val [major] = goal TermFn.thy
clasohm@0
    84
    "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
clasohm@0
    85
by (rtac (major RS term_map_type) 1);
clasohm@0
    86
by (etac RepFunI 1);
clasohm@0
    87
val term_map_type2 = result();
clasohm@0
    88
clasohm@0
    89
clasohm@0
    90
(** term_size **)
clasohm@0
    91
clasohm@0
    92
val term_size = standard (term_size_def RS def_term_rec);
clasohm@0
    93
clasohm@0
    94
goalw TermFn.thy [term_size_def] "!!t A. t: term(A) ==> term_size(t) : nat";
clasohm@0
    95
by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
clasohm@0
    96
val term_size_type = result();
clasohm@0
    97
clasohm@0
    98
clasohm@0
    99
(** reflect **)
clasohm@0
   100
clasohm@0
   101
val reflect = standard (reflect_def RS def_term_rec);
clasohm@0
   102
clasohm@0
   103
goalw TermFn.thy [reflect_def] "!!t A. t: term(A) ==> reflect(t) : term(A)";
clasohm@0
   104
by (REPEAT (ares_tac [term_rec_simple_type, rev_type, ApplyI] 1));
clasohm@0
   105
val reflect_type = result();
clasohm@0
   106
clasohm@0
   107
(** preorder **)
clasohm@0
   108
clasohm@0
   109
val preorder = standard (preorder_def RS def_term_rec);
clasohm@0
   110
clasohm@0
   111
goalw TermFn.thy [preorder_def]
clasohm@0
   112
    "!!t A. t: term(A) ==> preorder(t) : list(A)";
clasohm@0
   113
by (REPEAT (ares_tac [term_rec_simple_type, ConsI, flat_type] 1));
clasohm@0
   114
val preorder_type = result();
clasohm@0
   115
clasohm@0
   116
clasohm@0
   117
(** Term simplification **)
clasohm@0
   118
clasohm@0
   119
val term_typechecks =
clasohm@0
   120
    [ApplyI, term_map_type, term_map_type2, term_size_type, reflect_type, 
clasohm@0
   121
     preorder_type];
clasohm@0
   122
clasohm@0
   123
(*map_type2 and term_map_type2 instantiate variables*)
clasohm@0
   124
val term_ss = list_ss 
clasohm@0
   125
      addcongs (Term.congs @
clasohm@0
   126
		mk_congs TermFn.thy ["term_rec","term_map","term_size",
clasohm@0
   127
				   "reflect","preorder"])
clasohm@0
   128
      addrews [term_rec, term_map, term_size, reflect,
clasohm@0
   129
	       preorder]
clasohm@0
   130
      setauto type_auto_tac (list_typechecks@term_typechecks);
clasohm@0
   131
clasohm@0
   132
clasohm@0
   133
(** theorems about term_map **)
clasohm@0
   134
clasohm@0
   135
goal TermFn.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
clasohm@0
   136
by (etac term_induct_eqn 1);
clasohm@0
   137
by (ASM_SIMP_TAC (term_ss addrews [map_ident]) 1);
clasohm@0
   138
val term_map_ident = result();
clasohm@0
   139
clasohm@0
   140
goal TermFn.thy
clasohm@0
   141
  "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
clasohm@0
   142
by (etac term_induct_eqn 1);
clasohm@0
   143
by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
clasohm@0
   144
val term_map_compose = result();
clasohm@0
   145
clasohm@0
   146
goal TermFn.thy
clasohm@0
   147
    "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
clasohm@0
   148
by (etac term_induct_eqn 1);
clasohm@0
   149
by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose]) 1);
clasohm@0
   150
val term_map_reflect = result();
clasohm@0
   151
clasohm@0
   152
clasohm@0
   153
(** theorems about term_size **)
clasohm@0
   154
clasohm@0
   155
goal TermFn.thy
clasohm@0
   156
    "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
clasohm@0
   157
by (etac term_induct_eqn 1);
clasohm@0
   158
by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
clasohm@0
   159
val term_size_term_map = result();
clasohm@0
   160
clasohm@0
   161
goal TermFn.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
clasohm@0
   162
by (etac term_induct_eqn 1);
clasohm@0
   163
by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose,
clasohm@0
   164
				   list_add_rev]) 1);
clasohm@0
   165
val term_size_reflect = result();
clasohm@0
   166
clasohm@0
   167
goal TermFn.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
clasohm@0
   168
by (etac term_induct_eqn 1);
clasohm@0
   169
by (ASM_SIMP_TAC (term_ss addrews [length_flat, map_compose]) 1);
clasohm@0
   170
val term_size_length = result();
clasohm@0
   171
clasohm@0
   172
clasohm@0
   173
(** theorems about reflect **)
clasohm@0
   174
clasohm@0
   175
goal TermFn.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
clasohm@0
   176
by (etac term_induct_eqn 1);
clasohm@0
   177
by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib, map_compose,
clasohm@0
   178
				   map_ident, rev_rev_ident]) 1);
clasohm@0
   179
val reflect_reflect_ident = result();
clasohm@0
   180
clasohm@0
   181
clasohm@0
   182
(** theorems about preorder **)
clasohm@0
   183
clasohm@0
   184
goal TermFn.thy
clasohm@0
   185
    "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
clasohm@0
   186
by (etac term_induct_eqn 1);
clasohm@0
   187
by (ASM_SIMP_TAC (term_ss addrews [map_compose, map_flat]) 1);
clasohm@0
   188
val preorder_term_map = result();
clasohm@0
   189
clasohm@0
   190
(** preorder(reflect(t)) = rev(postorder(t)) **)
clasohm@0
   191
clasohm@0
   192
writeln"Reached end of file.";