<commit_before>(*  Title:      HOL/Semiring_Normalization.thy
    Author:     <NAME>, TU Muenchen
*)

header {* Semiring normalization *}

theory Semiring_Normalization
imports Numeral_Simprocs Nat_Transfer
uses
  "Tools/semiring_normalizer.ML"
begin

text {* Prelude *}

class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
  assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
begin

lemma crossproduct_noteq:
  "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c"
  by (simp add: crossproduct_eq)

lemma add_scale_eq_noteq:
  "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d"
proof (rule notI)
  assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
    and eq: "a + (r * c) = b + (r * d)"
  have "(0 * d) + (r * c) = (0 * c) + (r * d)"
    using add_imp_eq eq mult_zero_left by (simp add: cnd)
  then show False using crossproduct_eq [of 0 d] nz cnd by simp
qed

lemma add_0_iff:
  "b = b + a \<longleftrightarrow> a = 0"
  using add_imp_eq [of b a 0] by auto

end

sublocale idom < comm_semiring_1_cancel_crossproduct
proof
  fix w x y z<commit_msg>proper subclass instead of sublocale<commit_after>(*  Title:      HOL/Semiring_Normalization.thy
    Author:     <NAME>, TU Muenchen
*)

header {* Semiring normalization *}

theory Semiring_Normalization
imports Numeral_Simprocs Nat_Transfer
uses
  "Tools/semiring_normalizer.ML"
begin

text {* Prelude *}

class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
  assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
begin

lemma crossproduct_noteq:
  "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c"
  by (simp add: crossproduct_eq)

lemma add_scale_eq_noteq:
  "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d"
proof (rule notI)
  assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d"
    and eq: "a + (r * c) = b + (r * d)"
  have "(0 * d) + (r * c) = (0 * c) + (r * d)"
    using add_imp_eq eq mult_zero_left by (simp add: cnd)
  then show False using crossproduct_eq [of 0 d] nz cnd by simp
qed

lemma add_0_iff:
  "b = b + a \<longleftrightarrow> a = 0"
  using add_imp_eq [of b a 0] by auto

end

subclass (in idom) comm_semiring_1_cancel_crossproduct
proof
  fix w x y z
{'fraction_non_alphanumeric': 0.13287281592848435, 'fraction_numerical': 0.008939455505891914, 'mean_word_length': 3.4042933810375673, 'pattern_counts': {'":': 0, '<': 40, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5305732', 'n_tokens_mistral': 1050, 'n_tokens_neox': 979, 'n_words': 324}