src/ZF/List.thy

 
 declare list.intros [simp,TC]
 
 (*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
 

      "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
 apply (induct_tac "ls")
 apply (simp_all (no_asm_simp) add: list_add_app)
 done
 
-(** New induction rule **)
-
+(** New induction rules **)
 
 lemma list_append_induct:
     "[| l: list(A);
         P(Nil);
         !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])

 apply (subgoal_tac "P(rev(rev(l)))", simp)
 apply (erule rev_type [THEN list.induct], simp_all)
 done
 
 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. ***)
 
 (** min FIXME: replace by Int! **)

 apply (rule append_eq_append, auto)
 done
 
 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 *)
 lemma append1_eq_iff [rule_format,simp]:
      "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"

 done
 
 
 lemma append_right_is_self_iff [simp]:
      "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
-apply (simp (no_asm_simp) add: append_left_is_Nil_iff)
-done
+by (simp (no_asm_simp) add: append_left_is_Nil_iff)
 
 lemma append_right_is_self_iff2 [simp]:
      "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
 apply (rule iffI)
 apply (drule sym, auto) 

 done
 
 lemma rev_list_elim [rule_format]:
      "xs:list(A) ==>
       (xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P"
-apply (erule list_append_induct, auto)
-done
+by (erule list_append_induct, auto)
 
 
 (** more theorems about drop **)
 
 lemma length_drop [rule_format,simp]: