src/ZF/ex/termfn.ML
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/termfn.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,192 @@
     1.4 +(*  Title: 	ZF/ex/term
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Terms over a given alphabet -- function applications; illustrates list functor
    1.10 +  (essentially the same type as in Trees & Forests)
    1.11 +*)
    1.12 +
    1.13 +writeln"File ZF/ex/term-fn.";
    1.14 +
    1.15 +open TermFn;
    1.16 +
    1.17 +(*** term_rec -- by Vset recursion ***)
    1.18 +
    1.19 +(*Lemma: map works correctly on the underlying list of terms*)
    1.20 +val [major,ordi] = goal ListFn.thy
    1.21 +    "[| l: list(A);  Ord(i) |] ==>  \
    1.22 +\    rank(l): i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
    1.23 +by (rtac (major RS List.induct) 1);
    1.24 +by (SIMP_TAC list_ss 1);
    1.25 +by (rtac impI 1);
    1.26 +by (forward_tac [rank_Cons1 RS Ord_trans] 1);
    1.27 +by (dtac (rank_Cons2 RS Ord_trans) 2);
    1.28 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [ordi, VsetI])));
    1.29 +val map_lemma = result();
    1.30 +
    1.31 +(*Typing premise is necessary to invoke map_lemma*)
    1.32 +val [prem] = goal TermFn.thy
    1.33 +    "ts: list(A) ==> \
    1.34 +\    term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
    1.35 +by (rtac (term_rec_def RS def_Vrec RS trans) 1);
    1.36 +by (rewrite_goals_tac Term.con_defs);
    1.37 +val term_rec_ss = ZF_ss 
    1.38 +      addcongs (mk_typed_congs TermFn.thy [("d", "[i,i,i]=>i")])
    1.39 +      addrews [Ord_rank, rank_pair2, prem RS map_lemma];
    1.40 +by (SIMP_TAC term_rec_ss 1);
    1.41 +val term_rec = result();
    1.42 +
    1.43 +(*Slightly odd typing condition on r in the second premise!*)
    1.44 +val major::prems = goal TermFn.thy
    1.45 +    "[| t: term(A);					\
    1.46 +\       !!x zs r. [| x: A;  zs: list(term(A)); 		\
    1.47 +\                    r: list(UN t:term(A). C(t)) |]	\
    1.48 +\                 ==> d(x, zs, r): C(Apply(x,zs))  	\
    1.49 +\    |] ==> term_rec(t,d) : C(t)";
    1.50 +by (rtac (major RS Term.induct) 1);
    1.51 +by (forward_tac [list_CollectD] 1);
    1.52 +by (rtac (term_rec RS ssubst) 1);
    1.53 +by (REPEAT (ares_tac prems 1));
    1.54 +by (etac List.induct 1);
    1.55 +by (ALLGOALS (ASM_SIMP_TAC (list_ss addrews [term_rec])));
    1.56 +by (etac CollectE 1);
    1.57 +by (REPEAT (ares_tac [ConsI, UN_I] 1));
    1.58 +val term_rec_type = result();
    1.59 +
    1.60 +val [rew,tslist] = goal TermFn.thy
    1.61 +    "[| !!t. j(t)==term_rec(t,d);  ts: list(A) |] ==> \
    1.62 +\    j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
    1.63 +by (rewtac rew);
    1.64 +by (rtac (tslist RS term_rec) 1);
    1.65 +val def_term_rec = result();
    1.66 +
    1.67 +val prems = goal TermFn.thy
    1.68 +    "[| t: term(A);					     \
    1.69 +\       !!x zs r. [| x: A;  zs: list(term(A));  r: list(C) |]  \
    1.70 +\                 ==> d(x, zs, r): C  		     \
    1.71 +\    |] ==> term_rec(t,d) : C";
    1.72 +by (REPEAT (ares_tac (term_rec_type::prems) 1));
    1.73 +by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
    1.74 +val term_rec_simple_type = result();
    1.75 +
    1.76 +
    1.77 +(** term_map **)
    1.78 +
    1.79 +val term_map = standard (term_map_def RS def_term_rec);
    1.80 +
    1.81 +val prems = goalw TermFn.thy [term_map_def]
    1.82 +    "[| t: term(A);  !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
    1.83 +by (REPEAT (ares_tac ([term_rec_simple_type, ApplyI] @ prems) 1));
    1.84 +val term_map_type = result();
    1.85 +
    1.86 +val [major] = goal TermFn.thy
    1.87 +    "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
    1.88 +by (rtac (major RS term_map_type) 1);
    1.89 +by (etac RepFunI 1);
    1.90 +val term_map_type2 = result();
    1.91 +
    1.92 +
    1.93 +(** term_size **)
    1.94 +
    1.95 +val term_size = standard (term_size_def RS def_term_rec);
    1.96 +
    1.97 +goalw TermFn.thy [term_size_def] "!!t A. t: term(A) ==> term_size(t) : nat";
    1.98 +by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
    1.99 +val term_size_type = result();
   1.100 +
   1.101 +
   1.102 +(** reflect **)
   1.103 +
   1.104 +val reflect = standard (reflect_def RS def_term_rec);
   1.105 +
   1.106 +goalw TermFn.thy [reflect_def] "!!t A. t: term(A) ==> reflect(t) : term(A)";
   1.107 +by (REPEAT (ares_tac [term_rec_simple_type, rev_type, ApplyI] 1));
   1.108 +val reflect_type = result();
   1.109 +
   1.110 +(** preorder **)
   1.111 +
   1.112 +val preorder = standard (preorder_def RS def_term_rec);
   1.113 +
   1.114 +goalw TermFn.thy [preorder_def]
   1.115 +    "!!t A. t: term(A) ==> preorder(t) : list(A)";
   1.116 +by (REPEAT (ares_tac [term_rec_simple_type, ConsI, flat_type] 1));
   1.117 +val preorder_type = result();
   1.118 +
   1.119 +
   1.120 +(** Term simplification **)
   1.121 +
   1.122 +val term_typechecks =
   1.123 +    [ApplyI, term_map_type, term_map_type2, term_size_type, reflect_type, 
   1.124 +     preorder_type];
   1.125 +
   1.126 +(*map_type2 and term_map_type2 instantiate variables*)
   1.127 +val term_ss = list_ss 
   1.128 +      addcongs (Term.congs @
   1.129 +		mk_congs TermFn.thy ["term_rec","term_map","term_size",
   1.130 +				   "reflect","preorder"])
   1.131 +      addrews [term_rec, term_map, term_size, reflect,
   1.132 +	       preorder]
   1.133 +      setauto type_auto_tac (list_typechecks@term_typechecks);
   1.134 +
   1.135 +
   1.136 +(** theorems about term_map **)
   1.137 +
   1.138 +goal TermFn.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
   1.139 +by (etac term_induct_eqn 1);
   1.140 +by (ASM_SIMP_TAC (term_ss addrews [map_ident]) 1);
   1.141 +val term_map_ident = result();
   1.142 +
   1.143 +goal TermFn.thy
   1.144 +  "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
   1.145 +by (etac term_induct_eqn 1);
   1.146 +by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
   1.147 +val term_map_compose = result();
   1.148 +
   1.149 +goal TermFn.thy
   1.150 +    "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
   1.151 +by (etac term_induct_eqn 1);
   1.152 +by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose]) 1);
   1.153 +val term_map_reflect = result();
   1.154 +
   1.155 +
   1.156 +(** theorems about term_size **)
   1.157 +
   1.158 +goal TermFn.thy
   1.159 +    "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
   1.160 +by (etac term_induct_eqn 1);
   1.161 +by (ASM_SIMP_TAC (term_ss addrews [map_compose]) 1);
   1.162 +val term_size_term_map = result();
   1.163 +
   1.164 +goal TermFn.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
   1.165 +by (etac term_induct_eqn 1);
   1.166 +by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib RS sym, map_compose,
   1.167 +				   list_add_rev]) 1);
   1.168 +val term_size_reflect = result();
   1.169 +
   1.170 +goal TermFn.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
   1.171 +by (etac term_induct_eqn 1);
   1.172 +by (ASM_SIMP_TAC (term_ss addrews [length_flat, map_compose]) 1);
   1.173 +val term_size_length = result();
   1.174 +
   1.175 +
   1.176 +(** theorems about reflect **)
   1.177 +
   1.178 +goal TermFn.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
   1.179 +by (etac term_induct_eqn 1);
   1.180 +by (ASM_SIMP_TAC (term_ss addrews [rev_map_distrib, map_compose,
   1.181 +				   map_ident, rev_rev_ident]) 1);
   1.182 +val reflect_reflect_ident = result();
   1.183 +
   1.184 +
   1.185 +(** theorems about preorder **)
   1.186 +
   1.187 +goal TermFn.thy
   1.188 +    "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
   1.189 +by (etac term_induct_eqn 1);
   1.190 +by (ASM_SIMP_TAC (term_ss addrews [map_compose, map_flat]) 1);
   1.191 +val preorder_term_map = result();
   1.192 +
   1.193 +(** preorder(reflect(t)) = rev(postorder(t)) **)
   1.194 +
   1.195 +writeln"Reached end of file.";