143 |
143 |
144 val [prem1,prem2,A_subset_Sexp] = goal Term.thy |
144 val [prem1,prem2,A_subset_Sexp] = goal Term.thy |
145 "[| M: Sexp; N: List(Term(A)); A<=Sexp |] ==> \ |
145 "[| M: Sexp; N: List(Term(A)); A<=Sexp |] ==> \ |
146 \ Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))"; |
146 \ Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))"; |
147 by (rtac (Term_rec_unfold RS trans) 1); |
147 by (rtac (Term_rec_unfold RS trans) 1); |
148 by (rtac (Split RS trans) 1); |
|
149 by (simp_tac (HOL_ss addsimps |
148 by (simp_tac (HOL_ss addsimps |
150 [prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl, |
149 [Split, |
|
150 prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl, |
151 prem1, prem2 RS rev_subsetD, List_subset_Sexp, |
151 prem1, prem2 RS rev_subsetD, List_subset_Sexp, |
152 Term_subset_Sexp, A_subset_Sexp])1); |
152 Term_subset_Sexp, A_subset_Sexp])1); |
153 val Term_rec = result(); |
153 val Term_rec = result(); |
154 |
154 |
155 (*** term_rec -- by Term_rec ***) |
155 (*** term_rec -- by Term_rec ***) |