src/ZF/List.thy
changeset 13509 6f168374652a
parent 13396 11219ca224ab
child 13524 604d0f3622d6
     1.1 --- a/src/ZF/List.thy	Wed Aug 21 15:53:30 2002 +0200
     1.2 +++ b/src/ZF/List.thy	Wed Aug 21 15:55:40 2002 +0200
     1.3 @@ -135,6 +135,9 @@
     1.4  (*An elimination rule, for type-checking*)
     1.5  inductive_cases ConsE: "Cons(a,l) : list(A)"
     1.6  
     1.7 +lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
     1.8 +by (blast elim: ConsE) 
     1.9 +
    1.10  (*Proving freeness results*)
    1.11  lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
    1.12  by auto
    1.13 @@ -420,8 +423,7 @@
    1.14  apply (simp_all (no_asm_simp) add: list_add_app)
    1.15  done
    1.16  
    1.17 -(** New induction rule **)
    1.18 -
    1.19 +(** New induction rules **)
    1.20  
    1.21  lemma list_append_induct:
    1.22      "[| l: list(A);
    1.23 @@ -434,6 +436,29 @@
    1.24  
    1.25  lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]
    1.26  
    1.27 +lemma list_complete_induct_lemma [rule_format]:
    1.28 + assumes ih: 
    1.29 +    "\<And>l. [| l \<in> list(A); 
    1.30 +             \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|] 
    1.31 +          ==> P(l)"
    1.32 +  shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n --> P(l)"
    1.33 +apply (induct_tac n, simp)
    1.34 +apply (blast intro: ih elim!: leE) 
    1.35 +done
    1.36 +
    1.37 +theorem list_complete_induct:
    1.38 +      "[| l \<in> list(A); 
    1.39 +          \<And>l. [| l \<in> list(A); 
    1.40 +                  \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|] 
    1.41 +               ==> P(l)
    1.42 +       |] ==> P(l)"
    1.43 +apply (rule list_complete_induct_lemma [of A]) 
    1.44 +   prefer 4 apply (rule le_refl, simp) 
    1.45 +  apply blast 
    1.46 + apply simp 
    1.47 +apply assumption
    1.48 +done
    1.49 +
    1.50  
    1.51  (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
    1.52  
    1.53 @@ -573,13 +598,11 @@
    1.54  
    1.55  lemma append_self_iff [simp]:
    1.56       "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
    1.57 -apply (simp (no_asm_simp))
    1.58 -done
    1.59 +by simp
    1.60  
    1.61  lemma append_self_iff2 [simp]:
    1.62       "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
    1.63 -apply (simp (no_asm_simp))
    1.64 -done
    1.65 +by simp
    1.66  
    1.67  (* Can also be proved from append_eq_append_iff2,
    1.68  but the proof requires two more hypotheses: x:A and y:A *)
    1.69 @@ -597,8 +620,7 @@
    1.70  
    1.71  lemma append_right_is_self_iff [simp]:
    1.72       "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
    1.73 -apply (simp (no_asm_simp) add: append_left_is_Nil_iff)
    1.74 -done
    1.75 +by (simp (no_asm_simp) add: append_left_is_Nil_iff)
    1.76  
    1.77  lemma append_right_is_self_iff2 [simp]:
    1.78       "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
    1.79 @@ -630,8 +652,7 @@
    1.80  lemma rev_list_elim [rule_format]:
    1.81       "xs:list(A) ==>
    1.82        (xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P"
    1.83 -apply (erule list_append_induct, auto)
    1.84 -done
    1.85 +by (erule list_append_induct, auto)
    1.86  
    1.87  
    1.88  (** more theorems about drop **)