<commit_before>theory WordInterval_Lists
imports WordInterval
  "../Common/Negation_Type"
begin

subsection{*WordInterval to List*}
text{*A list of @{text "(start, end)"} tuples.*}

  fun br2l :: "'a::len wordinterval \<Rightarrow> ('a::len word \<times> 'a::len word) list" where
    "br2l (RangeUnion r1 r2) = br2l r1 @ br2l r2" |
    "br2l (WordInterval s e) = (if e < s then [] else [(s,e)])"
  
  fun l2br :: "('a::len word \<times> 'a::len word) list \<Rightarrow> 'a::len wordinterval" where
    "l2br [] = Empty_WordInterval" | 
    "l2br [(s,e)] = (WordInterval s e)" | 
    "l2br ((s,e)#rs) = (RangeUnion (WordInterval s e) (l2br rs))"
  

  lemma l2br_append: "wordinterval_to_set (l2br (l1@l2)) = wordinterval_to_set (l2br l1) \<union> wordinterval_to_set (l2br l2)"
    apply(induction l1 arbitrary: l2 rule:l2br.induct)
      apply(simp_all)
     apply(case_tac l2)
      apply(simp_all)
    by blast
  
  lemma l2br_br2l: "wordinterval_to_set (l2br (br2l r)) = wordinterval_to_set r"
    by(induction r) (simp_all add: l2br_append)

  lemma l2br: "wordinterval_to_set (l2br l) = (\<Union> (i,j) \<in> set l. {i .. j})"
    by(induction l rule: l2br.induct, simp_all)<commit_msg>tuned<commit_after>theory WordInterval_Lists
imports WordInterval
  "../Common/Negation_Type"
begin

subsection{*WordInterval to List*}
text{*A list of @{text "(start, end)"} tuples.*}

  fun br2l :: "'a::len wordinterval \<Rightarrow> ('a::len word \<times> 'a::len word) list" where
    "br2l (RangeUnion r1 r2) = br2l r1 @ br2l r2" |
    "br2l (WordInterval s e) = (if e < s then [] else [(s,e)])"
  
  fun l2br :: "('a::len word \<times> 'a::len word) list \<Rightarrow> 'a::len wordinterval" where
    "l2br [] = Empty_WordInterval" | 
    "l2br [(s,e)] = (WordInterval s e)" | 
    "l2br ((s,e)#rs) = (RangeUnion (WordInterval s e) (l2br rs))"
  

  lemma l2br_append: "wordinterval_to_set (l2br (l1@l2)) = wordinterval_to_set (l2br l1) \<union> wordinterval_to_set (l2br l2)"
    proof(induction l1 arbitrary: l2 rule:l2br.induct)
    case 1 thus ?case by simp
    next
    case (2 s e l2) thus ?case by (cases l2) simp_all
    next
    case 3 thus ?case by force
    qed
  
  lemma l2br_br2l: "wordinterval_to_set (l2br (br2l r)) = wordinterval_to_set r"
    by(induction r) (simp_all add: l2br_append)

  lemma l2br: "wordinterval_to_set (l2br l) = (\<Union> (i,j) \<in> set l. {i .. j})"
    by(induction l rule: l2br.induct, simp_all)
{'fraction_non_alphanumeric': 0.15545529122231339, 'fraction_numerical': 0.029532403609515995, 'mean_word_length': 3.8392857142857144, 'pattern_counts': {'":': 0, '<': 19, '<?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': '1339627', 'n_tokens_mistral': 1036, 'n_tokens_neox': 991, 'n_words': 271}