author paulson Wed, 21 Aug 2002 15:55:40 +0200 changeset 13509 6f168374652a parent 13508 890d736b93a5 child 13510 0a0f37f9c031
new lemmas
 src/ZF/List.thy file | annotate | diff | comparison | revisions
```--- a/src/ZF/List.thy	Wed Aug 21 15:53:30 2002 +0200
+++ b/src/ZF/List.thy	Wed Aug 21 15:55:40 2002 +0200
@@ -135,6 +135,9 @@
(*An elimination rule, for type-checking*)
inductive_cases ConsE: "Cons(a,l) : list(A)"

+lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
+by (blast elim: ConsE)
+
(*Proving freeness results*)
lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
by auto
@@ -420,8 +423,7 @@
done

-(** New induction rule **)
-
+(** New induction rules **)

lemma list_append_induct:
"[| l: list(A);
@@ -434,6 +436,29 @@

lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]

+lemma list_complete_induct_lemma [rule_format]:
+ assumes ih:
+    "\<And>l. [| l \<in> list(A);
+             \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|]
+          ==> P(l)"
+  shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n --> P(l)"
+apply (induct_tac n, simp)
+apply (blast intro: ih elim!: leE)
+done
+
+theorem list_complete_induct:
+      "[| l \<in> list(A);
+          \<And>l. [| l \<in> list(A);
+                  \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|]
+               ==> P(l)
+       |] ==> P(l)"
+apply (rule list_complete_induct_lemma [of A])
+   prefer 4 apply (rule le_refl, simp)
+  apply blast
+ apply simp
+apply assumption
+done
+

(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)

@@ -573,13 +598,11 @@

lemma append_self_iff [simp]:
"[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
-apply (simp (no_asm_simp))
-done
+by simp

lemma append_self_iff2 [simp]:
"[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
-apply (simp (no_asm_simp))
-done
+by simp

(* Can also be proved from append_eq_append_iff2,
but the proof requires two more hypotheses: x:A and y:A *)
@@ -597,8 +620,7 @@

lemma append_right_is_self_iff [simp]:
"[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
-done