equal
deleted
inserted
replaced
63 val Rep_term_in_sexp = |
63 val Rep_term_in_sexp = |
64 Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD); |
64 Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD); |
65 |
65 |
66 (*Induction for the abstract type 'a term*) |
66 (*Induction for the abstract type 'a term*) |
67 val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def] |
67 val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def] |
68 "[| !!x ts. (ALL t: setOfList ts. R t) ==> R(App x ts) \ |
68 "[| !!x ts. (ALL t: set_of_list ts. R t) ==> R(App x ts) \ |
69 \ |] ==> R(t)"; |
69 \ |] ==> R(t)"; |
70 by (rtac (Rep_term_inverse RS subst) 1); (*types force good instantiation*) |
70 by (rtac (Rep_term_inverse RS subst) 1); (*types force good instantiation*) |
71 by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1); |
71 by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1); |
72 by (rtac (Rep_term RS Term_induct) 1); |
72 by (rtac (Rep_term RS Term_induct) 1); |
73 by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS |
73 by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS |