theory Fun

  imports Lexer "~~/src/HOL/Library/Infinite_Set"

begin

section {* some fun tests *}

fun

 zeroable :: "rexp ⇒ bool"

where

  "zeroable (ZERO) = True"

| "zeroable (ONE) = False"

| "zeroable (CHAR c) = False"

| "zeroable (ALT r1 r2) = (zeroable r1 ∧ zeroable r2)"

| "zeroable (SEQ r1 r2) = (zeroable r1 ∨ zeroable r2)"

| "zeroable (STAR r) = False"

lemma zeroable_correctness:

  shows "zeroable r ⟷ L r = {}"

apply(induct r rule: zeroable.induct)

apply(auto simp add: Sequ_def)

done

fun

 atmostempty :: "rexp ⇒ bool"

where

  "atmostempty (ZERO) = True"

| "atmostempty (ONE) = True"

| "atmostempty (CHAR c) = False"

| "atmostempty (ALT r1 r2) = (atmostempty r1 ∧ atmostempty r2)"

| "atmostempty (SEQ r1 r2) = ((zeroable r1) ∨ (zeroable r2) ∨ (atmostempty r1 ∧ atmostempty r2))"

| "atmostempty (STAR r) = atmostempty r"

fun

 somechars :: "rexp ⇒ bool"

where

  "somechars (ZERO) = False"

| "somechars (ONE) = False"

| "somechars (CHAR c) = True"

| "somechars (ALT r1 r2) = (somechars r1 ∨ somechars r2)"

| "somechars (SEQ r1 r2) = ((¬zeroable r1 ∧ somechars r2) ∨ (¬zeroable r2 ∧ somechars r1) ∨ 

                           (somechars r1 ∧ nullable r2) ∨ (somechars r2 ∧ nullable r1))"

| "somechars (STAR r) = somechars r"

lemma somechars_correctness:

  shows "somechars r ⟷ (∃s. s ≠ [] ∧ s ∈ L r)"

apply(induct r rule: somechars.induct)

apply(simp)

apply(simp)

apply(simp)

apply(auto)[1]

prefer 2

apply(simp)

apply(rule iffI)

apply(auto)[1]

apply (metis Star_decomp neq_Nil_conv)

apply(rule iffI)

apply(simp add: Sequ_def zeroable_correctness nullable_correctness)

apply(auto)[1]

apply(simp add: Sequ_def zeroable_correctness nullable_correctness)

apply(auto)[1]

done

lemma atmostempty_correctness_aux:

  shows "atmostempty r ⟷ ¬somechars r"

apply(induct r)

apply(simp_all)

apply(auto simp add: zeroable_correctness nullable_correctness somechars_correctness)

done

lemma atmostempty_correctness:

  shows "atmostempty r ⟷ L r ⊆ {[]}"

by(auto simp add: atmostempty_correctness_aux somechars_correctness)

fun

 infinitestrings :: "rexp ⇒ bool"

where

  "infinitestrings (ZERO) = False"

| "infinitestrings (ONE) = False"

| "infinitestrings (CHAR c) = False"

| "infinitestrings (ALT r1 r2) = (infinitestrings r1 ∨ infinitestrings r2)"

| "infinitestrings (SEQ r1 r2) = ((¬zeroable r1 ∧ infinitestrings r2) ∨ (¬zeroable r2 ∧ infinitestrings r1))"

| "infinitestrings (STAR r) = (¬atmostempty r)"

lemma Star_atmostempty:

  assumes "A ⊆ {[]}"

  shows "A⋆ ⊆ {[]}"

using assms

using Star_string concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce

lemma Star_empty_string_finite:

  shows "finite ({[]}⋆)"

using Star_atmostempty infinite_super by auto

lemma Star_empty_finite:

  shows "finite ({}⋆)"

using Star_atmostempty infinite_super by auto

lemma Star_concat_replicate:

  assumes "s ∈ A"

  shows "concat (replicate n s) ∈ A⋆"

using assms

by (induct n) (auto)

lemma concat_replicate_inj:

  assumes "concat (replicate n s) = concat (replicate m s)" "s ≠ []"

  shows "n = m"

using assms

apply(induct n arbitrary: m)

apply(auto)[1]

apply(auto)

apply(case_tac m)

apply(clarify)

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

apply blast

by simp

lemma A0:

  assumes "finite (A ;; B)" "B ≠ {}"

  shows "finite A"

apply(subgoal_tac "∃s. s ∈ B")

apply(erule exE)

apply(subgoal_tac "finite {s1 @ s |s1. s1 ∈ A}")

apply(rule_tac f="λs1. s1 @ s" in finite_imageD)

apply(simp add: image_def)

apply(smt Collect_cong)

apply(simp add: inj_on_def)

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

apply(auto simp add: Sequ_def)[1]

apply(rule assms(1))

using assms(2) by auto

lemma A1:

  assumes "finite (A ;; B)" "A ≠ {}"

  shows "finite B"

apply(subgoal_tac "∃s. s ∈ A")

apply(erule exE)

apply(subgoal_tac "finite {s @ s1 |s1. s1 ∈ B}")

apply(rule_tac f="λs1. s @ s1" in finite_imageD)

apply(simp add: image_def)

apply(smt Collect_cong)

apply(simp add: inj_on_def)

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

apply(auto simp add: Sequ_def)[1]

apply(rule assms(1))

using assms(2) by auto

lemma Sequ_Prod_finite:

  assumes "A ≠ {}" "B ≠ {}"

  shows "finite (A ;; B) ⟷ (finite (A × B))"

apply(rule iffI)

apply(rule finite_cartesian_product)

apply(erule A0)

apply(rule assms(2))

apply(erule A1)

apply(rule assms(1))

apply(simp add: Sequ_def)

apply(rule finite_image_set2)

apply(drule finite_cartesian_productD1)

apply(rule assms(2))

apply(simp)

apply(drule finite_cartesian_productD2)

apply(rule assms(1))

apply(simp)

done

lemma Star_non_empty_string_infinite:

  assumes "s ∈ A" " s ≠ []"

  shows "infinite (A⋆)"

proof -

  have "inj (λn. concat (replicate n s))" 

  using assms(2) concat_replicate_inj

    by(auto simp add: inj_on_def)

  moreover

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

  ultimately

  have "infinite ((λn. concat (replicate n s)) ` UNIV)"

   by (simp add: range_inj_infinite)

  moreover

  have "((λn. concat (replicate n s)) ` UNIV) ⊆ (A⋆)"

    using Star_concat_replicate assms(1) by auto

  ultimately show "infinite (A⋆)" 

  using infinite_super by auto

qed

lemma infinitestrings_correctness:

  shows "infinitestrings r ⟷ infinite (L r)"

apply(induct r)

apply(simp_all)

apply(simp add: zeroable_correctness)

apply(rule iffI)

apply(erule disjE)

apply(subst Sequ_Prod_finite)

apply(auto)[2]

using finite_cartesian_productD2 apply blast

apply(subst Sequ_Prod_finite)

apply(auto)[2]

using finite_cartesian_productD1 apply blast

apply(subgoal_tac "L r1 ≠ {} ∧ L r2 ≠ {}")

prefer 2

apply(auto simp add: Sequ_def)[1]

apply(subst (asm) Sequ_Prod_finite)

apply(auto)[2]

apply(auto)[1]

apply(simp add: atmostempty_correctness)

apply(rule iffI)

apply (metis Star_empty_finite Star_empty_string_finite subset_singletonD)

using Star_non_empty_string_infinite apply blast

done

end