<commit_before>(* Author: <NAME>, <NAME> *)

header {* Preorders with explicit equivalence relation *}

theory Preorder
imports Orderings
begin

context preorder
begin

definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"

notation
  equiv ("op ~~") and
  equiv ("(_/ ~~ _)" [51, 51] 50)
  
notation (xsymbols)
  equiv ("op \<approx>") and
  equiv ("(_/ \<approx> _)"  [51, 51] 50)

notation (HTML output)
  equiv ("op \<approx>") and
  equiv ("(_/ \<approx> _)"  [51, 51] 50)

lemma refl [iff]:
  "x \<approx> x"
  unfolding equiv_def by simp

lemma trans:<commit_msg>better to have distinguished class for preorders<commit_after>(* Author: <NAME>, <NAME> *)

header {* Preorders with explicit equivalence relation *}

theory Preorder
imports Orderings
begin

class preorder_equiv = preorder
begin

definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
  "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"

notation
  equiv ("op ~~") and
  equiv ("(_/ ~~ _)" [51, 51] 50)
  
notation (xsymbols)
  equiv ("op \<approx>") and
  equiv ("(_/ \<approx> _)"  [51, 51] 50)

notation (HTML output)
  equiv ("op \<approx>") and
  equiv ("(_/ \<approx> _)"  [51, 51] 50)

lemma refl [iff]:
  "x \<approx> x"
  unfolding equiv_def by simp

lemma trans:
{'fraction_non_alphanumeric': 0.1706408345752608, 'fraction_numerical': 0.026825633383010434, 'mean_word_length': 3.7793594306049823, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 29, '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': '6787809', 'n_tokens_mistral': 544, 'n_tokens_neox': 466, 'n_words': 166}