--- a/src/HOL/Library/NList.thy Thu Aug 11 11:57:19 2022 +0200
+++ b/src/HOL/Library/NList.thy Thu Aug 11 13:23:00 2022 +0200
@@ -14,20 +14,23 @@
lemma nlistsI: "\<lbrakk> size xs = n; set xs \<subseteq> A \<rbrakk> \<Longrightarrow> xs \<in> nlists n A"
by (simp add: nlists_def)
-lemma nlistsE_length (*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> size xs = n"
+text \<open>These [simp] attributes are double-edged.
+ Many proofs in Jinja rely on it but they can degrade performance.\<close>
+
+lemma nlistsE_length [simp]: "xs \<in> nlists n A \<Longrightarrow> size xs = n"
by (simp add: nlists_def)
lemma less_lengthI: "\<lbrakk> xs \<in> nlists n A; p < n \<rbrakk> \<Longrightarrow> p < size xs"
-by (simp add: nlistsE_length)
+by (simp)
-lemma nlistsE_set[simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> set xs \<subseteq> A"
+lemma nlistsE_set[simp]: "xs \<in> nlists n A \<Longrightarrow> set xs \<subseteq> A"
unfolding nlists_def by (simp)
lemma nlists_mono:
assumes "A \<subseteq> B" shows "nlists n A \<subseteq> nlists n B"
proof
fix xs assume "xs \<in> nlists n A"
- then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by (simp add:nlistsE_length)
+ then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by (simp)
with assms have "set xs \<subseteq> B" by simp
with size show "xs \<in> nlists n B" by(clarsimp intro!: nlistsI)
qed