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