<commit_before>(*  Title:      IPv4Addr.thy
    Authors:    <NAME>, <NAME>
*)
theory WordInterval
imports Main
  NumberWang
  "~~/src/HOL/Word/Word"
  "~~/src/HOL/Library/Code_Target_Nat" (*!*)
begin

text{*Intervals of consecutive words*}

value "(2::nat) < 2^32" (*without Code_Target_Nat, this would be really slow*)

  datatype ('a::len) wordinterval = WordInterval
                                        "('a::len) word" --"start (inclusive)"
                                        "('a::len) word" --"end (inclusive)"
                                  | RangeUnion "'a wordinterval" "'a wordinterval"

  fun wordinterval_to_set :: "'a::len wordinterval \<Rightarrow> ('a::len word) set" where
    "wordinterval_to_set (WordInterval start end) = {start .. end}" |
    "wordinterval_to_set (RangeUnion r1 r2) = (wordinterval_to_set r1) \<union> (wordinterval_to_set r2)"

  fun wordinterval_element :: "'a::len word \<Rightarrow> 'a::len wordinterval \<Rightarrow> bool" where
    "wordinterval_element el (WordInterval s e) = (s \<le> el \<and> el \<le> e)" |
    "wordinterval_element el (RangeUnion r1 r2) = (wordinterval_element el r1 \<or> wordinterval_element el r2)"
  lemma wordinterval_element_set_eq[simp]: "wordinterval_element el rg = (el \<in> wordinterval_to_set rg)"
    by(induction rg rule: wordinterval_element.induct) simp_all

  fun wordinterval_union :: "'a::len wordinterval \<Rightarrow> 'a::len wordinterval \<Rightarrow> 'a::len wordinterval" where 
    "wordinterval_union r1 r2 = RangeUnion r1 r2"
  lemma wordinterval_union_set_eq[simp]: "wordinterval_to_set (wordinterval_union r1 r2) = wordinterval_to_set r1 \<union> wordinterval_to_set r2" by simp

  fun wordinterval_empty :: "'a::len wordinterval \<Rightarrow> bool" where
    "wordinterval_empty (WordInterval s e) = (e < s)" |
    "wordinterval_empty (RangeUnion r1 r2) = (wordinterval_empty r1 \<and> wordinterval_empty r2)"
  lemma wordinterval_empty_set_eq[simp]: "wordinterval_empty r \<longleftrightarrow> wordinterval_to_set r = {}"
    by(induction r) auto

  context
  begin
    fun wordinterval_optimize_empty where
      "wordinterval_optimize_empty (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1 in (let r2o = wordinterval_optimize_empty r2 in (
        if wordinterval_empty r1o then r2o else (if wordinterval_empty r2o then r1o else (RangeUnion r1o r2o)))))" |
      "wordinterval_optimize_empty r = r"
    lemma wordinterval_optimize_empty_set_eq[simp]: "wordinterval_to_set (wordinterval_optimize_empty r) = wordinterval_to_set r"
      by(induction r) (simp_all add: Let_def)
    lemma wordinterval_optimize_empty_double[simp]: "wordinterval_optimize_empty (wordinterval_optimize_empty r) = wordinterval_optimize_empty r"
      apply(induction r)
      by(simp_all add: Let_def)
    private fun wordinterval_empty_shallow where
      "wordinterval_empty_shallow (WordInterval s e) = (e < s)" |
      "wordinterval_empty_shallow (RangeUnion _ _) = False"
    private lemma helper_optimize_shallow: "wordinterval_empty (wordinterval_optimize_empty r) = wordinterval_empty_shallow (wordinterval_optimize_empty r)"
      by(induction r) fastforce+
    private fun wordinterval_optimize_empty2 where
      "wordinterval_optimize_empty2 (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1 in (let r2o = wordinterval_optimize_empty r2 in (
        if wordinterval_empty_shallow r1o then r2o else (if wordinterval_empty_shallow r2o then r1o else (RangeUnion r1o r2o)))))" |
      "wordinterval_optimize_empty2 r = r"
    lemma wordinterval_optimize_empty_code[code_unfold]: "wordinterval_optimize_empty = wordinterval_optimize_empty2"
      by (subst fun_eq_iff, clarify, rename_tac r, induct_tac r)
         (unfold wordinterval_optimize_empty.simps wordinterval_optimize_empty2.simps Let_def helper_optimize_shallow[symmetric], simp_all)
  end

  definition Empty_WordInterval :: "'a::len wordinterval" where  "Empty_WordInterval \<equiv> WordInterval 1 0"
  lemma wordinterval_empty_Empty_WordInterval: "wordinterval_empty Empty_WordInterval" by(simp add: Empty_WordInterval_def)
  lemma Empty_WordInterval_set_eq[simp]: "wordinterval_to_set Empty_WordInterval = {}" by(simp add: Empty_WordInterval_def)

  fun wordinterval_to_list  :: "'a::len wordinterval \<Rightarrow> ('a::len wordinterval) list" where
    "wordinterval_to_list (RangeUnion r1 r2) = wordinterval_to_list r1 @ wordinterval_to_list r2" |
    "wordinterval_to_list r = (if wordinterval_empty r then [] else [r])"

  lemma wordinterval_to_list_set_eq: "(\<Union>set (map wordinterval_to_set (wordinterval_to_list rs))) = wordinterval_to_set rs"
  by(induction rs) simp_all

  fun list_to_wordinterval where
    "list_to_wordinterval [r] = r" |
    "list_to_wordinterval (r#rs) = (RangeUnion r (list_to_wordinterval rs))" |
    "list_to_wordinterval [] = Empty_WordInterval"

  lemma list_to_wordinterval_set_eq: "(\<Union>set (map wordinterval_to_set rs)) = wordinterval_to_set (list_to_wordinterval rs)"
    by(induction rs rule: list_to_wordinterval.induct) simp_all
  
  lemma list_to_wordinterval_set_eq_simp[simp]: "wordinterval_to_set (list_to_wordinterval (a # as)) = wordinterval_to_set (wordinterval_union a (list_to_wordinterval as))"
    by(cases as) auto
    
    
  fun wordinterval_linearize :: "('a::len) wordinterval \<Rightarrow> ('a::len) wordinterval" where
    "wordinterval_linearize rs = list_to_wordinterval (wordinterval_to_list rs)"
  lemma "wordinterval_to_set (wordinterval_linearize r) = wordinterval_to_set r"
    by(simp, metis list_to_wordinterval_set_eq wordinterval_to_list_set_eq)

  fun wordinterval_optimize_same where "wordinterval_optimize_same rs = list_to_wordinterval (remdups (wordinterval_to_list rs))"
  lemma wordinterval_optimize_same_set_eq[simp]: "wordinterval_to_set (wordinterval_optimize_same rs) = wordinterval_to_set rs"
   by(simp, subst list_to_wordinterval_set_eq[symmetric]) (metis image_set wordinterval_to_list_set_eq set_remdups)

  fun wordinterval_is_simple where "wordinterval_is_simple (WordInterval _ _) = True" | "wordinterval_is_simple (RangeUnion _ _) = False"
  fun wordintervalist_union_free where
    "wordintervalist_union_free (r#rs) = (wordinterval_is_simple r \<and> wordintervalist_union_free rs)" |
    "wordintervalist_union_free [] = True"
  lemma wordintervalist_union_freeX: "wordintervalist_union_free (r # rs) \<Longrightarrow> \<exists> s e. r = WordInterval s e"
    by (induction rs) (cases r, simp, simp)+
  lemma wordintervalist_union_free_append: "wordintervalist_union_free (a@b) = (wordintervalist_union_free a \<and> wordintervalist_union_free b)"<commit_msg>cleaned<commit_after>(*  Title:      IPv4Addr.thy
    Authors:    <NAME>, <NAME>
*)
theory WordInterval
imports Main
  NumberWang
  "~~/src/HOL/Word/Word"
  "~~/src/HOL/Library/Code_Target_Nat" (*!*)
begin

text{*Intervals of consecutive words*}

value "(2::nat) < 2^32" (*without Code_Target_Nat, this would be really slow*)

  datatype ('a::len) wordinterval = WordInterval
                                        "('a::len) word" --"start (inclusive)"
                                        "('a::len) word" --"end (inclusive)"
                                  | RangeUnion "'a wordinterval" "'a wordinterval"

  fun wordinterval_to_set :: "'a::len wordinterval \<Rightarrow> ('a::len word) set" where
    "wordinterval_to_set (WordInterval start end) = {start .. end}" |
    "wordinterval_to_set (RangeUnion r1 r2) = (wordinterval_to_set r1) \<union> (wordinterval_to_set r2)"

  fun wordinterval_element :: "'a::len word \<Rightarrow> 'a::len wordinterval \<Rightarrow> bool" where
    "wordinterval_element el (WordInterval s e) = (s \<le> el \<and> el \<le> e)" |
    "wordinterval_element el (RangeUnion r1 r2) = (wordinterval_element el r1 \<or> wordinterval_element el r2)"
  lemma wordinterval_element_set_eq[simp]: "wordinterval_element el rg = (el \<in> wordinterval_to_set rg)"
    by(induction rg rule: wordinterval_element.induct) simp_all

  fun wordinterval_union :: "'a::len wordinterval \<Rightarrow> 'a::len wordinterval \<Rightarrow> 'a::len wordinterval" where 
    "wordinterval_union r1 r2 = RangeUnion r1 r2"
  lemma wordinterval_union_set_eq[simp]: "wordinterval_to_set (wordinterval_union r1 r2) = wordinterval_to_set r1 \<union> wordinterval_to_set r2" by simp

  fun wordinterval_empty :: "'a::len wordinterval \<Rightarrow> bool" where
    "wordinterval_empty (WordInterval s e) = (e < s)" |
    "wordinterval_empty (RangeUnion r1 r2) = (wordinterval_empty r1 \<and> wordinterval_empty r2)"
  lemma wordinterval_empty_set_eq[simp]: "wordinterval_empty r \<longleftrightarrow> wordinterval_to_set r = {}"
    by(induction r) auto

  context
  begin
    fun wordinterval_optimize_empty where
      "wordinterval_optimize_empty (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1 in (let r2o = wordinterval_optimize_empty r2 in (
        if wordinterval_empty r1o then r2o else (if wordinterval_empty r2o then r1o else (RangeUnion r1o r2o)))))" |
      "wordinterval_optimize_empty r = r"
    lemma wordinterval_optimize_empty_set_eq[simp]: "wordinterval_to_set (wordinterval_optimize_empty r) = wordinterval_to_set r"
      by(induction r) (simp_all add: Let_def)
    lemma wordinterval_optimize_empty_double[simp]: "wordinterval_optimize_empty (wordinterval_optimize_empty r) = wordinterval_optimize_empty r"
      apply(induction r)
      by(simp_all add: Let_def)
    private fun wordinterval_empty_shallow where
      "wordinterval_empty_shallow (WordInterval s e) = (e < s)" |
      "wordinterval_empty_shallow (RangeUnion _ _) = False"
    private lemma helper_optimize_shallow: "wordinterval_empty (wordinterval_optimize_empty r) = wordinterval_empty_shallow (wordinterval_optimize_empty r)"
      by(induction r) fastforce+
    private fun wordinterval_optimize_empty2 where
      "wordinterval_optimize_empty2 (RangeUnion r1 r2) = (let r1o = wordinterval_optimize_empty r1 in (let r2o = wordinterval_optimize_empty r2 in (
        if wordinterval_empty_shallow r1o then r2o else (if wordinterval_empty_shallow r2o then r1o else (RangeUnion r1o r2o)))))" |
      "wordinterval_optimize_empty2 r = r"
    lemma wordinterval_optimize_empty_code[code_unfold]: "wordinterval_optimize_empty = wordinterval_optimize_empty2"
      by (subst fun_eq_iff, clarify, rename_tac r, induct_tac r)
         (unfold wordinterval_optimize_empty.simps wordinterval_optimize_empty2.simps Let_def helper_optimize_shallow[symmetric], simp_all)
  end

  definition Empty_WordInterval :: "'a::len wordinterval" where  "Empty_WordInterval \<equiv> WordInterval 1 0"
  lemma wordinterval_empty_Empty_WordInterval: "wordinterval_empty Empty_WordInterval" by(simp add: Empty_WordInterval_def)
  lemma Empty_WordInterval_set_eq[simp]: "wordinterval_to_set Empty_WordInterval = {}" by(simp add: Empty_WordInterval_def)

  fun wordinterval_to_list  :: "'a::len wordinterval \<Rightarrow> ('a::len wordinterval) list" where
    "wordinterval_to_list (RangeUnion r1 r2) = wordinterval_to_list r1 @ wordinterval_to_list r2" |
    "wordinterval_to_list r = (if wordinterval_empty r then [] else [r])"

  lemma wordinterval_to_list_set_eq: "(\<Union>set (map wordinterval_to_set (wordinterval_to_list rs))) = wordinterval_to_set rs"
  by(induction rs) simp_all

  fun list_to_wordinterval where
    "list_to_wordinterval [r] = r" |
    "list_to_wordinterval (r#rs) = (RangeUnion r (list_to_wordinterval rs))" |
    "list_to_wordinterval [] = Empty_WordInterval"

  lemma list_to_wordinterval_set_eq: "(\<Union>set (map wordinterval_to_set rs)) = wordinterval_to_set (list_to_wordinterval rs)"
    by(induction rs rule: list_to_wordinterval.induct) simp_all
  
  lemma list_to_wordinterval_set_eq_simp[simp]: "wordinterval_to_set (list_to_wordinterval (a # as)) = wordinterval_to_set (wordinterval_union a (list_to_wordinterval as))"
    by(cases as) auto
    
  (*
  fun wordinterval_linearize :: "('a::len) wordinterval \<Rightarrow> ('a::len) wordinterval" where
    "wordinterval_linearize rs = list_to_wordinterval (wordinterval_to_list rs)"
  lemma "wordinterval_to_set (wordinterval_linearize r) = wordinterval_to_set r"
    by(simp, metis list_to_wordinterval_set_eq wordinterval_to_list_set_eq)
  *)

  fun wordinterval_optimize_same where "wordinterval_optimize_same rs = list_to_wordinterval (remdups (wordinterval_to_list rs))"
  lemma wordinterval_optimize_same_set_eq[simp]: "wordinterval_to_set (wordinterval_optimize_same rs) = wordinterval_to_set rs"
   by(simp, subst list_to_wordinterval_set_eq[symmetric]) (metis image_set wordinterval_to_list_set_eq set_remdups)

  fun wordinterval_is_simple where "wordinterval_is_simple (WordInterval _ _) = True" | "wordinterval_is_simple (RangeUnion _ _) = False"
  fun wordintervalist_union_free where
    "wordintervalist_union_free (r#rs) = (wordinterval_is_simple r \<and> wordintervalist_union_free rs)" |
    "wordintervalist_union_free [] = True"
  lemma wordintervalist_union_freeX: "wordintervalist_union_free (r # rs) \<Longrightarrow> \<exists> s e. r = WordInterval s e"
    by (induction rs) (cases r, simp, simp)+
  lemma wordintervalist_union_free_append: "wordintervalist_union_free (a@b) = (wordintervalist_union_free a \<and> wordintervalist_union_free b)"
{'fraction_non_alphanumeric': 0.09311771342610003, 'fraction_numerical': 0.009025949605114705, 'mean_word_length': 5.189944134078212, 'pattern_counts': {'":': 0, '<': 61, '<?xml version=': 0, '>': 55, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4005746', 'n_tokens_mistral': 4540, 'n_tokens_neox': 4361, 'n_words': 1037}