src/HOL/List.ML
changeset 4911 6195e4468c54
parent 4830 bd73675adbed
child 4935 1694e2daef8f
     1.1 --- a/src/HOL/List.ML	Mon May 11 14:40:40 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Tue May 12 08:36:07 1998 +0200
     1.3 @@ -20,14 +20,11 @@
     1.4  qed "neq_Nil_conv";
     1.5  
     1.6  (* Induction over the length of a list: *)
     1.7 -val prems = goal thy
     1.8 - "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
     1.9 -by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
    1.10 -     wf_induct 1);
    1.11 -by (Simp_tac 1);
    1.12 -by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
    1.13 -by (eresolve_tac prems 1);
    1.14 -qed "list_length_induct";
    1.15 +val [prem] = goal thy
    1.16 +  "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
    1.17 +by(rtac measure_induct 1 THEN etac prem 1);
    1.18 +qed "length_induct";
    1.19 +
    1.20  
    1.21  (** "lists": the list-forming operator over sets **)
    1.22  
    1.23 @@ -252,7 +249,7 @@
    1.24    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
    1.25  
    1.26  val prems = goal thy "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
    1.27 -by(res_inst_tac [("xs","xs")] list_length_induct 1);
    1.28 +by(res_inst_tac [("xs","xs")] length_induct 1);
    1.29  by(res_inst_tac [("xs","xs")] snoc_exhaust 1);
    1.30   by(Clarify_tac 1);
    1.31   brs prems 1;
    1.32 @@ -562,11 +559,6 @@
    1.33  (**  More case analysis and induction **)
    1.34  section "More case analysis and induction";
    1.35  
    1.36 -val [prem] = goal thy
    1.37 -  "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
    1.38 -by(rtac measure_induct 1 THEN etac prem 1);
    1.39 -qed "length_induct";
    1.40 -
    1.41  goal thy "xs ~= [] --> (? ys y. xs = ys@[y])";
    1.42  by(res_inst_tac [("xs","xs")] length_induct 1);
    1.43  by(Clarify_tac 1);