equal
deleted
inserted
replaced
125 apply simp |
125 apply simp |
126 apply (rule le_imp_less_Suc) |
126 apply (rule le_imp_less_Suc) |
127 apply (rule trans_le_add1) |
127 apply (rule trans_le_add1) |
128 apply (rule trans_le_add2) |
128 apply (rule trans_le_add2) |
129 apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev) |
129 apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev) |
130 apply (simp add: member_le_sum_list_nat) |
130 apply (simp add: member_le_sum_list) |
131 done |
131 done |
132 |
132 |
133 theorem Apps_dB_induct: |
133 theorem Apps_dB_induct: |
134 assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)" |
134 assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)" |
135 and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)" |
135 and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)" |