diff -r 000000000000 -r 7949f97df77a ex/Term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/Term.ML Thu Sep 16 12:21:07 1993 +0200 @@ -0,0 +1,177 @@ +(* Title: HOL/ex/term + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +For term.thy. illustrates List functor + (essentially the same type as in Trees & Forests) +*) + +open Term; + +(*** Monotonicity and unfolding of the function ***) + +goal Term.thy "mono(%Z. A <*> List(Z))"; +by (REPEAT (ares_tac [monoI, subset_refl, List_mono, uprod_mono] 1)); +val Term_fun_mono = result(); + +val Term_unfold = Term_fun_mono RS (Term_def RS def_lfp_Tarski); + +(*This justifies using Term in other recursive type definitions*) +goalw Term.thy [Term_def] "!!A B. A<=B ==> Term(A) <= Term(B)"; +by (REPEAT (ares_tac [lfp_mono, subset_refl, List_mono, uprod_mono] 1)); +val Term_mono = result(); + +(** Type checking rules -- Term creates well-founded sets **) + +val prems = goalw Term.thy [Term_def] "Term(Sexp) <= Sexp"; +by (rtac lfp_lowerbound 1); +by (fast_tac (univ_cs addIs [Sexp_SconsI, List_Sexp RS subsetD]) 1); +val Term_Sexp = result(); + +(* A <= Sexp ==> Term(A) <= Sexp *) +val Term_subset_Sexp = standard + (Term_mono RS (Term_Sexp RSN (2,subset_trans))); + + +(** Elimination -- structural induction on the set Term(A) **) + +(*Induction for the set Term(A) *) +val [major,minor] = goal Term.thy + "[| M: Term(A); \ +\ !!x zs. [| x: A; zs: List(Term(A)); zs: List({x.R(x)}) \ +\ |] ==> R(x.zs) \ +\ |] ==> R(M)"; +by (rtac (major RS (Term_def RS def_induct)) 1); +by (rtac Term_fun_mono 1); +by (REPEAT (eresolve_tac ([uprodE, ssubst, minor] @ + ([Int_lower1,Int_lower2] RL [List_mono RS subsetD])) 1)); +val Term_induct = result(); + +(*Induction on Term(A) followed by induction on List *) +val major::prems = goal Term.thy + "[| M: Term(A); \ +\ !!x. [| x: A |] ==> R(x.NIL); \ +\ !!x z zs. [| x: A; z: Term(A); zs: List(Term(A)); R(x.zs) \ +\ |] ==> R(x . CONS(z,zs)) \ +\ |] ==> R(M)"; +by (rtac (major RS Term_induct) 1); +by (etac List_induct 1); +by (REPEAT (ares_tac prems 1)); +val Term_induct2 = result(); + +(*** Structural Induction on the abstract type 'a term ***) + +val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons]; + +val Rep_Term_in_Sexp = + Rep_Term RS (range_Leaf_subset_Sexp RS Term_subset_Sexp RS subsetD); + +(*Induction for the abstract type 'a term*) +val prems = goalw Term.thy [App_def,Rep_TList_def,Abs_TList_def] + "[| !!x ts. list_all(R,ts) ==> R(App(x,ts)) \ +\ |] ==> R(t)"; +by (rtac (Rep_Term_inverse RS subst) 1); (*types force good instantiation*) +by (res_inst_tac [("P","Rep_Term(t) : Sexp")] conjunct2 1); +by (rtac (Rep_Term RS Term_induct) 1); +by (REPEAT (ares_tac [conjI, Sexp_SconsI, Term_subset_Sexp RS + List_subset_Sexp,range_Leaf_subset_Sexp] 1 + ORELSE etac rev_subsetD 1)); +by (eres_inst_tac [("A1","Term(?u)"), ("f1","Rep_Term"), ("g1","Abs_Term")] + (Abs_map_inverse RS subst) 1); +by (rtac (range_Leaf_subset_Sexp RS Term_subset_Sexp) 1); +by (etac Abs_Term_inverse 1); +by (etac rangeE 1); +by (hyp_subst_tac 1); +by (resolve_tac prems 1); +by (etac List_induct 1); +by (etac CollectE 2); +by (stac Abs_map_CONS 2); +by (etac conjunct1 2); +by (etac rev_subsetD 2); +by (rtac List_subset_Sexp 2); +by (fast_tac set_cs 2); +by (ALLGOALS (asm_simp_tac list_all_ss)); +val term_induct = result(); + +(*Induction for the abstract type 'a term*) +val prems = goal Term.thy + "[| !!x. R(App(x,Nil)); \ +\ !!x t ts. R(App(x,ts)) ==> R(App(x, Cons(t,ts))) \ +\ |] ==> R(t)"; +by (rtac term_induct 1); (*types force good instantiation*) +by (etac rev_mp 1); +by (rtac list_induct 1); (*types force good instantiation*) +by (ALLGOALS (asm_simp_tac (list_all_ss addsimps prems))); +val term_induct2 = result(); + +(*Perform induction on xs. *) +fun term_ind2_tac a i = + EVERY [res_inst_tac [("t",a)] term_induct2 i, + rename_last_tac a ["1","s"] (i+1)]; + + +(** Introduction rule for Term **) + +(* c : A <*> List(Term(A)) ==> c : Term(A) *) +val TermI = standard (Term_unfold RS equalityD2 RS subsetD); + +(*The constant APP is not declared; it is simply . *) +val prems = goal Term.thy "[| M: A; N : List(Term(A)) |] ==> M.N : Term(A)"; +by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1)); +val APP_I = result(); + + +(*** Term_rec -- by wf recursion on pred_Sexp ***) + +val Term_rec_unfold = + wf_pred_Sexp RS wf_trancl RS (Term_rec_def RS def_wfrec); + +(** conversion rules **) + +val [prem] = goal Term.thy + "N: List(Term(A)) ==> \ +\ !M. : pred_Sexp^+ --> \ +\ Abs_map(cut(h, pred_Sexp^+, M), N) = \ +\ Abs_map(h,N)"; +by (rtac (prem RS List_induct) 1); +by (simp_tac list_all_ss 1); +by (strip_tac 1); +by (etac (pred_Sexp_CONS_D RS conjE) 1); +by (asm_simp_tac (list_all_ss addsimps [trancl_pred_SexpD1, cut_apply]) 1); +val Abs_map_lemma = result(); + +val [prem1,prem2,A_subset_Sexp] = goal Term.thy + "[| M: Sexp; N: List(Term(A)); A<=Sexp |] ==> \ +\ Term_rec(M.N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))"; +by (rtac (Term_rec_unfold RS trans) 1); +by (rtac (Split RS trans) 1); +by (simp_tac (HOL_ss addsimps + [prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl, + prem1, prem2 RS rev_subsetD, List_subset_Sexp, + Term_subset_Sexp, A_subset_Sexp])1); +val Term_rec = result(); + +(*** term_rec -- by Term_rec ***) + +local + val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy) + [("f","Rep_Term")] Rep_map_type; + val Rep_TList = Rep_Term RS Rep_map_type1; + val Rep_Term_rec = range_Leaf_subset_Sexp RSN (2,Rep_TList RSN(2,Term_rec)); + + (*Now avoids conditional rewriting with the premise N: List(Term(A)), + since A will be uninstantiated and will cause rewriting to fail. *) + val term_rec_ss = HOL_ss + addsimps [Rep_TList RS (rangeI RS APP_I RS Abs_Term_inverse), + Rep_Term_in_Sexp, Rep_Term_rec, Rep_Term_inverse, + inj_Leaf, Inv_f_f, + Abs_Rep_map, map_ident, Sexp_LeafI] +in + +val term_rec = prove_goalw Term.thy + [term_rec_def, App_def, Rep_TList_def, Abs_TList_def] + "term_rec(App(f,ts), d) = d(f, ts, map (%t. term_rec(t,d), ts))" + (fn _ => [simp_tac term_rec_ss 1]) + +end;