src/HOL/List.ML
changeset 4830 bd73675adbed
parent 4686 74a12e86b20b
child 4911 6195e4468c54
     1.1 --- a/src/HOL/List.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -19,6 +19,15 @@
     1.4  by (Asm_simp_tac 1);
     1.5  qed "neq_Nil_conv";
     1.6  
     1.7 +(* Induction over the length of a list: *)
     1.8 +val prems = goal thy
     1.9 + "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
    1.10 +by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
    1.11 +     wf_induct 1);
    1.12 +by (Simp_tac 1);
    1.13 +by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
    1.14 +by (eresolve_tac prems 1);
    1.15 +qed "list_length_induct";
    1.16  
    1.17  (** "lists": the list-forming operator over sets **)
    1.18  
    1.19 @@ -219,6 +228,40 @@
    1.20  qed "tl_append2";
    1.21  Addsimps [tl_append2];
    1.22  
    1.23 +
    1.24 +(** Snoc exhaustion and induction **)
    1.25 +section "Snoc exhaustion and induction";
    1.26 +
    1.27 +goal thy "xs ~= [] --> (? ys y. xs = ys@[y])";
    1.28 +by(induct_tac "xs" 1);
    1.29 +by(Simp_tac 1);
    1.30 +by(exhaust_tac "list" 1);
    1.31 + by(Asm_simp_tac 1);
    1.32 + by(res_inst_tac [("x","[]")] exI 1);
    1.33 + by(Simp_tac 1);
    1.34 +by(Asm_full_simp_tac 1);
    1.35 +by(Clarify_tac 1);
    1.36 +by(res_inst_tac [("x","a#ys")] exI 1);
    1.37 +by(Asm_simp_tac 1);
    1.38 +val lemma = result();
    1.39 +
    1.40 +goal thy  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
    1.41 +by(cut_facts_tac [lemma] 1);
    1.42 +by(Blast_tac 1);
    1.43 +bind_thm ("snoc_exhaust",
    1.44 +  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
    1.45 +
    1.46 +val prems = goal thy "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
    1.47 +by(res_inst_tac [("xs","xs")] list_length_induct 1);
    1.48 +by(res_inst_tac [("xs","xs")] snoc_exhaust 1);
    1.49 + by(Clarify_tac 1);
    1.50 + brs prems 1;
    1.51 +by(Clarify_tac 1);
    1.52 +brs prems 1;
    1.53 +auto();
    1.54 +qed "snoc_induct";
    1.55 +
    1.56 +
    1.57  (** map **)
    1.58  
    1.59  section "map";