<commit_before>(*  Title:      HOL/Library/Quotient_List.thy
    Author:     <NAME> and <NAME>
*)

header {* Quotient infrastructure for the list type *}

theory Quotient_List
imports Main Quotient_Syntax
begin

declare [[map list = (map, list_all2)]]

lemma split_list_all:
  shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
  apply(auto)
  apply(case_tac x)
  apply(simp_all)
  done

lemma map_id[id_simps]:
  shows "map id = id"
  apply(simp add: fun_eq_iff)
  apply(rule allI)
  apply(induct_tac x)
  apply(simp_all)
  done

lemma list_all2_reflp:
  shows "equivp R \<Longrightarrow> list_all2 R xs xs"
  by (induct xs, simp_all add: equivp_reflp)

lemma list_all2_symp:
  assumes a: "equivp R"
  and b: "list_all2 R xs ys"
  shows "list_all2 R ys xs"
  using list_all2_lengthD[OF b] b
  apply(induct xs ys rule: list_induct2)
  apply(simp_all)
  apply(rule equivp_symp[OF a])
  apply(simp)
  done

thm list_induct3

lemma list_all2_transp:
  assumes a: "equivp R"
  and b: "list_all2 R xs1 xs2"
  and c: "list_all2 R xs2 xs3"
  shows "list_all2 R xs1 xs3"
  using list_all2_lengthD[OF b] list_all2_lengthD[OF c] b c
  apply(induct rule: list_induct3)
  apply(simp_all)
  apply(auto intro: equivp_transp[OF a])
  done

lemma list_equivp[quot_equiv]:
  assumes a: "equivp R"
  shows "equivp (list_all2 R)"
  apply (intro equivpI)
  unfolding reflp_def symp_def transp_def
  apply(simp add: list_all2_reflp[OF a])
  apply(blast intro: list_all2_symp[OF a])
  apply(blast intro: list_all2_transp[OF a])<commit_msg>removing something that probably slipped into the Quotient_List theory<commit_after>(*  Title:      HOL/Library/Quotient_List.thy
    Author:     <NAME> and <NAME>
*)

header {* Quotient infrastructure for the list type *}

theory Quotient_List
imports Main Quotient_Syntax
begin

declare [[map list = (map, list_all2)]]

lemma split_list_all:
  shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
  apply(auto)
  apply(case_tac x)
  apply(simp_all)
  done

lemma map_id[id_simps]:
  shows "map id = id"
  apply(simp add: fun_eq_iff)
  apply(rule allI)
  apply(induct_tac x)
  apply(simp_all)
  done

lemma list_all2_reflp:
  shows "equivp R \<Longrightarrow> list_all2 R xs xs"
  by (induct xs, simp_all add: equivp_reflp)

lemma list_all2_symp:
  assumes a: "equivp R"
  and b: "list_all2 R xs ys"
  shows "list_all2 R ys xs"
  using list_all2_lengthD[OF b] b
  apply(induct xs ys rule: list_induct2)
  apply(simp_all)
  apply(rule equivp_symp[OF a])
  apply(simp)
  done

lemma list_all2_transp:
  assumes a: "equivp R"
  and b: "list_all2 R xs1 xs2"
  and c: "list_all2 R xs2 xs3"
  shows "list_all2 R xs1 xs3"
  using list_all2_lengthD[OF b] list_all2_lengthD[OF c] b c
  apply(induct rule: list_induct3)
  apply(simp_all)
  apply(auto intro: equivp_transp[OF a])
  done

lemma list_equivp[quot_equiv]:
  assumes a: "equivp R"
  shows "equivp (list_all2 R)"
  apply (intro equivpI)
  unfolding reflp_def symp_def transp_def
  apply(simp add: list_all2_reflp[OF a])
  apply(blast intro: list_all2_symp[OF a])
  apply(blast intro: list_all2_transp[OF a])
{'fraction_non_alphanumeric': 0.10181355392936685, 'fraction_numerical': 0.016226535157492842, 'mean_word_length': 4.346938775510204, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 17, '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': '5196085', 'n_tokens_mistral': 1368, 'n_tokens_neox': 1325, 'n_words': 357}