1 theory Exercises

     2   imports Spec "~~/src/HOL/Library/Infinite_Set"

     3 begin

     4 

     5 section {* Some Fun Facts *}

     6 

     7 fun

     8  zeroable :: "rexp \<Rightarrow> bool"

     9 where

    10   "zeroable (ZERO) \<longleftrightarrow> True"

    11 | "zeroable (ONE) \<longleftrightarrow> False"

    12 | "zeroable (CH c) \<longleftrightarrow> False"

    13 | "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2"

    14 | "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2"

    15 | "zeroable (STAR r) \<longleftrightarrow> False"

    16 

    17 lemma zeroable_correctness:

    18   shows "zeroable r \<longleftrightarrow> L r = {}"

    19 by(induct r)(auto simp add: Sequ_def)

    20 

    21 

    22 fun

    23  atmostempty :: "rexp \<Rightarrow> bool"

    24 where

    25   "atmostempty (ZERO) \<longleftrightarrow> True"

    26 | "atmostempty (ONE) \<longleftrightarrow> True"

    27 | "atmostempty (CH c) \<longleftrightarrow> False"

    28 | "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2"

    29 | "atmostempty (SEQ r1 r2) \<longleftrightarrow> 

    30      zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"

    31 | "atmostempty (STAR r) = atmostempty r"

    32 

    33 

    34 

    35 fun

    36  somechars :: "rexp \<Rightarrow> bool"

    37 where

    38   "somechars (ZERO) \<longleftrightarrow> False"

    39 | "somechars (ONE) \<longleftrightarrow> False"

    40 | "somechars (CH c) \<longleftrightarrow> True"

    41 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2"

    42 | "somechars (SEQ r1 r2) \<longleftrightarrow> 

    43       (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> 

    44       (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)"

    45 | "somechars (STAR r) \<longleftrightarrow> somechars r"

    46 

    47 lemma somechars_correctness:

    48   shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)"

    49 apply(induct r)

    50 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def)

    51 using Nil_is_append_conv apply blast

    52 apply blast

    53   apply(auto)

    54   by (metis Star_decomp hd_Cons_tl list.distinct(1))

    55 

    56 lemma atmostempty_correctness_aux:

    57   shows "atmostempty r \<longleftrightarrow> \<not> somechars r"

    58 apply(induct r)

    59 apply(simp_all)

    60 apply(auto simp add: zeroable_correctness nullable_correctness somechars_correctness)

    61 done

    62 

    63 lemma atmostempty_correctness:

    64   shows "atmostempty r \<longleftrightarrow> L r \<subseteq> {[]}"

    65 by(auto simp add: atmostempty_correctness_aux somechars_correctness)

    66 

    67 fun

    68  leastsinglechar :: "rexp \<Rightarrow> bool"

    69 where

    70   "leastsinglechar (ZERO) \<longleftrightarrow> False"

    71 | "leastsinglechar (ONE) \<longleftrightarrow> False"

    72 | "leastsinglechar (CH c) \<longleftrightarrow> True"

    73 | "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2"

    74 | "leastsinglechar (SEQ r1 r2) \<longleftrightarrow> 

    75       (if (zeroable r1 \<or> zeroable r2) then False

    76        else ((nullable r1 \<and> leastsinglechar r2) \<or> (nullable r2 \<and> leastsinglechar r1)))"

    77 | "leastsinglechar (STAR r) \<longleftrightarrow> leastsinglechar r"

    78 

    79 lemma leastsinglechar_correctness:

    80   "leastsinglechar r \<longleftrightarrow> (\<exists>c. [c] \<in> L r)"

    81   apply(induct r)

    82   apply(simp)

    83   apply(simp)

    84   apply(simp)

    85   prefer 2

    86   apply(simp)

    87   apply(blast)

    88   prefer 2

    89   apply(simp)

    90   using Star.step Star_decomp apply fastforce

    91   apply(simp add: Sequ_def zeroable_correctness nullable_correctness)

    92   by (metis append_Nil append_is_Nil_conv butlast_append butlast_snoc)

    93 

    94 fun

    95  infinitestrings :: "rexp \<Rightarrow> bool"

    96 where

    97   "infinitestrings (ZERO) = False"

    98 | "infinitestrings (ONE) = False"

    99 | "infinitestrings (CH c) = False"

   100 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"

   101 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> 

   102       (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"

   103 | "infinitestrings (STAR r) = (\<not> atmostempty r)"

   104 

   105 

   106 

   107 

   108 

   109 lemma Star_atmostempty:

   110   assumes "A \<subseteq> {[]}"

   111   shows "A\<star> \<subseteq> {[]}"

   112   using assms

   113   using Star_decomp concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD 

   114   apply(auto)

   115 proof -

   116   fix x :: "char list"

   117   assume a1: "x \<in> A\<star>"

   118   assume "\<And>c x A. c # x \<in> A\<star> \<Longrightarrow> \<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"

   119   then have f2: "\<forall>cs C c. \<exists>csa. c # csa \<in> C \<or> c # cs \<notin> C\<star>"

   120     by auto

   121   obtain cc :: "char list \<Rightarrow> char" and ccs :: "char list \<Rightarrow> char list" where

   122     "\<And>cs. cs = [] \<or> cc cs # ccs cs = cs"

   123     by (metis (no_types) list.exhaust)

   124   then show "x = []"

   125     using f2 a1 by (metis assms empty_iff insert_iff list.distinct(1) subset_singletonD)

   126 qed

   127   

   128 

   129 lemma Star_empty_string_finite:

   130   shows "finite ({[]}\<star>)"

   131 using Star_atmostempty infinite_super by auto

   132 

   133 lemma Star_empty_finite:

   134   shows "finite ({}\<star>)"

   135 using Star_atmostempty infinite_super by auto

   136 

   137 lemma Star_concat_replicate:

   138   assumes "s \<in> A"

   139   shows "concat (replicate n s) \<in> A\<star>"

   140 using assms

   141 by (induct n) (auto)

   142 

   143 

   144 lemma concat_replicate_inj:

   145   assumes "concat (replicate n s) = concat (replicate m s)" "s \<noteq> []"

   146   shows "n = m"

   147 using assms

   148 apply(induct n arbitrary: m)

   149 apply(auto)[1]

   150 apply(auto)

   151 apply(case_tac m)

   152 apply(clarify)

   153 apply(simp only: replicate.simps concat.simps)

   154 apply blast

   155 by simp

   156 

   157 lemma A0:

   158   assumes "finite (A ;; B)" "B \<noteq> {}"

   159   shows "finite A"

   160 apply(subgoal_tac "\<exists>s. s \<in> B")

   161 apply(erule exE)

   162 apply(subgoal_tac "finite {s1 @ s |s1. s1 \<in> A}")

   163 apply(rule_tac f="\<lambda>s1. s1 @ s" in finite_imageD)

   164 apply(simp add: image_def)

   165 apply(smt Collect_cong)

   166 apply(simp add: inj_on_def)

   167 apply(rule_tac B="A ;; B" in finite_subset)

   168 apply(auto simp add: Sequ_def)[1]

   169 apply(rule assms(1))

   170 using assms(2) by auto

   171 

   172 lemma A1:

   173   assumes "finite (A ;; B)" "A \<noteq> {}"

   174   shows "finite B"

   175 apply(subgoal_tac "\<exists>s. s \<in> A")

   176 apply(erule exE)

   177 apply(subgoal_tac "finite {s @ s1 |s1. s1 \<in> B}")

   178 apply(rule_tac f="\<lambda>s1. s @ s1" in finite_imageD)

   179 apply(simp add: image_def)

   180 apply(smt Collect_cong)

   181 apply(simp add: inj_on_def)

   182 apply(rule_tac B="A ;; B" in finite_subset)

   183 apply(auto simp add: Sequ_def)[1]

   184 apply(rule assms(1))

   185 using assms(2) by auto

   186 

   187 lemma Sequ_Prod_finite:

   188   assumes "A \<noteq> {}" "B \<noteq> {}"

   189   shows "finite (A ;; B) \<longleftrightarrow> (finite (A \<times> B))"

   190 apply(rule iffI)

   191 apply(rule finite_cartesian_product)

   192 apply(erule A0)

   193 apply(rule assms(2))

   194 apply(erule A1)

   195 apply(rule assms(1))

   196 apply(simp add: Sequ_def)

   197 apply(rule finite_image_set2)

   198 apply(drule finite_cartesian_productD1)

   199 apply(rule assms(2))

   200 apply(simp)

   201 apply(drule finite_cartesian_productD2)

   202 apply(rule assms(1))

   203 apply(simp)

   204 done

   205 

   206 

   207 lemma Star_non_empty_string_infinite:

   208   assumes "s \<in> A" " s \<noteq> []"

   209   shows "infinite (A\<star>)"

   210 proof -

   211   have "inj (\<lambda>n. concat (replicate n s))" 

   212   using assms(2) concat_replicate_inj

   213     by(auto simp add: inj_on_def)

   214   moreover

   215   have "infinite (UNIV::nat set)" by simp

   216   ultimately

   217   have "infinite ((\<lambda>n. concat (replicate n s)) ` UNIV)"

   218    by (simp add: range_inj_infinite)

   219   moreover

   220   have "((\<lambda>n. concat (replicate n s)) ` UNIV) \<subseteq> (A\<star>)"

   221     using Star_concat_replicate assms(1) by auto

   222   ultimately show "infinite (A\<star>)" 

   223   using infinite_super by auto

   224 qed

   225 

   226 lemma infinitestrings_correctness:

   227   shows "infinitestrings r \<longleftrightarrow> infinite (L r)"

   228 apply(induct r)

   229 apply(simp_all)

   230 apply(simp add: zeroable_correctness)

   231 apply(rule iffI)

   232 apply(erule disjE)

   233 apply(subst Sequ_Prod_finite)

   234 apply(auto)[2]

   235 using finite_cartesian_productD2 apply blast

   236 apply(subst Sequ_Prod_finite)

   237 apply(auto)[2]

   238 using finite_cartesian_productD1 apply blast

   239 apply(subgoal_tac "L r1 \<noteq> {} \<and> L r2 \<noteq> {}")

   240 prefer 2

   241 apply(auto simp add: Sequ_def)[1]

   242 apply(subst (asm) Sequ_Prod_finite)

   243 apply(auto)[2]

   244 apply(auto)[1]

   245 apply(simp add: atmostempty_correctness)

   246 apply(rule iffI)

   247 apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD)

   248 using Star_non_empty_string_infinite apply blast

   249 done

   250 

   251 unused_thms

   252 

   253 end