equal
deleted
inserted
replaced
108 apply clarify |
108 apply clarify |
109 apply (erule allE, erule impE) |
109 apply (erule allE, erule impE) |
110 prefer 2 |
110 prefer 2 |
111 apply (erule allE, erule mp, rule refl) |
111 apply (erule allE, erule mp, rule refl) |
112 apply simp |
112 apply simp |
113 apply (simp only: foldl_conv_fold add.commute fold_plus_listsum_rev) |
113 apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev) |
114 apply (fastforce simp add: listsum_map_remove1) |
114 apply (fastforce simp add: sum_list_map_remove1) |
115 apply clarify |
115 apply clarify |
116 apply (rule assms) |
116 apply (rule assms) |
117 apply (erule allE, erule impE) |
117 apply (erule allE, erule impE) |
118 prefer 2 |
118 prefer 2 |
119 apply (erule allE, erule mp, rule refl) |
119 apply (erule allE, erule mp, rule refl) |
124 apply (erule allE, erule mp, rule refl) |
124 apply (erule allE, erule mp, rule refl) |
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_listsum_rev) |
129 apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev) |
130 apply (simp add: member_le_listsum_nat) |
130 apply (simp add: member_le_sum_list_nat) |
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)" |