thys/Exercises.thy
changeset 259 78dd6bca5627
parent 258 6670f2cb5741
child 260 160d0b08471c
equal deleted inserted replaced
258:6670f2cb5741 259:78dd6bca5627
       
     1 theory Exercises
       
     2   imports Lexer "~~/src/HOL/Library/Infinite_Set"
       
     3 begin
       
     4 
       
     5 section {* some fun tests *}
       
     6 
       
     7 fun
       
     8  zeroable :: "rexp \<Rightarrow> bool"
       
     9 where
       
    10   "zeroable (ZERO) \<longleftrightarrow> True"
       
    11 | "zeroable (ONE) \<longleftrightarrow> False"
       
    12 | "zeroable (CHAR 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 apply(induct r rule: zeroable.induct)
       
    20 apply(auto simp add: Sequ_def)
       
    21 done
       
    22 
       
    23 fun
       
    24  atmostempty :: "rexp \<Rightarrow> bool"
       
    25 where
       
    26   "atmostempty (ZERO) \<longleftrightarrow> True"
       
    27 | "atmostempty (ONE) \<longleftrightarrow> True"
       
    28 | "atmostempty (CHAR c) \<longleftrightarrow> False"
       
    29 | "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2"
       
    30 | "atmostempty (SEQ r1 r2) \<longleftrightarrow> 
       
    31      zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"
       
    32 | "atmostempty (STAR r) = atmostempty r"
       
    33 
       
    34 fun
       
    35  somechars :: "rexp \<Rightarrow> bool"
       
    36 where
       
    37   "somechars (ZERO) \<longleftrightarrow> False"
       
    38 | "somechars (ONE) \<longleftrightarrow> False"
       
    39 | "somechars (CHAR c) \<longleftrightarrow> True"
       
    40 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2"
       
    41 | "somechars (SEQ r1 r2) \<longleftrightarrow> 
       
    42       (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> 
       
    43       (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)"
       
    44 | "somechars (STAR r) \<longleftrightarrow> somechars r"
       
    45 
       
    46 lemma somechars_correctness:
       
    47   shows "somechars r \<longleftrightarrow> (\<exists>s. s \<noteq> [] \<and> s \<in> L r)"
       
    48 apply(induct r rule: somechars.induct)
       
    49 apply(simp)
       
    50 apply(simp)
       
    51 apply(simp)
       
    52 apply(auto)[1]
       
    53 prefer 2
       
    54 apply(simp)
       
    55 apply(rule iffI)
       
    56 apply(auto)[1]
       
    57 apply (metis Star_decomp neq_Nil_conv)
       
    58 apply(rule iffI)
       
    59 apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
       
    60 apply(auto)[1]
       
    61 apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
       
    62 apply(auto)[1]
       
    63 done
       
    64 
       
    65 lemma atmostempty_correctness_aux:
       
    66   shows "atmostempty r \<longleftrightarrow> \<not> somechars r"
       
    67 apply(induct r)
       
    68 apply(simp_all)
       
    69 apply(auto simp add: zeroable_correctness nullable_correctness somechars_correctness)
       
    70 done
       
    71 
       
    72 lemma atmostempty_correctness:
       
    73   shows "atmostempty r \<longleftrightarrow> L r \<subseteq> {[]}"
       
    74 by(auto simp add: atmostempty_correctness_aux somechars_correctness)
       
    75 
       
    76 fun
       
    77  infinitestrings :: "rexp \<Rightarrow> bool"
       
    78 where
       
    79   "infinitestrings (ZERO) = False"
       
    80 | "infinitestrings (ONE) = False"
       
    81 | "infinitestrings (CHAR c) = False"
       
    82 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"
       
    83 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> 
       
    84       (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"
       
    85 | "infinitestrings (STAR r) = (\<not> atmostempty r)"
       
    86 
       
    87 lemma Star_atmostempty:
       
    88   assumes "A \<subseteq> {[]}"
       
    89   shows "A\<star> \<subseteq> {[]}"
       
    90 using assms
       
    91 using Star_string concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce
       
    92 
       
    93 lemma Star_empty_string_finite:
       
    94   shows "finite ({[]}\<star>)"
       
    95 using Star_atmostempty infinite_super by auto
       
    96 
       
    97 lemma Star_empty_finite:
       
    98   shows "finite ({}\<star>)"
       
    99 using Star_atmostempty infinite_super by auto
       
   100 
       
   101 lemma Star_concat_replicate:
       
   102   assumes "s \<in> A"
       
   103   shows "concat (replicate n s) \<in> A\<star>"
       
   104 using assms
       
   105 by (induct n) (auto)
       
   106 
       
   107 
       
   108 lemma concat_replicate_inj:
       
   109   assumes "concat (replicate n s) = concat (replicate m s)" "s \<noteq> []"
       
   110   shows "n = m"
       
   111 using assms
       
   112 apply(induct n arbitrary: m)
       
   113 apply(auto)[1]
       
   114 apply(auto)
       
   115 apply(case_tac m)
       
   116 apply(clarify)
       
   117 apply(simp only: replicate.simps concat.simps)
       
   118 apply blast
       
   119 by simp
       
   120 
       
   121 lemma A0:
       
   122   assumes "finite (A ;; B)" "B \<noteq> {}"
       
   123   shows "finite A"
       
   124 apply(subgoal_tac "\<exists>s. s \<in> B")
       
   125 apply(erule exE)
       
   126 apply(subgoal_tac "finite {s1 @ s |s1. s1 \<in> A}")
       
   127 apply(rule_tac f="\<lambda>s1. s1 @ s" in finite_imageD)
       
   128 apply(simp add: image_def)
       
   129 apply(smt Collect_cong)
       
   130 apply(simp add: inj_on_def)
       
   131 apply(rule_tac B="A ;; B" in finite_subset)
       
   132 apply(auto simp add: Sequ_def)[1]
       
   133 apply(rule assms(1))
       
   134 using assms(2) by auto
       
   135 
       
   136 lemma A1:
       
   137   assumes "finite (A ;; B)" "A \<noteq> {}"
       
   138   shows "finite B"
       
   139 apply(subgoal_tac "\<exists>s. s \<in> A")
       
   140 apply(erule exE)
       
   141 apply(subgoal_tac "finite {s @ s1 |s1. s1 \<in> B}")
       
   142 apply(rule_tac f="\<lambda>s1. s @ s1" in finite_imageD)
       
   143 apply(simp add: image_def)
       
   144 apply(smt Collect_cong)
       
   145 apply(simp add: inj_on_def)
       
   146 apply(rule_tac B="A ;; B" in finite_subset)
       
   147 apply(auto simp add: Sequ_def)[1]
       
   148 apply(rule assms(1))
       
   149 using assms(2) by auto
       
   150 
       
   151 lemma Sequ_Prod_finite:
       
   152   assumes "A \<noteq> {}" "B \<noteq> {}"
       
   153   shows "finite (A ;; B) \<longleftrightarrow> (finite (A \<times> B))"
       
   154 apply(rule iffI)
       
   155 apply(rule finite_cartesian_product)
       
   156 apply(erule A0)
       
   157 apply(rule assms(2))
       
   158 apply(erule A1)
       
   159 apply(rule assms(1))
       
   160 apply(simp add: Sequ_def)
       
   161 apply(rule finite_image_set2)
       
   162 apply(drule finite_cartesian_productD1)
       
   163 apply(rule assms(2))
       
   164 apply(simp)
       
   165 apply(drule finite_cartesian_productD2)
       
   166 apply(rule assms(1))
       
   167 apply(simp)
       
   168 done
       
   169 
       
   170 
       
   171 lemma Star_non_empty_string_infinite:
       
   172   assumes "s \<in> A" " s \<noteq> []"
       
   173   shows "infinite (A\<star>)"
       
   174 proof -
       
   175   have "inj (\<lambda>n. concat (replicate n s))" 
       
   176   using assms(2) concat_replicate_inj
       
   177     by(auto simp add: inj_on_def)
       
   178   moreover
       
   179   have "infinite (UNIV::nat set)" by simp
       
   180   ultimately
       
   181   have "infinite ((\<lambda>n. concat (replicate n s)) ` UNIV)"
       
   182    by (simp add: range_inj_infinite)
       
   183   moreover
       
   184   have "((\<lambda>n. concat (replicate n s)) ` UNIV) \<subseteq> (A\<star>)"
       
   185     using Star_concat_replicate assms(1) by auto
       
   186   ultimately show "infinite (A\<star>)" 
       
   187   using infinite_super by auto
       
   188 qed
       
   189 
       
   190 lemma infinitestrings_correctness:
       
   191   shows "infinitestrings r \<longleftrightarrow> infinite (L r)"
       
   192 apply(induct r)
       
   193 apply(simp_all)
       
   194 apply(simp add: zeroable_correctness)
       
   195 apply(rule iffI)
       
   196 apply(erule disjE)
       
   197 apply(subst Sequ_Prod_finite)
       
   198 apply(auto)[2]
       
   199 using finite_cartesian_productD2 apply blast
       
   200 apply(subst Sequ_Prod_finite)
       
   201 apply(auto)[2]
       
   202 using finite_cartesian_productD1 apply blast
       
   203 apply(subgoal_tac "L r1 \<noteq> {} \<and> L r2 \<noteq> {}")
       
   204 prefer 2
       
   205 apply(auto simp add: Sequ_def)[1]
       
   206 apply(subst (asm) Sequ_Prod_finite)
       
   207 apply(auto)[2]
       
   208 apply(auto)[1]
       
   209 apply(simp add: atmostempty_correctness)
       
   210 apply(rule iffI)
       
   211 apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD)
       
   212 using Star_non_empty_string_infinite apply blast
       
   213 done
       
   214 
       
   215 
       
   216 end