<commit_before>(*  Title:      HOL/List
    ID:         $Id$
    Author:     <NAME>
    Copyright   1994 TU Muenchen

List lemmas
*)

Goal "!x. xs ~= x#xs";
by (induct_tac "xs" 1);
by Auto_tac;
qed_spec_mp "not_Cons_self";
bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
Addsimps [not_Cons_self,not_Cons_self2];

Goal "(xs ~= []) = (? y ys. xs = y#ys)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "neq_Nil_conv";

(* Induction over the length of a list: *)
val [prem] = Goal
  "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
by (rtac measure_induct 1 THEN etac prem 1);
qed "length_induct";


(** "lists": the list-forming operator over sets **)

Goalw lists.defs "A<=B ==> lists A <= lists B";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "lists_mono";

val listsE = lists.mk_cases "x#l : lists A";
AddSEs [listsE];
AddSIs lists.intrs;

Goal "l: lists A ==> l: lists B --> l: lists (A Int B)";
by (etac lists.induct 1);
by (ALLGOALS Blast_tac);
qed_spec_mp "lists_IntI";

Goal "lists (A Int B) = lists A Int lists B";
by (rtac (mono_Int RS equalityI) 1);
by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1);
by (blast_tac (claset() addSIs [lists_IntI]) 1);
qed "lists_Int_eq";
Addsimps [lists_Int_eq];


(**  Case analysis **)
section "Case analysis";

val prems = Goal "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
by (induct_tac "xs" 1);
by (REPEAT(resolve_tac prems 1));
qed "list_cases";

Goal "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
by (induct_tac "xs" 1);
by (Blast_tac 1);
by (Blast_tac 1);
bind_thm("list_eq_cases",
  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));

(** length **)
(* needs to come before "@" because of thm append_eq_append_conv *)

section "length";

Goal "length(xs@ys) = length(xs)+length(ys)";
by (induct_tac "xs" 1);
by Auto_tac;
qed"length_append";
Addsimps [length_append];

Goal "length (map f xs) = length xs";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_map";
Addsimps [length_map];

Goal "length(rev xs) = length(xs)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_rev";
Addsimps [length_rev];

Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
by (exhaust_tac "xs" 1);
by Auto_tac;
qed "length_tl";
Addsimps [length_tl];

Goal "(length xs = 0) = (xs = [])";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_0_conv";
AddIffs [length_0_conv];

Goal "(0 = length xs) = (xs = [])";
by (induct_tac "xs" 1);
by Auto_tac;
qed "zero_length_conv";
AddIffs [zero_length_conv];

Goal "(0 < length xs) = (xs ~= [])";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_greater_0_conv";
AddIffs [length_greater_0_conv];

Goal "(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_Suc_conv";

(** @ - append **)<commit_msg>Modifid length_tl<commit_after>(*  Title:      HOL/List
    ID:         $Id$
    Author:     <NAME>
    Copyright   1994 TU Muenchen

List lemmas
*)

Goal "!x. xs ~= x#xs";
by (induct_tac "xs" 1);
by Auto_tac;
qed_spec_mp "not_Cons_self";
bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
Addsimps [not_Cons_self,not_Cons_self2];

Goal "(xs ~= []) = (? y ys. xs = y#ys)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "neq_Nil_conv";

(* Induction over the length of a list: *)
val [prem] = Goal
  "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
by (rtac measure_induct 1 THEN etac prem 1);
qed "length_induct";


(** "lists": the list-forming operator over sets **)

Goalw lists.defs "A<=B ==> lists A <= lists B";
by (rtac lfp_mono 1);
by (REPEAT (ares_tac basic_monos 1));
qed "lists_mono";

val listsE = lists.mk_cases "x#l : lists A";
AddSEs [listsE];
AddSIs lists.intrs;

Goal "l: lists A ==> l: lists B --> l: lists (A Int B)";
by (etac lists.induct 1);
by (ALLGOALS Blast_tac);
qed_spec_mp "lists_IntI";

Goal "lists (A Int B) = lists A Int lists B";
by (rtac (mono_Int RS equalityI) 1);
by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1);
by (blast_tac (claset() addSIs [lists_IntI]) 1);
qed "lists_Int_eq";
Addsimps [lists_Int_eq];


(**  Case analysis **)
section "Case analysis";

val prems = Goal "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
by (induct_tac "xs" 1);
by (REPEAT(resolve_tac prems 1));
qed "list_cases";

Goal "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
by (induct_tac "xs" 1);
by (Blast_tac 1);
by (Blast_tac 1);
bind_thm("list_eq_cases",
  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));

(** length **)
(* needs to come before "@" because of thm append_eq_append_conv *)

section "length";

Goal "length(xs@ys) = length(xs)+length(ys)";
by (induct_tac "xs" 1);
by Auto_tac;
qed"length_append";
Addsimps [length_append];

Goal "length (map f xs) = length xs";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_map";
Addsimps [length_map];

Goal "length(rev xs) = length(xs)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_rev";
Addsimps [length_rev];

Goal "length(tl xs) = (length xs) - 1";
by (exhaust_tac "xs" 1);
by Auto_tac;
qed "length_tl";
Addsimps [length_tl];

Goal "(length xs = 0) = (xs = [])";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_0_conv";
AddIffs [length_0_conv];

Goal "(0 = length xs) = (xs = [])";
by (induct_tac "xs" 1);
by Auto_tac;
qed "zero_length_conv";
AddIffs [zero_length_conv];

Goal "(0 < length xs) = (xs ~= [])";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_greater_0_conv";
AddIffs [length_greater_0_conv];

Goal "(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "length_Suc_conv";

(** @ - append **)
{'fraction_non_alphanumeric': 0.18809056872882868, 'fraction_numerical': 0.014262791941522553, 'mean_word_length': 4.521653543307087, 'pattern_counts': {'":': 2, '<': 13, '<?xml version=': 0, '>': 26, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1017130', 'n_tokens_mistral': 2620, 'n_tokens_neox': 2512, 'n_words': 710}