1 theory GeneralRegexBound 

     2   imports "BasicIdentities" 

     3 begin

     4 

     5 lemma size_geq1:

     6   shows "rsize r \<ge> 1"

     7   by (induct r) auto 

     8 

     9 definition RSEQ_set where

    10   "RSEQ_set A n \<equiv> {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A \<and> rsize r1 + rsize r2 \<le> n}"

    11 

    12 definition RSEQ_set_cartesian where

    13   "RSEQ_set_cartesian A  = {RSEQ r1 r2 | r1 r2. r1 \<in> A \<and> r2 \<in> A}"

    14 

    15 definition RALT_set where

    16   "RALT_set A n \<equiv> {RALTS rs | rs. set rs \<subseteq> A \<and> rsizes rs \<le> n}"

    17 

    18 definition RALTs_set where

    19   "RALTs_set A n \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n}"

    20 

    21 definition RNTIMES_set where

    22   "RNTIMES_set A n \<equiv> {RNTIMES r m | m r. r \<in> A \<and> rsize r + m \<le> n}"

    23 

    24 

    25 definition

    26   "sizeNregex N \<equiv> {r. rsize r \<le> N}"

    27 

    28 

    29 lemma sizenregex_induct1:

    30   "sizeNregex (Suc n) = (({RZERO, RONE} \<union> {RCHAR c| c. True}) 

    31                          \<union> (RSTAR ` sizeNregex n) 

    32                          \<union> (RSEQ_set (sizeNregex n) n)

    33                          \<union> (RALTs_set (sizeNregex n) n))

    34                          \<union> (RNTIMES_set (sizeNregex n) n)"

    35   apply(auto)

    36         apply(case_tac x)

    37              apply(auto simp add: RSEQ_set_def)

    38   using sizeNregex_def apply force

    39   using sizeNregex_def apply auto[1]

    40   apply (simp add: sizeNregex_def)

    41          apply (simp add: sizeNregex_def)

    42          apply (simp add: RALTs_set_def)

    43   apply (metis imageI list.set_map member_le_sum_list order_trans)

    44   apply (simp add: sizeNregex_def)

    45         apply (simp add: sizeNregex_def)

    46   apply (simp add: RNTIMES_set_def)

    47   apply (simp add: sizeNregex_def)

    48   using sizeNregex_def apply force

    49   apply (simp add: sizeNregex_def)

    50   apply (simp add: sizeNregex_def)

    51   apply (simp add: sizeNregex_def)

    52     apply (simp add: RALTs_set_def)

    53   apply(simp add: sizeNregex_def)

    54   apply(auto)

    55   using ex_in_conv apply fastforce

    56   apply (simp add: RNTIMES_set_def)

    57   apply(simp add: sizeNregex_def)

    58   by force

    59   

    60 

    61 lemma s4:

    62   "RSEQ_set A n \<subseteq> RSEQ_set_cartesian A"

    63   using RSEQ_set_cartesian_def RSEQ_set_def by fastforce

    64 

    65 lemma s5:

    66   assumes "finite A"

    67   shows "finite (RSEQ_set_cartesian A)"

    68   using assms

    69   apply(subgoal_tac "RSEQ_set_cartesian A = (\<lambda>(x1, x2). RSEQ x1 x2) ` (A \<times> A)")

    70   apply simp

    71   unfolding RSEQ_set_cartesian_def

    72   apply(auto)

    73   done

    74 

    75 

    76 definition RALTs_set_length

    77   where

    78   "RALTs_set_length A n l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> rsizes rs \<le> n \<and> length rs \<le> l}"

    79 

    80 

    81 definition RALTs_set_length2

    82   where

    83   "RALTs_set_length2 A l \<equiv> {RALTS rs | rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}"

    84 

    85 definition set_length2

    86   where

    87   "set_length2 A l \<equiv> {rs. \<forall>r \<in> set rs. r \<in> A \<and> length rs \<le> l}"

    88 

    89 

    90 lemma r000: 

    91   shows "RALTs_set_length A n l \<subseteq> RALTs_set_length2 A l"

    92   apply(auto simp add: RALTs_set_length2_def RALTs_set_length_def)

    93   done

    94 

    95 

    96 lemma r02: 

    97   shows "set_length2 A 0 \<subseteq> {[]}"

    98   apply(auto simp add: set_length2_def)

    99   apply(case_tac x)

   100   apply(auto)

   101   done

   102 

   103 lemma r03:

   104   shows "set_length2 A (Suc n) \<subseteq> 

   105           {[]} \<union> (\<lambda>(h, t). h # t) ` (A \<times> (set_length2 A n))"

   106   apply(auto simp add: set_length2_def)

   107   apply(case_tac x)

   108    apply(auto)

   109   done

   110 

   111 lemma r1:

   112   assumes "finite A" 

   113   shows "finite (set_length2 A n)"

   114   using assms

   115   apply(induct n)

   116   apply(rule finite_subset)

   117     apply(rule r02)

   118    apply(simp)    

   119   apply(rule finite_subset)

   120    apply(rule r03)

   121   apply(simp)

   122   done

   123 

   124 lemma size_sum_more_than_len:

   125   shows "rsizes rs \<ge> length rs"

   126   apply(induct rs)

   127    apply simp

   128   apply simp

   129   apply(subgoal_tac "rsize a \<ge> 1")

   130    apply linarith

   131   using size_geq1 by auto

   132 

   133 

   134 lemma sum_list_len:

   135   shows "rsizes rs \<le> n \<Longrightarrow> length rs \<le> n"

   136   by (meson order.trans size_sum_more_than_len)

   137 

   138 

   139 lemma t2:

   140   shows "RALTs_set A n \<subseteq> RALTs_set_length A n n"

   141   unfolding RALTs_set_length_def RALTs_set_def

   142   apply(auto)

   143   using sum_list_len by blast

   144 

   145 lemma s8_aux:

   146   assumes "finite A" 

   147   shows "finite (RALTs_set_length A n n)"

   148 proof -

   149   have "finite A" by fact

   150   then have "finite (set_length2 A n)"

   151     by (simp add: r1)

   152   moreover have "(RALTS ` (set_length2 A n)) = RALTs_set_length2 A n"

   153     unfolding RALTs_set_length2_def set_length2_def

   154     by (auto)

   155   ultimately have "finite (RALTs_set_length2 A n)"

   156     by (metis finite_imageI)

   157   then show ?thesis

   158     by (metis infinite_super r000)

   159 qed

   160 

   161 lemma char_finite:

   162   shows "finite  {RCHAR c |c. True}"

   163   apply simp

   164   apply(subgoal_tac "finite (RCHAR ` (UNIV::char set))")

   165    prefer 2

   166    apply simp

   167   by (simp add: full_SetCompr_eq)

   168 

   169 thm RNTIMES_set_def

   170 

   171 lemma s9_aux0:

   172   shows "RNTIMES_set (insert r A) n \<subseteq> RNTIMES_set A n \<union> (\<Union> i \<in> {..n}. {RNTIMES r i})"

   173 apply(auto simp add: RNTIMES_set_def)

   174   done

   175 

   176 lemma s9_aux:

   177   assumes "finite A"

   178   shows "finite (RNTIMES_set A n)"

   179   using assms

   180   apply(induct A arbitrary: n)

   181    apply(auto simp add: RNTIMES_set_def)[1]

   182   apply(subgoal_tac "finite (RNTIMES_set F n \<union> (\<Union> i \<in> {..n}. {RNTIMES x i}))")

   183   apply (metis finite_subset s9_aux0)

   184   by blast

   185 

   186 lemma finite_size_n:

   187   shows "finite (sizeNregex n)"

   188   apply(induct n)

   189    apply(simp add: sizeNregex_def)

   190   apply (metis (mono_tags, lifting) not_finite_existsD not_one_le_zero size_geq1)

   191   apply(subst sizenregex_induct1)

   192   apply(simp only: finite_Un)

   193   apply(rule conjI)+

   194   apply(simp)

   195   

   196   using char_finite apply blast

   197     apply(simp)

   198    apply(rule finite_subset)

   199     apply(rule s4)

   200    apply(rule s5)

   201    apply(simp)

   202   apply(rule finite_subset)

   203    apply(rule t2)

   204   apply(rule s8_aux)

   205    apply(simp)

   206   by (simp add: s9_aux)

   207 

   208 lemma three_easy_cases0: 

   209   shows "rsize (rders_simp RZERO s) \<le> Suc 0"

   210   apply(induct s)

   211    apply simp

   212   apply simp

   213   done

   214 

   215 

   216 lemma three_easy_cases1: 

   217   shows "rsize (rders_simp RONE s) \<le> Suc 0"

   218     apply(induct s)

   219    apply simp

   220   apply simp

   221   using three_easy_cases0 by auto

   222 

   223 

   224 lemma three_easy_casesC: 

   225   shows "rsize (rders_simp (RCHAR c) s) \<le> Suc 0"

   226   apply(induct s)

   227    apply simp

   228   apply simp

   229   apply(case_tac " a = c")

   230   using three_easy_cases1 apply blast

   231   apply simp

   232   using three_easy_cases0 by force

   233   

   234 

   235 unused_thms

   236 

   237 

   238 end

   239