equal
deleted
inserted
replaced
34 lemma subst_comp: |
34 lemma subst_comp: |
35 "(subst_term ((subst_term f1) \<circ> f2) t) = |
35 "(subst_term ((subst_term f1) \<circ> f2) t) = |
36 (subst_term f1 (subst_term f2 t)) \<and> |
36 (subst_term f1 (subst_term f2 t)) \<and> |
37 (subst_term_list ((subst_term f1) \<circ> f2) ts) = |
37 (subst_term_list ((subst_term f1) \<circ> f2) ts) = |
38 (subst_term_list f1 (subst_term_list f2 ts))" |
38 (subst_term_list f1 (subst_term_list f2 ts))" |
39 apply (induct t and ts rule: term.induct) |
39 apply (induct t and ts) |
40 apply simp_all |
40 apply simp_all |
41 done |
41 done |
42 |
42 |
43 |
43 |
44 text {* \medskip Alternative induction rule *} |
44 text {* \medskip Alternative induction rule *} |
48 (!!f ts. list_all P ts ==> P (App f ts)) |
48 (!!f ts. list_all P ts ==> P (App f ts)) |
49 ==> P t" |
49 ==> P t" |
50 proof - |
50 proof - |
51 case rule_context |
51 case rule_context |
52 have "P t \<and> list_all P ts" |
52 have "P t \<and> list_all P ts" |
53 apply (induct t and ts rule: term.induct) |
53 apply (induct t and ts) |
54 apply (rule rule_context) |
54 apply (rule rule_context) |
55 apply (rule rule_context) |
55 apply (rule rule_context) |
56 apply assumption |
56 apply assumption |
57 apply simp_all |
57 apply simp_all |
58 done |
58 done |