# HG changeset patch # User berghofe # Date 909140173 -7200 # Node ID 0d8698c154394da6a637c49fec77f731e365f145 # Parent 31fc1d0e66d579a6199720402e8c3f99c371b5e9 Terms are now defined using the new datatype package. diff -r 31fc1d0e66d5 -r 0d8698c15439 src/HOL/Induct/Term.ML --- a/src/HOL/Induct/Term.ML Fri Oct 23 12:55:36 1998 +0200 +++ b/src/HOL/Induct/Term.ML Fri Oct 23 12:56:13 1998 +0200 @@ -1,169 +1,30 @@ -(* Title: HOL/ex/Term +(* Title: HOL/Induct/Term.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge + Author: Stefan Berghofer, TU Muenchen + Copyright 1998 TU Muenchen -Terms over a given alphabet -- function applications; illustrates list functor - (essentially the same type as in Trees & Forests) +Terms over a given alphabet -- function applications *) -(** Monotonicity and unfolding of the function **) - -Goal "term(A) = A <*> list(term(A))"; -by (fast_tac (claset() addSIs term.intrs - addEs [term.elim]) 1); -qed "term_unfold"; - -(*This justifies using term in other recursive type definitions*) -Goalw term.defs "A<=B ==> term(A) <= term(B)"; -by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1)); -qed "term_mono"; - -(** Type checking -- term creates well-founded sets **) - -Goalw term.defs "term(sexp) <= sexp"; -by (rtac lfp_lowerbound 1); -by (fast_tac (claset() addIs [sexp.SconsI, list_sexp RS subsetD]) 1); -qed "term_sexp"; - -(* A <= sexp ==> term(A) <= sexp *) -bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans)); - - -(** Elimination -- structural induction on the set term(A) **) +(** a simple theorem about composition of substitutions **) -(*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 (Scons x zs) \ -\ |] ==> R(M)"; -by (rtac (major RS term.induct) 1); -by (REPEAT (eresolve_tac ([minor] @ - ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); -(*Proof could also use mono_Int RS subsetD RS IntE *) -qed "Term_induct"; - -(*Induction on term(A) followed by induction on list *) -val major::prems = goal Term.thy - "[| M: term(A); \ -\ !!x. [| x: A |] ==> R (Scons x NIL); \ -\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); R (Scons x zs) \ -\ |] ==> R (Scons x (CONS z zs)) \ -\ |] ==> R(M)"; -by (rtac (major RS Term_induct) 1); -by (etac list.induct 1); -by (REPEAT (ares_tac prems 1)); -qed "Term_induct2"; - -(*** Structural Induction on the abstract type 'a term ***) - -val Rep_term_in_sexp = - Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD); +Goal "(subst_term ((subst_term f1) o f2) t) = \ + \ (subst_term f1 (subst_term f2 t)) & \ + \ (subst_term_list ((subst_term f1) o f2) ts) = \ + \ (subst_term_list f1 (subst_term_list f2 ts))"; +by (mutual_induct_tac ["t", "ts"] 1); +by (ALLGOALS Asm_full_simp_tac); +qed "subst_comp"; -(*Induction for the abstract type 'a term*) -val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def] - "[| !!x ts. (ALL t: set ts. R t) ==> 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 (ALLGOALS Asm_simp_tac); -by (ALLGOALS Fast_tac); -qed "term_induct"; - -(*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 (t#ts)) \ -\ |] ==> R(t)"; -by (rtac term_induct 1); (*types force good instantiation*) -by (etac rev_mp 1); -by (rtac list_induct2 1); (*types force good instantiation*) -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); -qed "term_induct2"; - -(*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)]; - - - -(*** Term_rec -- by wf recursion on pred_sexp ***) - -Goal "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \ - \ (%g. Split(%x y. d x y (Abs_map g y)))"; -by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1); -bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS - ((result() RS eq_reflection) RS def_wfrec)); +(**** alternative induction rule ****) -(*--------------------------------------------------------------------------- - * Old: - * 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. (N,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 1); -by (strip_tac 1); -by (etac (pred_sexp_CONS_D RS conjE) 1); -by (asm_simp_tac (simpset() addsimps [trancl_pred_sexpD1]) 1); -qed "Abs_map_lemma"; - -val [prem1,prem2,A_subset_sexp] = goal Term.thy - "[| M: sexp; N: list(term(A)); A<=sexp |] ==> \ -\ Term_rec (Scons M N) d = d M N (Abs_map (%Z. Term_rec Z d) N)"; -by (rtac (Term_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps - [Split, - 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); -qed "Term_rec"; - -(*** 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 term.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_ident2, 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; +bind_thm ("term_induct2", prove_goal thy + "[| !!v. P (Var v); \ + \ !!f ts. list_all P ts ==> P (App f ts) |] ==> \ + \ P t & list_all P ts" + (fn prems => + [mutual_induct_tac ["t", "ts"] 1, + resolve_tac prems 1, + resolve_tac prems 1, + atac 1, + ALLGOALS Asm_simp_tac]) RS conjunct1); diff -r 31fc1d0e66d5 -r 0d8698c15439 src/HOL/Induct/Term.thy --- a/src/HOL/Induct/Term.thy Fri Oct 23 12:55:36 1998 +0200 +++ b/src/HOL/Induct/Term.thy Fri Oct 23 12:56:13 1998 +0200 @@ -1,55 +1,31 @@ -(* Title: HOL/ex/Term +(* Title: HOL/Induct/Term.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge + Author: Stefan Berghofer, TU Muenchen + Copyright 1998 TU Muenchen -Terms over a given alphabet -- function applications; illustrates list functor - (essentially the same type as in Trees & Forests) - -There is no constructor APP because it is simply Scons +Terms over a given alphabet -- function applications *) -Term = SList + +Term = Main + -types 'a term +datatype + ('a, 'b) term = Var 'a + | App 'b ((('a, 'b) term) list) -arities term :: (term)term + +(** substitution function on terms **) consts - term :: 'a item set => 'a item set - Rep_term :: 'a term => 'a item - Abs_term :: 'a item => 'a term - Rep_Tlist :: 'a term list => 'a item - Abs_Tlist :: 'a item => 'a term list - App :: ['a, ('a term)list] => 'a term - Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b - term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b - -inductive "term(A)" - intrs - APP_I "[| M: A; N : list(term(A)) |] ==> Scons M N : term(A)" - monos list_mono - -defs - (*defining abstraction/representation functions for term list...*) - Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)" - Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)" + subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term" + subst_term_list :: + "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list" - (*defining the abstract constants*) - App_def "App a ts == Abs_term(Scons (Leaf a) (Rep_Tlist ts))" - - (*list recursion*) - Term_rec_def - "Term_rec M d == wfrec (trancl pred_sexp) - (%g. Split(%x y. d x y (Abs_map g y))) M" +primrec + "subst_term f (Var a) = f a" + "subst_term f (App b ts) = App b (subst_term_list f ts)" - term_rec_def - "term_rec t d == - Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)" + "subst_term_list f [] = []" + "subst_term_list f (t # ts) = + subst_term f t # subst_term_list f ts" -rules - (*faking a type definition for term...*) - Rep_term "Rep_term(n): term(range(Leaf))" - Rep_term_inverse "Abs_term(Rep_term(t)) = t" - Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M" end