# HG changeset patch
# User urbanc
# Date 1314703878 0
# Node ID 91e3e906034caefb2dc48c2c1527c3e85cd71f40
# Parent  296930182fe1275160af0e6564a231da4851d70b
added a further test

diff -r 296930182fe1 -r 91e3e906034c Closures2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Closures2.thy	Tue Aug 30 11:31:18 2011 +0000
@@ -0,0 +1,310 @@
+theory Closure2
+imports Closures
+begin
+
+inductive emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
+where
+   emb0 [Pure.intro]: "emb [] bs"
+ | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
+ | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
+
+lemma emb_refl:
+  shows "x \<preceq> x"
+apply(induct x)
+apply(auto intro: emb.intros)
+done
+
+lemma emb_right:
+  assumes a: "x \<preceq> y"
+  shows "x \<preceq> y @ y'"
+using a
+apply(induct arbitrary: y')
+apply(auto intro: emb.intros)
+done
+
+lemma emb_left:
+  assumes a: "x \<preceq> y"
+  shows "x \<preceq> y' @ y"
+using a
+apply(induct y')
+apply(auto intro: emb.intros)
+done
+
+lemma emb_appendI:
+  assumes a: "x \<preceq> x'"
+  and     b: "y \<preceq> y'"
+  shows "x @ y \<preceq> x' @ y'"
+using a b
+apply(induct)
+apply(auto intro: emb.intros emb_left)
+done
+
+lemma emb_append:
+  assumes a: "x \<preceq> y1 @ y2"
+  shows "\<exists>x1 x2. x = x1 @ x2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2"
+using a
+apply(induct x y\<equiv>"y1 @ y2" arbitrary: y1 y2)
+apply(auto intro: emb0)[1]
+apply(simp add: Cons_eq_append_conv)
+apply(auto)[1]
+apply(rule_tac x="[]" in exI)
+apply(rule_tac x="as" in exI)
+apply(auto intro: emb.intros)[1]
+apply(simp add: append_eq_append_conv2)
+apply(drule_tac x="ys'" in meta_spec)
+apply(drule_tac x="y2" in meta_spec)
+apply(auto)[1]
+apply(rule_tac x="x1" in exI)
+apply(rule_tac x="x2" in exI)
+apply(auto intro: emb.intros)[1]
+apply(subst (asm) Cons_eq_append_conv)
+apply(auto)[1]
+apply(rule_tac x="[]" in exI)
+apply(rule_tac x="a # as" in exI)
+apply(auto intro: emb.intros)[1]
+apply(simp add: append_eq_append_conv2)
+apply(drule_tac x="ys'" in meta_spec)
+apply(drule_tac x="y2" in meta_spec)
+apply(auto)[1]
+apply(rule_tac x="a # x1" in exI)
+apply(rule_tac x="x2" in exI)
+apply(auto intro: emb.intros)[1]
+done
+
+
+definition
+ "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}"
+
+definition
+ "SUPSEQ A \<equiv> (- SUBSEQ A) \<union> A"
+
+lemma [simp]:
+  "SUBSEQ {} = {}"
+unfolding SUBSEQ_def
+by auto
+
+lemma [simp]:
+  "SUBSEQ {[]} = {[]}"
+unfolding SUBSEQ_def
+apply(auto)
+apply(erule emb.cases)
+apply(auto)[3]
+apply(rule emb0)
+done
+
+lemma SUBSEQ_atom [simp]:
+  "SUBSEQ {[a]} = {[], [a]}"
+apply(auto simp add: SUBSEQ_def)
+apply(erule emb.cases)
+apply(auto)[3]
+apply(erule emb.cases)
+apply(auto)[3]
+apply(erule emb.cases)
+apply(auto)[3]
+apply(rule emb0)
+apply(rule emb2)
+apply(rule emb0)
+done
+
+lemma SUBSEQ_union [simp]:
+  "SUBSEQ (A \<union> B) = SUBSEQ A \<union> SUBSEQ B"
+unfolding SUBSEQ_def by auto
+
+lemma SUBSEQ_Union [simp]:
+  fixes A :: "nat \<Rightarrow> 'a lang"
+  shows "SUBSEQ (\<Union>n. (A n)) = (\<Union>n. (SUBSEQ  (A n)))"
+unfolding SUBSEQ_def image_def by auto
+
+lemma SUBSEQ_conc1:
+  "\<lbrakk>x \<in> SUBSEQ A; y \<in> SUBSEQ B\<rbrakk> \<Longrightarrow> x @ y \<in> SUBSEQ (A \<cdot> B)"
+unfolding SUBSEQ_def 
+apply(auto)
+apply(rule_tac x="xa @ xaa" in bexI)
+apply(rule emb_appendI)
+apply(simp_all)
+done
+
+lemma SUBSEQ_conc2:
+  "x \<in> SUBSEQ (A \<cdot> B) \<Longrightarrow> x \<in> (SUBSEQ A) \<cdot> (SUBSEQ B)"
+unfolding SUBSEQ_def conc_def 
+apply(auto)
+apply(drule emb_append)
+apply(auto)
+done
+
+lemma SUBSEQ_conc [simp]:
+  "SUBSEQ (A \<cdot> B) = SUBSEQ A \<cdot> SUBSEQ B"
+apply(auto)
+apply(simp add: SUBSEQ_conc2)
+apply(subst (asm) conc_def)
+apply(auto simp add: SUBSEQ_conc1)
+done
+
+lemma SUBSEQ_star1:
+  assumes a: "x \<in> (SUBSEQ A)\<star>" 
+  shows "x \<in> SUBSEQ (A\<star>)"
+using a
+apply(induct rule: star_induct)
+apply(simp add: SUBSEQ_def)
+apply(rule_tac x="[]" in bexI)
+apply(rule emb0)
+apply(auto)[1]
+apply(drule SUBSEQ_conc1)
+apply(assumption)
+apply(subst star_unfold_left)
+apply(simp only: SUBSEQ_union)
+apply(simp)
+done
+
+lemma SUBSEQ_star2_aux:
+  assumes a: "x \<in> SUBSEQ (A ^^ n)" 
+  shows "x \<in> (SUBSEQ A)\<star>"
+using a
+apply(induct n arbitrary: x)
+apply(simp)
+apply(simp)
+apply(simp add: conc_def)
+apply(auto)
+done
+
+lemma SUBSEQ_star2:
+  assumes a: "x \<in> SUBSEQ (A\<star>)" 
+  shows "x \<in> (SUBSEQ A)\<star>"
+using a
+apply(subst (asm) star_def)
+apply(auto simp add: SUBSEQ_star2_aux)
+done
+
+lemma SUBSEQ_star [simp]:
+  shows "SUBSEQ (A\<star>) = (SUBSEQ A)\<star>"
+using SUBSEQ_star1 SUBSEQ_star2 by auto
+
+lemma SUBSEQ_fold:
+  shows "SUBSEQ A \<union> A = SUBSEQ A"
+apply(auto simp add: SUBSEQ_def)
+apply(rule_tac x="x" in bexI)
+apply(auto simp add: emb_refl)
+done
+
+
+lemma SUPSEQ_union [simp]:
+  "SUPSEQ (A \<union> B) = (SUPSEQ A \<union> B) \<inter> (SUPSEQ B \<union> A)"
+unfolding SUPSEQ_def 
+by auto
+
+
+definition
+  Notreg :: "'a::finite rexp \<Rightarrow> 'a rexp"
+where
+  "Notreg r \<equiv> SOME r'. lang r' = - (lang r)"
+
+lemma [simp]:
+  "lang (Notreg r) = - lang r"
+apply(simp add: Notreg_def)
+apply(rule someI2_ex)
+apply(auto)
+apply(subgoal_tac "regular (lang r)")
+apply(drule closure_complement)
+apply(auto) 
+done
+
+definition
+  Interreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+where
+  "Interreg r1 r2 = Notreg (Plus (Notreg r1) (Notreg r2))"
+
+lemma [simp]:
+  "lang (Interreg r1 r2) = (lang r1) \<inter> (lang r2)"
+by (simp add: Interreg_def)
+
+definition
+  Diffreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+where
+  "Diffreg r1 r2 = Notreg (Plus (Notreg r1) r2)"
+
+lemma [simp]:
+  "lang (Diffreg r1 r2) = (lang r1) - (lang r2)"
+by (auto simp add: Diffreg_def)
+
+definition
+  Allreg :: "'a::finite rexp"
+where
+  "Allreg \<equiv> \<Uplus>(Atom ` UNIV)"
+
+lemma Allreg_lang [simp]:
+  "lang Allreg = (\<Union>a. {[a]})"
+unfolding Allreg_def
+by auto
+
+lemma [simp]:
+  "(\<Union>a. {[a]})\<star> = UNIV"
+apply(auto)
+apply(induct_tac x rule: list.induct)
+apply(auto)
+apply(subgoal_tac "[a] @ list \<in> (\<Union>a. {[a]})\<star>")
+apply(simp)
+apply(rule append_in_starI)
+apply(auto)
+done
+
+lemma Star_Allreg_lang [simp]:
+  "lang (Star Allreg) = UNIV"
+by (simp)
+
+fun UP :: "'a::finite rexp \<Rightarrow> 'a rexp"
+where
+  "UP (Zero) = Star Allreg"
+| "UP (One) = Star Allreg"
+| "UP (Atom c) = Times Allreg (Star Allreg)"   
+| "UP (Plus r1 r2) = Interreg (Plus (UP r1) (r2)) (Plus (UP r2) r1)"
+| "UP (Times r1 r2) = 
+     Plus (Notreg (Times (Plus (Notreg (UP r1)) r1) (Plus (Notreg (UP r2)) r2))) (Times r1 r2)"
+| "UP (Star r) = Plus (Notreg (Star (Plus (Notreg (UP r)) r))) (Star r)"
+
+lemma UP:
+  "lang (UP r) = SUPSEQ (lang r)"
+apply(induct r)
+apply(simp add: SUPSEQ_def)
+apply(simp add: SUPSEQ_def)
+apply(simp add: Compl_eq_Diff_UNIV)
+apply(auto)[1]
+apply(simp add: SUPSEQ_def)
+apply(simp add: Compl_eq_Diff_UNIV)
+apply(rule sym)
+apply(rule_tac s="UNIV - {[]}" in trans)
+apply(auto)[1]
+apply(auto simp add: conc_def)[1]
+apply(case_tac x)
+apply(simp)
+apply(simp)
+apply(rule_tac x="[a]" in exI)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp add: SUPSEQ_def)
+apply(simp add: Un_Int_distrib2)
+apply(simp add: Compl_partition2)
+apply(simp add: SUBSEQ_fold)
+apply(simp add: Un_Diff)
+apply(simp add: SUPSEQ_def)
+apply(simp add: Un_Int_distrib2)
+apply(simp add: Compl_partition2)
+apply(simp add: SUBSEQ_fold)
+done
+
+lemma SUPSEQ_reg:
+  fixes A :: "'a::finite lang"
+  assumes "regular A"
+  shows "regular (SUPSEQ A)"
+proof -
+  from assms obtain r::"'a::finite rexp" where eq: "lang r = A" by auto
+  moreover 
+  have "lang (UP r) = SUPSEQ (lang r)" by (rule UP)
+  ultimately show "regular (SUPSEQ A)" by auto
+qed
+   
+
+ 
+
+
+end