equal
deleted
inserted
replaced
112 listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow> |
112 listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow> |
113 listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)" |
113 listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)" |
114 by (induct ts) simp_all |
114 by (induct ts) simp_all |
115 |
115 |
116 lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF" |
116 lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF" |
117 apply (induct fixing: i j set: NF) |
117 apply (induct arbitrary: i j set: NF) |
118 apply simp |
118 apply simp |
119 apply (frule listall_conj1) |
119 apply (frule listall_conj1) |
120 apply (drule listall_conj2) |
120 apply (drule listall_conj2) |
121 apply (drule_tac i=i and j=j in subst_terms_NF) |
121 apply (drule_tac i=i and j=j in subst_terms_NF) |
122 apply assumption |
122 apply assumption |
154 listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow> |
154 listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow> |
155 listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)" |
155 listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)" |
156 by (induct ts) simp_all |
156 by (induct ts) simp_all |
157 |
157 |
158 lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF" |
158 lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF" |
159 apply (induct fixing: i set: NF) |
159 apply (induct arbitrary: i set: NF) |
160 apply (frule listall_conj1) |
160 apply (frule listall_conj1) |
161 apply (drule listall_conj2) |
161 apply (drule listall_conj2) |
162 apply (drule_tac i=i in lift_terms_NF) |
162 apply (drule_tac i=i in lift_terms_NF) |
163 apply assumption |
163 apply assumption |
164 apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard]) |
164 apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard]) |