34 |
34 |
35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100) |
35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100) |
36 where |
36 where |
37 "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}" |
37 "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}" |
38 |
38 |
39 text {* |
|
40 Transitive closure of language @{text "L"}. |
|
41 *} |
|
42 |
|
43 inductive_set |
|
44 Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102) |
|
45 for L |
|
46 where |
|
47 start[intro]: "[] \<in> L\<star>" |
|
48 | step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" |
|
49 |
|
50 text {* Some properties of operator @{text ";;"}. *} |
39 text {* Some properties of operator @{text ";;"}. *} |
|
40 |
|
41 lemma seq_add_left: |
|
42 assumes a: "A = B" |
|
43 shows "C ;; A = C ;; B" |
|
44 using a by simp |
51 |
45 |
52 lemma seq_union_distrib_right: |
46 lemma seq_union_distrib_right: |
53 shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)" |
47 shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)" |
54 unfolding Seq_def by auto |
48 unfolding Seq_def by auto |
55 |
49 |
71 lemma seq_empty [simp]: |
65 lemma seq_empty [simp]: |
72 shows "A ;; {[]} = A" |
66 shows "A ;; {[]} = A" |
73 and "{[]} ;; A = A" |
67 and "{[]} ;; A = A" |
74 by (simp_all add: Seq_def) |
68 by (simp_all add: Seq_def) |
75 |
69 |
76 |
70 fun |
77 lemma star_intro1[rule_format]: |
71 pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100) |
78 "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>" |
72 where |
79 by (erule Star.induct, auto) |
73 "A \<up> 0 = {[]}" |
80 |
74 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
81 lemma star_intro2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>" |
75 |
82 by (drule step[of y lang "[]"], auto simp:start) |
76 definition |
83 |
77 Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102) |
84 lemma star_intro3[rule_format]: |
78 where |
85 "x \<in> lang\<star> \<Longrightarrow> \<forall>y . y \<in> lang \<longrightarrow> x @ y \<in> lang\<star>" |
79 "A\<star> \<equiv> (\<Union>n. A \<up> n)" |
86 by (erule Star.induct, auto intro:star_intro2) |
80 |
|
81 lemma star_start[intro]: |
|
82 shows "[] \<in> A\<star>" |
|
83 proof - |
|
84 have "[] \<in> A \<up> 0" by auto |
|
85 then show "[] \<in> A\<star>" unfolding Star_def by blast |
|
86 qed |
|
87 |
|
88 lemma star_step [intro]: |
|
89 assumes a: "s1 \<in> A" |
|
90 and b: "s2 \<in> A\<star>" |
|
91 shows "s1 @ s2 \<in> A\<star>" |
|
92 proof - |
|
93 from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto |
|
94 then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def) |
|
95 then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast |
|
96 qed |
|
97 |
|
98 lemma star_induct[consumes 1, case_names start step]: |
|
99 assumes a: "x \<in> A\<star>" |
|
100 and b: "P []" |
|
101 and c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)" |
|
102 shows "P x" |
|
103 proof - |
|
104 from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto |
|
105 then show "P x" |
|
106 by (induct n arbitrary: x) |
|
107 (auto intro!: b c simp add: Seq_def Star_def) |
|
108 qed |
|
109 |
|
110 lemma star_intro1: |
|
111 assumes a: "x \<in> A\<star>" |
|
112 and b: "y \<in> A\<star>" |
|
113 shows "x @ y \<in> A\<star>" |
|
114 using a b |
|
115 by (induct rule: star_induct) (auto) |
|
116 |
|
117 lemma star_intro2: |
|
118 assumes a: "y \<in> A" |
|
119 shows "y \<in> A\<star>" |
|
120 proof - |
|
121 from a have "y @ [] \<in> A\<star>" by blast |
|
122 then show "y \<in> A\<star>" by simp |
|
123 qed |
|
124 |
|
125 lemma star_intro3: |
|
126 assumes a: "x \<in> A\<star>" |
|
127 and b: "y \<in> A" |
|
128 shows "x @ y \<in> A\<star>" |
|
129 using a b by (blast intro: star_intro1 star_intro2) |
87 |
130 |
88 lemma star_decom: |
131 lemma star_decom: |
89 "\<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>)" |
132 "\<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>)" |
90 by (induct x rule: Star.induct, simp, blast) |
133 apply(induct rule: star_induct) |
|
134 apply(simp) |
|
135 apply(blast) |
|
136 done |
91 |
137 |
92 lemma lang_star_cases: |
138 lemma lang_star_cases: |
93 shows "L\<star> = {[]} \<union> L ;; L\<star>" |
139 shows "L\<star> = {[]} \<union> L ;; L\<star>" |
94 proof |
140 proof |
95 { fix x |
141 { fix x |
96 have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ;; L\<star>" |
142 have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ;; L\<star>" |
97 unfolding Seq_def |
143 unfolding Seq_def |
98 by (induct rule: Star.induct) (auto) |
144 by (induct rule: star_induct) (auto) |
99 } |
145 } |
100 then show "L\<star> \<subseteq> {[]} \<union> L ;; L\<star>" by auto |
146 then show "L\<star> \<subseteq> {[]} \<union> L ;; L\<star>" by auto |
101 next |
147 next |
102 show "{[]} \<union> L ;; L\<star> \<subseteq> L\<star>" |
148 show "{[]} \<union> L ;; L\<star> \<subseteq> L\<star>" |
103 unfolding Seq_def by auto |
149 unfolding Seq_def by auto |
104 qed |
|
105 |
|
106 fun |
|
107 pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100) |
|
108 where |
|
109 "A \<up> 0 = {[]}" |
|
110 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
|
111 |
|
112 lemma star_pow_eq: |
|
113 shows "A\<star> = (\<Union>n. A \<up> n)" |
|
114 proof - |
|
115 { fix n x |
|
116 assume "x \<in> (A \<up> n)" |
|
117 then have "x \<in> A\<star>" |
|
118 by (induct n arbitrary: x) (auto simp add: Seq_def) |
|
119 } |
|
120 moreover |
|
121 { fix x |
|
122 assume "x \<in> A\<star>" |
|
123 then have "\<exists>n. x \<in> A \<up> n" |
|
124 proof (induct rule: Star.induct) |
|
125 case start |
|
126 have "[] \<in> A \<up> 0" by auto |
|
127 then show "\<exists>n. [] \<in> A \<up> n" by blast |
|
128 next |
|
129 case (step s1 s2) |
|
130 have "s1 \<in> A" by fact |
|
131 moreover |
|
132 have "\<exists>n. s2 \<in> A \<up> n" by fact |
|
133 then obtain n where "s2 \<in> A \<up> n" by blast |
|
134 ultimately |
|
135 have "s1 @ s2 \<in> A \<up> (Suc n)" by (auto simp add: Seq_def) |
|
136 then show "\<exists>n. s1 @ s2 \<in> A \<up> n" by blast |
|
137 qed |
|
138 } |
|
139 ultimately show "A\<star> = (\<Union>n. A \<up> n)" by auto |
|
140 qed |
150 qed |
141 |
151 |
142 lemma |
152 lemma |
143 shows seq_Union_left: "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))" |
153 shows seq_Union_left: "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))" |
144 and seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)" |
154 and seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)" |
224 proof |
234 proof |
225 assume eq: "X = B ;; A\<star>" |
235 assume eq: "X = B ;; A\<star>" |
226 have "A\<star> = {[]} \<union> A\<star> ;; A" |
236 have "A\<star> = {[]} \<union> A\<star> ;; A" |
227 unfolding seq_star_comm[symmetric] |
237 unfolding seq_star_comm[symmetric] |
228 by (rule lang_star_cases) |
238 by (rule lang_star_cases) |
229 then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" |
239 then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" |
230 unfolding Seq_def by simp |
240 by (rule seq_add_left) |
231 also have "\<dots> = B \<union> B ;; (A\<star> ;; A)" |
241 also have "\<dots> = B \<union> B ;; (A\<star> ;; A)" |
232 unfolding seq_union_distrib_left by simp |
242 unfolding seq_union_distrib_left by simp |
233 also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" |
243 also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" |
234 by (simp only: seq_assoc) |
244 by (simp only: seq_assoc) |
235 finally show "X = X ;; A \<union> B" |
245 finally show "X = X ;; A \<union> B" |
236 using eq by blast |
246 using eq by blast |
237 next |
247 next |
238 assume eq: "X = X ;; A \<union> B" |
248 assume eq: "X = X ;; A \<union> B" |
239 { fix n::nat |
249 { fix n::nat |
240 have "B ;; (A \<up> n) \<subseteq> X" using ardens_helper[OF eq, of "n"] by auto } |
250 have "B ;; (A \<up> n) \<subseteq> X" using ardens_helper[OF eq, of "n"] by auto } |
241 then have "B ;; A\<star> \<subseteq> X" unfolding star_pow_eq Seq_def |
251 then have "B ;; A\<star> \<subseteq> X" |
242 by (auto simp add: UNION_def) |
252 unfolding Seq_def Star_def UNION_def |
|
253 by auto |
243 moreover |
254 moreover |
244 { fix s::string |
255 { fix s::string |
245 obtain k where "k = length s" by auto |
256 obtain k where "k = length s" by auto |
246 then have not_in: "s \<notin> X ;; (A \<up> Suc k)" |
257 then have not_in: "s \<notin> X ;; (A \<up> Suc k)" |
247 using seq_pow_length[OF nemp] by blast |
258 using seq_pow_length[OF nemp] by blast |