theory "RegSet"
  imports "Main" 
begin


text {* Sequential composition of sets *}

definition
  lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
where 
  "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"


section {* Kleene star for sets *}

inductive_set
  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
  for L :: "string set"
where
  start[intro]: "[] \<in> L\<star>"
| step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"


text {* A standard property of star *}

lemma lang_star_cases:
  shows "L\<star> =  {[]} \<union> L ; L\<star>"
proof
  { fix x
    have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"
      unfolding lang_seq_def
    by (induct rule: Star.induct) (auto)
  }
  then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto
next
  show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>" 
    unfolding lang_seq_def by auto
qed


lemma lang_star_cases2:
  shows "[] \<notin> L \<Longrightarrow> L\<star> - {[]} =  L ; L\<star>"
by (subst lang_star_cases)
   (simp add: lang_seq_def)


section {* Regular Expressions *}

datatype rexp =
  NULL
| EMPTY
| CHAR char
| SEQ rexp rexp
| ALT rexp rexp
| STAR rexp


section {* Semantics of Regular Expressions *}

fun
  L :: "rexp \<Rightarrow> string set"
where
  "L (NULL) = {}"
| "L (EMPTY) = {[]}"
| "L (CHAR c) = {[c]}"
| "L (SEQ r1 r2) = (L r1) ; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
| "L (STAR r) = (L r)\<star>"

abbreviation
  CUNIV :: "string set"
where
  "CUNIV \<equiv> (\<lambda>x. [x]) ` (UNIV::char set)"

lemma CUNIV_star_minus:
  "(CUNIV\<star> - {[c]}) = {[]} \<union> (CUNIV - {[c]}; (CUNIV\<star>))"
apply(subst lang_star_cases)
apply(simp add: lang_seq_def)
oops


lemma string_in_CUNIV:
  shows "s \<in> CUNIV\<star>"
proof (induct s)
  case Nil
  show "[] \<in> CUNIV\<star>" by (rule start)
next
  case (Cons c s)
  have "[c] \<in> CUNIV" by simp
  moreover
  have "s \<in> CUNIV\<star>" by fact
  ultimately have "[c] @ s \<in> CUNIV\<star>" by (rule step)
  then show "c # s \<in> CUNIV\<star>" by simp
qed

lemma UNIV_CUNIV_star: 
  shows "UNIV = CUNIV\<star>"
using string_in_CUNIV
by (auto)

abbreviation 
  reg :: "string set => bool"
where
  "reg L1 \<equiv> (\<exists>r. L r = L1)"

lemma reg_null [intro]:
  shows "reg {}"
by (metis L.simps(1))

lemma reg_empty [intro]:
  shows "reg {[]}"
by (metis L.simps(2))

lemma reg_star [intro]:
  shows "reg L1 \<Longrightarrow> reg (L1\<star>)"
by (metis L.simps(6))

lemma reg_seq [intro]:
  assumes a: "reg L1" "reg L2"
  shows "reg (L1 ; L2)"
using a
by (metis L.simps(4)) 

lemma reg_union [intro]:
  assumes a: "reg L1" "reg L2"
  shows "reg (L1 \<union> L2)"
using a
by (metis L.simps(5)) 

lemma reg_string [intro]:
  fixes s::string
  shows "reg {s}"
proof (induct s)
  case Nil
  show "reg {[]}" by (rule reg_empty)
next
  case (Cons c s)
  have "reg {s}" by fact
  then obtain r where "L r = {s}" by auto
  then have "L (SEQ (CHAR c) r) = {[c]} ; {s}" by simp
  also have "\<dots> = {c # s}" by (simp add: lang_seq_def)
  finally show "reg {c # s}" by blast 
qed

lemma reg_finite [intro]:
  assumes a: "finite L1"
  shows "reg L1"
using a
proof(induct)
  case empty
  show "reg {}" by (rule reg_null)
next
  case (insert s S)
  have "reg {s}" by (rule reg_string)
  moreover 
  have "reg S" by fact
  ultimately have "reg ({s} \<union> S)" by (rule reg_union)
  then show "reg (insert s S)" by simp
qed
  
lemma reg_cuniv [intro]:
  shows "reg (CUNIV)"
by (rule reg_finite) (auto)

lemma reg_univ:
  shows "reg (UNIV::string set)"
proof -
  have "reg CUNIV" by (rule reg_cuniv)
  then have "reg (CUNIV\<star>)" by (rule reg_star)
  then show "reg UNIV" by (simp add: UNIV_CUNIV_star)
qed

lemma reg_finite_subset:
  assumes a: "finite L1"
  and     b: "reg L1" "L2 \<subseteq> L1"
  shows "reg L2"
using a b
apply(induct arbitrary: L2)
apply(simp add: reg_empty)
oops


lemma reg_not:
  shows "reg (UNIV - L r)"
proof (induct r)
  case NULL
  have "reg UNIV" by (rule reg_univ)
  then show "reg (UNIV - L NULL)" by simp
next
  case EMPTY
  have "[] \<notin> CUNIV" by auto
  moreover
  have "reg (CUNIV; CUNIV\<star>)" by auto
  ultimately have "reg (CUNIV\<star> - {[]})" 
    using lang_star_cases2 by simp
  then show "reg (UNIV - L EMPTY)" by (simp add: UNIV_CUNIV_star)
next
  case (CHAR c)
  then show "?case"
    apply(simp)
   
using reg_UNIV
apply(simp)
apply(simp add: char_star2[symmetric])
apply(rule reg_seq)
apply(rule reg_cuniv)
apply(rule reg_star)
apply(rule reg_cuniv)
oops



end