New induction schemas for lists (length and snoc).
authornipkow
Sun Feb 22 14:12:23 1998 +0100 (1998-02-22)
changeset 46431b40fcac5a09
parent 4642 2d3910d6ab10
child 4644 ecf8f17f6fe0
New induction schemas for lists (length and snoc).
src/HOL/Lex/Prefix.ML
src/HOL/List.ML
src/HOL/List.thy
src/HOL/WF_Rel.ML
     1.1 --- a/src/HOL/Lex/Prefix.ML	Fri Feb 20 17:57:16 1998 +0100
     1.2 +++ b/src/HOL/Lex/Prefix.ML	Sun Feb 22 14:12:23 1998 +0100
     1.3 @@ -4,8 +4,7 @@
     1.4      Copyright   1995 TUM
     1.5  *)
     1.6  
     1.7 -open Prefix;
     1.8 -
     1.9 +(* Junk: *)
    1.10  val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
    1.11  by (rtac allI 1);
    1.12  by (list.induct_tac "l" 1);
    1.13 @@ -13,6 +12,25 @@
    1.14  by (rtac min 1);
    1.15  val list_cases = result();
    1.16  
    1.17 +(** <= is a partial order: **)
    1.18 +
    1.19 +goalw thy [prefix_def] "xs <= (xs::'a list)";
    1.20 +by(Simp_tac 1);
    1.21 +qed "prefix_refl";
    1.22 +Addsimps[prefix_refl];
    1.23 +
    1.24 +goalw thy [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
    1.25 +by(Clarify_tac 1);
    1.26 +by(Simp_tac 1);
    1.27 +qed "prefix_trans";
    1.28 +
    1.29 +goalw thy [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
    1.30 +by(Clarify_tac 1);
    1.31 +by(Asm_full_simp_tac 1);
    1.32 +qed "prefix_antisym";
    1.33 +
    1.34 +(** recursion equations **)
    1.35 +
    1.36  goalw Prefix.thy [prefix_def] "[] <= xs";
    1.37  by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    1.38  qed "Nil_prefix";
    1.39 @@ -25,6 +43,34 @@
    1.40  qed "prefix_Nil";
    1.41  Addsimps [prefix_Nil];
    1.42  
    1.43 +goalw thy [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
    1.44 +br iffI 1;
    1.45 + be exE 1;
    1.46 + by(rename_tac "zs" 1);
    1.47 + by(res_inst_tac [("xs","zs")] snoc_eq_cases 1);
    1.48 +  by(Asm_full_simp_tac 1);
    1.49 + by(hyp_subst_tac 1);
    1.50 + by(asm_full_simp_tac (simpset() delsimps [append_assoc]
    1.51 +                                 addsimps [append_assoc RS sym])1);
    1.52 +be disjE 1;
    1.53 + by(Asm_simp_tac 1);
    1.54 +by(Clarify_tac 1);
    1.55 +by (Simp_tac 1);
    1.56 +qed "prefix_snoc";
    1.57 +Addsimps [prefix_snoc];
    1.58 +
    1.59 +goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
    1.60 +by (Simp_tac 1);
    1.61 +by (Fast_tac 1);
    1.62 +qed"Cons_prefix_Cons";
    1.63 +Addsimps [Cons_prefix_Cons];
    1.64 +
    1.65 +goalw thy [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";
    1.66 +by(Clarify_tac 1);
    1.67 +by (Simp_tac 1);
    1.68 +qed "prefix_prefix";
    1.69 +Addsimps [prefix_prefix];
    1.70 +
    1.71  (* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
    1.72  goalw Prefix.thy [prefix_def]
    1.73     "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
    1.74 @@ -33,9 +79,3 @@
    1.75  by (Simp_tac 1);
    1.76  by (Fast_tac 1);
    1.77  qed "prefix_Cons";
    1.78 -
    1.79 -goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
    1.80 -by (Simp_tac 1);
    1.81 -by (Fast_tac 1);
    1.82 -qed"Cons_prefix_Cons";
    1.83 -Addsimps [Cons_prefix_Cons];
     2.1 --- a/src/HOL/List.ML	Fri Feb 20 17:57:16 1998 +0100
     2.2 +++ b/src/HOL/List.ML	Sun Feb 22 14:12:23 1998 +0100
     2.3 @@ -6,8 +6,6 @@
     2.4  List lemmas
     2.5  *)
     2.6  
     2.7 -open List;
     2.8 -
     2.9  goal thy "!x. xs ~= x#xs";
    2.10  by (induct_tac "xs" 1);
    2.11  by (ALLGOALS Asm_simp_tac);
    2.12 @@ -46,7 +44,8 @@
    2.13  Addsimps [lists_Int_eq];
    2.14  
    2.15  
    2.16 -(** list_case **)
    2.17 +(**  Case analysis **)
    2.18 +section "Case analysis";
    2.19  
    2.20  val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    2.21  by (induct_tac "xs" 1);
    2.22 @@ -60,7 +59,6 @@
    2.23  bind_thm("list_eq_cases",
    2.24    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
    2.25  
    2.26 -
    2.27  (** length **)
    2.28  (* needs to come before "@" because of thm append_eq_append_conv *)
    2.29  
    2.30 @@ -509,6 +507,51 @@
    2.31  qed_spec_mp "nth_mem";
    2.32  Addsimps [nth_mem];
    2.33  
    2.34 +(**  More case analysis and induction **)
    2.35 +section "More case analysis and induction";
    2.36 +
    2.37 +val [prem] = goal thy
    2.38 +  "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
    2.39 +by(rtac measure_induct 1 THEN etac prem 1);
    2.40 +qed "length_induct";
    2.41 +
    2.42 +goal thy "xs ~= [] --> (? ys y. xs = ys@[y])";
    2.43 +by(res_inst_tac [("xs","xs")] length_induct 1);
    2.44 +by(Clarify_tac 1);
    2.45 +bd (neq_Nil_conv RS iffD1) 1;
    2.46 +by(Clarify_tac 1);
    2.47 +by(rename_tac "ys" 1);
    2.48 +by(case_tac "ys = []" 1);
    2.49 + by(res_inst_tac [("x","[]")] exI 1);
    2.50 + by(Asm_full_simp_tac 1);
    2.51 +by(eres_inst_tac [("x","ys")] allE 1);
    2.52 +by(Asm_full_simp_tac 1);
    2.53 +by(REPEAT(etac exE 1));
    2.54 +by(rename_tac "zs z" 1);
    2.55 +by(hyp_subst_tac 1);
    2.56 +by(res_inst_tac [("x","y#zs")] exI 1);
    2.57 +by(Simp_tac 1);
    2.58 +qed_spec_mp "neq_Nil_snocD";
    2.59 +
    2.60 +val prems = goal thy
    2.61 +  "[| xs=[] ==> P []; !!ys y. xs=ys@[y] ==> P(ys@[y]) |] ==> P xs";
    2.62 +by(case_tac "xs = []" 1);
    2.63 + by(Asm_simp_tac 1);
    2.64 + bes prems 1;
    2.65 +bd neq_Nil_snocD 1;
    2.66 +by(REPEAT(etac exE 1));
    2.67 +by(Asm_simp_tac 1);
    2.68 +bes prems 1;
    2.69 +qed "snoc_eq_cases";
    2.70 +
    2.71 +val prems = goal thy
    2.72 +  "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P(xs)";
    2.73 +by(res_inst_tac [("xs","xs")] length_induct 1);
    2.74 +by(res_inst_tac [("xs","xs")] snoc_eq_cases 1);
    2.75 + brs prems 1;
    2.76 +by(fast_tac (claset() addIs prems addss simpset()) 1);
    2.77 +qed "snoc_induct";
    2.78 +
    2.79  (** last & butlast **)
    2.80  
    2.81  goal thy "last(xs@[x]) = x";
    2.82 @@ -523,6 +566,12 @@
    2.83  qed "butlast_snoc";
    2.84  Addsimps [butlast_snoc];
    2.85  
    2.86 +goal thy "length(butlast xs) = length xs - 1";
    2.87 +by(res_inst_tac [("xs","xs")] snoc_induct 1);
    2.88 +by(ALLGOALS Asm_simp_tac);
    2.89 +qed "length_butlast";
    2.90 +Addsimps [length_butlast];
    2.91 +
    2.92  goal thy
    2.93    "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
    2.94  by (induct_tac "xs" 1);
     3.1 --- a/src/HOL/List.thy	Fri Feb 20 17:57:16 1998 +0100
     3.2 +++ b/src/HOL/List.thy	Sun Feb 22 14:12:23 1998 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  The datatype of finite lists.
     3.5  *)
     3.6  
     3.7 -List = Divides +
     3.8 +List = WF_Rel +
     3.9  
    3.10  datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
    3.11  
     4.1 --- a/src/HOL/WF_Rel.ML	Fri Feb 20 17:57:16 1998 +0100
     4.2 +++ b/src/HOL/WF_Rel.ML	Sun Feb 22 14:12:23 1998 +0100
     4.3 @@ -59,6 +59,11 @@
     4.4  qed "wf_measure";
     4.5  AddIffs [wf_measure];
     4.6  
     4.7 +val measure_induct = standard
     4.8 +    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
     4.9 +      (wf_measure RS wf_induct));
    4.10 +store_thm("measure_induct",measure_induct);
    4.11 +
    4.12  (*----------------------------------------------------------------------------
    4.13   * Wellfoundedness of lexicographic combinations
    4.14   *---------------------------------------------------------------------------*)