--- a/src/HOL/List.thy Wed Sep 22 11:46:28 2010 +0200
+++ b/src/HOL/List.thy Wed Sep 22 16:52:09 2010 +0200
@@ -4157,8 +4157,8 @@
lists :: "'a set => 'a list set"
for A :: "'a set"
where
- Nil [intro!]: "[]: lists A"
- | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
+ Nil [intro!, simp]: "[]: lists A"
+ | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
@@ -4184,6 +4184,9 @@
lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
+lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"
+by auto
+
lemma append_in_listsp_conv [iff]:
"(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
by (induct xs) auto
@@ -4209,6 +4212,9 @@
lemma lists_eq_set: "lists A = {xs. set xs <= A}"
by auto
+lemma lists_empty [simp]: "lists {} = {[]}"
+by auto
+
lemma lists_UNIV [simp]: "lists UNIV = UNIV"
by auto
--- a/src/HOL/Nominal/Examples/Standardization.thy Wed Sep 22 11:46:28 2010 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy Wed Sep 22 16:52:09 2010 +0200
@@ -654,7 +654,6 @@
shows "listsp ((pi::name prm) \<bullet> p) (pi \<bullet> xs)" using xs
apply induct
apply simp
- apply (rule listsp.intros)
apply simp
apply (rule listsp.intros)
apply (drule_tac pi=pi in perm_boolI)
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy Wed Sep 22 11:46:28 2010 +0200
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Wed Sep 22 16:52:09 2010 +0200
@@ -24,7 +24,6 @@
rule IT.Var,
erule listsp.induct,
simp (no_asm),
- rule listsp.Nil,
simp (no_asm),
rule listsp.Cons,
blast,
@@ -44,7 +43,6 @@
rule IT.Var,
erule listsp.induct,
simp (no_asm),
- rule listsp.Nil,
simp (no_asm),
rule listsp.Cons,
fast,