--- a/Myhill_1.thy Mon Jan 31 14:51:47 2011 +0000
+++ b/Myhill_1.thy Wed Feb 02 06:05:12 2011 +0000
@@ -36,18 +36,12 @@
where
"A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
-text {*
- Transitive closure of language @{text "L"}.
-*}
+text {* Some properties of operator @{text ";;"}. *}
-inductive_set
- Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
- for L
-where
- start[intro]: "[] \<in> L\<star>"
-| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>"
-
-text {* Some properties of operator @{text ";;"}. *}
+lemma seq_add_left:
+ assumes a: "A = B"
+ shows "C ;; A = C ;; B"
+using a by simp
lemma seq_union_distrib_right:
shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
@@ -73,21 +67,73 @@
and "{[]} ;; A = A"
by (simp_all add: Seq_def)
+fun
+ pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
+where
+ "A \<up> 0 = {[]}"
+| "A \<up> (Suc n) = A ;; (A \<up> n)"
-lemma star_intro1[rule_format]:
- "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>"
-by (erule Star.induct, auto)
+definition
+ Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
+where
+ "A\<star> \<equiv> (\<Union>n. A \<up> n)"
+
+lemma star_start[intro]:
+ shows "[] \<in> A\<star>"
+proof -
+ have "[] \<in> A \<up> 0" by auto
+ then show "[] \<in> A\<star>" unfolding Star_def by blast
+qed
+
+lemma star_step [intro]:
+ assumes a: "s1 \<in> A"
+ and b: "s2 \<in> A\<star>"
+ shows "s1 @ s2 \<in> A\<star>"
+proof -
+ from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto
+ then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)
+ then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast
+qed
-lemma star_intro2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>"
-by (drule step[of y lang "[]"], auto simp:start)
+lemma star_induct[consumes 1, case_names start step]:
+ assumes a: "x \<in> A\<star>"
+ and b: "P []"
+ and c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"
+ shows "P x"
+proof -
+ from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto
+ then show "P x"
+ by (induct n arbitrary: x)
+ (auto intro!: b c simp add: Seq_def Star_def)
+qed
+
+lemma star_intro1:
+ assumes a: "x \<in> A\<star>"
+ and b: "y \<in> A\<star>"
+ shows "x @ y \<in> A\<star>"
+using a b
+by (induct rule: star_induct) (auto)
-lemma star_intro3[rule_format]:
- "x \<in> lang\<star> \<Longrightarrow> \<forall>y . y \<in> lang \<longrightarrow> x @ y \<in> lang\<star>"
-by (erule Star.induct, auto intro:star_intro2)
+lemma star_intro2:
+ assumes a: "y \<in> A"
+ shows "y \<in> A\<star>"
+proof -
+ from a have "y @ [] \<in> A\<star>" by blast
+ then show "y \<in> A\<star>" by simp
+qed
+
+lemma star_intro3:
+ assumes a: "x \<in> A\<star>"
+ and b: "y \<in> A"
+ shows "x @ y \<in> A\<star>"
+using a b by (blast intro: star_intro1 star_intro2)
lemma star_decom:
- "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> lang \<and> b \<in> lang\<star>)"
-by (induct x rule: Star.induct, simp, blast)
+ "\<lbrakk>x \<in> A\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>)"
+apply(induct rule: star_induct)
+apply(simp)
+apply(blast)
+done
lemma lang_star_cases:
shows "L\<star> = {[]} \<union> L ;; L\<star>"
@@ -95,50 +141,14 @@
{ fix x
have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ;; L\<star>"
unfolding Seq_def
- by (induct rule: Star.induct) (auto)
+ 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>"
+ show "{[]} \<union> L ;; L\<star> \<subseteq> L\<star>"
unfolding Seq_def by auto
qed
-fun
- pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
-where
- "A \<up> 0 = {[]}"
-| "A \<up> (Suc n) = A ;; (A \<up> n)"
-
-lemma star_pow_eq:
- shows "A\<star> = (\<Union>n. A \<up> n)"
-proof -
- { fix n x
- assume "x \<in> (A \<up> n)"
- then have "x \<in> A\<star>"
- by (induct n arbitrary: x) (auto simp add: Seq_def)
- }
- moreover
- { fix x
- assume "x \<in> A\<star>"
- then have "\<exists>n. x \<in> A \<up> n"
- proof (induct rule: Star.induct)
- case start
- have "[] \<in> A \<up> 0" by auto
- then show "\<exists>n. [] \<in> A \<up> n" by blast
- next
- case (step s1 s2)
- have "s1 \<in> A" by fact
- moreover
- have "\<exists>n. s2 \<in> A \<up> n" by fact
- then obtain n where "s2 \<in> A \<up> n" by blast
- ultimately
- have "s1 @ s2 \<in> A \<up> (Suc n)" by (auto simp add: Seq_def)
- then show "\<exists>n. s1 @ s2 \<in> A \<up> n" by blast
- qed
- }
- ultimately show "A\<star> = (\<Union>n. A \<up> n)" by auto
-qed
-
lemma
shows seq_Union_left: "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"
and seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"
@@ -150,7 +160,7 @@
lemma seq_star_comm:
shows "A ;; A\<star> = A\<star> ;; A"
-unfolding star_pow_eq
+unfolding Star_def
unfolding seq_Union_left
unfolding seq_pow_comm
unfolding seq_Union_right
@@ -226,8 +236,8 @@
have "A\<star> = {[]} \<union> A\<star> ;; A"
unfolding seq_star_comm[symmetric]
by (rule lang_star_cases)
- then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
- unfolding Seq_def by simp
+ then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
+ by (rule seq_add_left)
also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"
unfolding seq_union_distrib_left by simp
also have "\<dots> = B \<union> (B ;; A\<star>) ;; A"
@@ -238,8 +248,9 @@
assume eq: "X = X ;; A \<union> B"
{ fix n::nat
have "B ;; (A \<up> n) \<subseteq> X" using ardens_helper[OF eq, of "n"] by auto }
- then have "B ;; A\<star> \<subseteq> X" unfolding star_pow_eq Seq_def
- by (auto simp add: UNION_def)
+ then have "B ;; A\<star> \<subseteq> X"
+ unfolding Seq_def Star_def UNION_def
+ by auto
moreover
{ fix s::string
obtain k where "k = length s" by auto
@@ -252,7 +263,8 @@
moreover
have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto
ultimately
- have "s \<in> B ;; A\<star>" unfolding star_pow_eq seq_Union_left
+ have "s \<in> B ;; A\<star>"
+ unfolding seq_Union_left Star_def
by auto }
then have "X \<subseteq> B ;; A\<star>" by auto
ultimately