Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/LexerExt.thy
changeset 228 8b432cef3805
parent 227 a8749366ad5d
child 229 81c85f2746f5
equal deleted inserted replaced
227:a8749366ad5d 228:8b432cef3805 
    11 where 
    11 where 
    12   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
 
    12   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
 
    13 
    13 
    14 text {* Two Simple Properties about Sequential Composition *}
 
    14 text {* Two Simple Properties about Sequential Composition *}
 
    15 
    15 
    16 lemma seq_empty [simp]:
 
    16 lemma Sequ_empty [simp]:
 
    17   shows "A ;; {[]} = A"
 
    17   shows "A ;; {[]} = A"
 
    18   and   "{[]} ;; A = A"
 
    18   and   "{[]} ;; A = A"
 
    19 by (simp_all add: Sequ_def)
 
    19 by (simp_all add: Sequ_def)
 
    20 
    20 
    21 lemma seq_null [simp]:
 
    21 lemma Sequ_null [simp]:
 
    22   shows "A ;; {} = {}"
 
    22   shows "A ;; {} = {}"
 
    23   and   "{} ;; A = {}"
 
    23   and   "{} ;; A = {}"
 
    24 by (simp_all add: Sequ_def)
 
    24 by (simp_all add: Sequ_def)
 
    25 
    25 
    26 lemma seq_assoc: 
    26 lemma Sequ_assoc: 
    27   shows "A ;; (B ;; C) = (A ;; B) ;; C"
 
    27   shows "A ;; (B ;; C) = (A ;; B) ;; C"
 
    28 apply(auto simp add: Sequ_def)
 
    28 apply(auto simp add: Sequ_def)
 
    29 apply(metis append_assoc)
 
    29 apply(metis append_assoc)
 
    30 apply(metis)
 
    30 apply(metis)
 
    31 done
 
    31 done
 
       
    32 
       
    33 lemma Sequ_UNION: 
       
    34   shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)"
 
       
    35 by (auto simp add: Sequ_def)
 
       
    36 
    32 
    37 
    33 section {* Semantic Derivative (Left Quotient) of Languages *}
 
    38 section {* Semantic Derivative (Left Quotient) of Languages *}
 
    34 
    39 
    35 definition
 
    40 definition
 
    36   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 
    41   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 
    82 
    87 
    83 lemma Pow_empty [simp]:
 
    88 lemma Pow_empty [simp]:
 
    84   shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
 
    89   shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
 
    85 by(induct n) (auto simp add: Sequ_def)
 
    90 by(induct n) (auto simp add: Sequ_def)
 
    86 
    91 
       
    92 lemma Der_Pow [simp]:
 
       
    93   shows "Der c (A \<up> (Suc n)) = 
       
    94      (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
 
       
    95 unfolding Der_def Sequ_def 
       
    96 by(auto simp add: Cons_eq_append_conv Sequ_def)
 
       
    97 
       
    98 lemma Der_Pow_subseteq:
 
       
    99   assumes "[] \<in> A"  
       
   100   shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
 
       
   101 using assms
 
       
   102 apply(induct n)
 
       
   103 apply(simp add: Sequ_def Der_def)
 
       
   104 apply(simp)
 
       
   105 apply(rule conjI)
 
       
   106 apply (smt Sequ_def append_Nil2 mem_Collect_eq Sequ_assoc subsetI)
 
       
   107 apply(subgoal_tac "((Der c A) ;; (A \<up> n)) \<subseteq> ((Der c A) ;; (A ;; (A \<up> n)))")
 
       
   108 apply(auto)[1]
 
       
   109 by (smt Sequ_def append_Nil2 mem_Collect_eq Sequ_assoc subsetI)
 
       
   110 
       
   111 lemma test:
 
       
   112   shows "(\<Union>x\<le>Suc n. Der c (A \<up> x)) = (\<Union>x\<le>n. Der c A ;; A \<up> x)"
 
       
   113 apply(induct n)
 
       
   114 apply(simp)
 
       
   115 apply(auto)[1]
 
       
   116 apply(case_tac xa)
 
       
   117 apply(simp)
 
       
   118 apply(simp)
 
       
   119 apply(auto)[1]
 
       
   120 apply(case_tac "[] \<in> A")
 
       
   121 apply(simp)
 
       
   122 apply(simp)
 
       
   123 by (smt Der_Pow Der_Pow_subseteq UN_insert atMost_Suc sup.orderE sup_bot.right_neutral)
 
       
   124 
       
   125 lemma test2:
 
       
   126   shows "(\<Union>x\<in>(Suc ` A). Der c (B \<up> x)) = (\<Union>x\<in>A. Der c B ;; B \<up> x)"
 
       
   127 apply(auto)[1]
 
       
   128 apply(case_tac "[] \<in> B")
 
       
   129 apply(simp)
 
       
   130 using Der_Pow_subseteq apply blast
 
       
   131 apply(simp)
 
       
   132 done
 
       
   133 
       
   134 
    87 section {* Kleene Star for Languages *}
 
   135 section {* Kleene Star for Languages *}
 
    88 
   136 
    89 inductive_set
 
   137 definition 
    90   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
 
   138   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) where
 
    91   for A :: "string set"
 
   139   "A\<star> = (\<Union>n. A \<up> n)"
 
    92 where
 
   140 
    93   start[intro]: "[] \<in> A\<star>"
 
   141 lemma Star_empty [intro]:
 
    94 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
   142   shows "[] \<in> A\<star>"
 
       
   143 unfolding Star_def
 
       
   144 by auto
 
       
   145 
       
   146 lemma Star_step [intro]:
 
       
   147   assumes "s1 \<in> A" "s2 \<in> A\<star>"
 
       
   148   shows "s1 @ s2 \<in> A\<star>"
 
       
   149 proof -
 
       
   150   from assms obtain n where "s1 \<in>A" "s2 \<in> A \<up> n"
 
       
   151   unfolding Star_def by auto
 
       
   152   then have "s1 @ s2 \<in> A ;; (A \<up> n)"
 
       
   153   by (auto simp add: Sequ_def)
 
       
   154   then have "s1 @ s2 \<in> A \<up> (Suc n)"
 
       
   155   by simp
 
       
   156   then show "s1 @ s2 \<in> A\<star>" 
       
   157   unfolding Star_def 
       
   158   by (auto simp del: Pow.simps)
 
       
   159 qed
 
    95 
   160 
    96 lemma star_cases:
 
   161 lemma star_cases:
 
    97   shows "A\<star> = {[]} \<union> A ;; A\<star>"
 
   162   shows "A\<star> = {[]} \<union> A ;; A\<star>"
 
    98 unfolding Sequ_def
 
   163 unfolding Star_def
 
    99 by (auto) (metis Star.simps)
 
   164 apply(simp add: Sequ_def)
 
   100 
   165 apply(auto)
 
   101 lemma star_decomp: 
   166 apply(case_tac xa)
 
   102   assumes a: "c # x \<in> A\<star>" 
   167 apply(auto simp add: Sequ_def)
 
   103   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
 
   168 apply(rule_tac x="Suc xa" in exI)
 
   104 using a
 
   169 apply(auto simp add: Sequ_def)
 
   105 by (induct x\<equiv>"c # x" rule: Star.induct) 
   170 done
 
   106    (auto simp add: append_eq_Cons_conv)
 
   171 
       
   172 lemma Der_Star1:
 
       
   173   shows "Der c (A ;; A\<star>) = (Der c A) ;; A\<star>"
 
       
   174 proof -
 
       
   175   have "(Der c A) ;; A\<star> = (Der c A) ;; (\<Union>n. A \<up> n)"
 
       
   176   unfolding Star_def by simp
 
       
   177   also have "... = (\<Union>n. Der c A ;; A \<up> n)"
 
       
   178   unfolding Sequ_UNION by simp
 
       
   179   also have "... = (\<Union>x\<in>(Suc ` UNIV). Der c (A \<up> x))"
 
       
   180   unfolding test2 by simp
 
       
   181   also have "... = (\<Union>n. Der c (A \<up> (Suc n)))"
 
       
   182   by (simp)
 
       
   183   also have "... = Der c (\<Union>n. A \<up> (Suc n))"
 
       
   184   unfolding Der_UNION by simp
 
       
   185   also have "... = Der c (A ;; (\<Union>n. A \<up> n))"
 
       
   186   by (simp only: Pow.simps Sequ_UNION)
 
       
   187   finally show "Der c (A ;; A\<star>) = (Der c A) ;; A\<star>"
 
       
   188   unfolding Star_def[symmetric] by blast 
       
   189 qed
 
   107 
   190 
   108 lemma Der_star [simp]:
 
   191 lemma Der_star [simp]:
 
   109   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 
   192   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 
   110 proof -    
   193 proof -    
   111   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  
   194   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  
   112     by (simp only: star_cases[symmetric])
 
   195     by (simp only: star_cases[symmetric])
 
   113   also have "... = Der c (A ;; A\<star>)"
 
   196   also have "... = Der c (A ;; A\<star>)"
 
   114     by (simp only: Der_union Der_empty) (simp)
 
   197     by (simp only: Der_union Der_empty) (simp)
 
   115   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
 
       
   116     by simp
 
       
   117   also have "... =  (Der c A) ;; A\<star>"
 
   198   also have "... =  (Der c A) ;; A\<star>"
 
   118     unfolding Sequ_def Der_def
 
   199     using Der_Star1 by simp
 
   119     by (auto dest: star_decomp)
 
       
   120   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 
   200   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 
   121 qed
 
   201 qed
 
   122 
   202 
   123 lemma Star_in_Pow:
 
   203 
   124   assumes a: "s \<in> A\<star>"
 
       
   125   shows "\<exists>n. s \<in> A \<up> n"
 
       
   126 using a
 
       
   127 apply(induct)
 
       
   128 apply(auto)
 
       
   129 apply(rule_tac x="Suc n" in exI)
 
       
   130 apply(auto simp add: Sequ_def)
 
       
   131 done
 
       
   132 
       
   133 lemma Pow_in_Star:
 
       
   134   assumes a: "s \<in> A \<up> n"
 
       
   135   shows "s \<in> A\<star>"
 
       
   136 using a
 
       
   137 by (induct n arbitrary: s) (auto simp add: Sequ_def)
 
       
   138 
       
   139 
       
   140 lemma Star_def2: 
       
   141   shows "A\<star> = (\<Union>n. A \<up> n)"
 
       
   142 using Star_in_Pow Pow_in_Star
 
       
   143 by (auto)
 
       
   144 
   204 
   145 
   205 
   146 section {* Regular Expressions *}
 
   206 section {* Regular Expressions *}
 
   147 
   207 
   148 datatype rexp =
 
   208 datatype rexp =
 
   206 | "der c (NTIMES r 0) = ZERO"
 
   266 | "der c (NTIMES r 0) = ZERO"
 
   207 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)"
 
   267 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)"
 
   208 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
 
   268 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
 
   209 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)"
 
   269 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)"
 
   210 | "der c (NMTIMES r n m) = 
   270 | "der c (NMTIMES r n m) = 
   211      (if m < n then ZERO else (if n = 0 then  (if m = 0 then ZERO else SEQ (der c r) (UPNTIMES r (m - 1))) else 
   271      (if m < n then ZERO 
   212                                SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
   272       else (if n = 0 then (if m = 0 then ZERO else 
       
   273                            SEQ (der c r) (UPNTIMES r (m - 1))) else 
       
   274                            SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
   213 
   275 
   214 fun 
   276 fun 
   215  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   277  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   216 where
 
   278 where
 
   217   "ders [] r = r"
 
   279   "ders [] r = r"
 
   221 lemma nullable_correctness:
 
   283 lemma nullable_correctness:
 
   222   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
   284   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 
   223 apply(induct r) 
   285 apply(induct r) 
   224 apply(auto simp add: Sequ_def) 
   286 apply(auto simp add: Sequ_def) 
   225 done
 
   287 done
 
   226 
       
   227 
       
   228 lemma Suc_reduce_Union2:
 
       
   229   "(\<Union>x\<in>{Suc n..}. B x) = (\<Union>x\<in>{n..}. B (Suc x))"
 
       
   230 apply(auto)
 
       
   231 apply(rule_tac x="xa - 1" in bexI)
 
       
   232 apply(simp)
 
       
   233 apply(simp)
 
       
   234 done
 
       
   235 
       
   236 lemma Seq_UNION: 
       
   237   shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)"
 
       
   238 by (auto simp add: Sequ_def)
 
       
   239 
       
   240 lemma Der_Pow [simp]:
 
       
   241   shows "Der c (A \<up> (Suc n)) = 
       
   242      (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
 
       
   243 unfolding Der_def Sequ_def 
       
   244 by(auto simp add: Cons_eq_append_conv Sequ_def)
 
       
   245 
       
   246 lemma Suc_Union:
 
       
   247   "(\<Union>x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union>x\<le>m. B x))"
 
       
   248 by (metis UN_insert atMost_Suc)
 
       
   249 
       
   250 
       
   251 lemma Der_Pow_subseteq:
 
       
   252   assumes "[] \<in> A"  
       
   253   shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
 
       
   254 using assms
 
       
   255 apply(induct n)
 
       
   256 apply(simp add: Sequ_def Der_def)
 
       
   257 apply(simp)
 
       
   258 apply(rule conjI)
 
       
   259 apply (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI)
 
       
   260 apply(subgoal_tac "((Der c A) ;; (A \<up> n)) \<subseteq> ((Der c A) ;; (A ;; (A \<up> n)))")
 
       
   261 apply(auto)[1]
 
       
   262 by (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI)
 
       
   263 
       
   264 lemma test:
 
       
   265   shows "(\<Union>x\<le>Suc n. Der c (L r \<up> x)) = (\<Union>x\<le>n. Der c (L r) ;; L r \<up> x)"
 
       
   266 apply(induct n)
 
       
   267 apply(simp)
 
       
   268 apply(auto)[1]
 
       
   269 apply(case_tac xa)
 
       
   270 apply(simp)
 
       
   271 apply(simp)
 
       
   272 apply(auto)[1]
 
       
   273 apply(case_tac "[] \<in> L r")
 
       
   274 apply(simp)
 
       
   275 apply(simp)
 
       
   276 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem)
 
       
   277 
       
   278 lemma test2:
 
       
   279   shows "(\<Union>x\<in>(Suc ` A). Der c (L r \<up> x)) = (\<Union>x\<in>A. Der c (L r) ;; L r \<up> x)"
 
       
   280 apply(auto)[1]
 
       
   281 apply(case_tac "[] \<in> L r")
 
       
   282 apply(simp)
 
       
   283 defer
 
       
   284 apply(simp)
 
       
   285 using Der_Pow_subseteq by blast
 
       
   286 
       
   287 
   288 
   288 lemma Der_Pow_notin:
 
   289 lemma Der_Pow_notin:
 
   289   assumes "[] \<notin> A"
 
   290   assumes "[] \<notin> A"
 
   290   shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
 
   291   shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
 
   291 using assms
 
   292 using assms
 
   295   shows "L (der c r) = Der c (L r)"
 
   296   shows "L (der c r) = Der c (L r)"
 
   296 apply(induct c r rule: der.induct) 
   297 apply(induct c r rule: der.induct) 
   297 apply(simp_all add: nullable_correctness)[7]
 
   298 apply(simp_all add: nullable_correctness)[7]
 
   298 apply(simp only: der.simps L.simps)
 
   299 apply(simp only: der.simps L.simps)
 
   299 apply(simp only: Der_UNION)
 
   300 apply(simp only: Der_UNION)
 
   300 apply(simp only: Seq_UNION[symmetric])
 
   301 apply(simp only: Sequ_UNION[symmetric])
 
   301 apply(simp add: test)
 
   302 apply(simp add: test)
 
   302 apply(simp)
 
   303 apply(simp)
 
   303 (* NTIMES *)
 
   304 (* NTIMES *)
 
   304 apply(simp only: L.simps der.simps)
 
   305 apply(simp only: L.simps der.simps)
 
   305 apply(simp)
 
   306 apply(simp)
 
   307 apply (simp add: Der_Pow_subseteq sup_absorb1)
 
   308 apply (simp add: Der_Pow_subseteq sup_absorb1)
 
   308 (* FROMNTIMES *)
 
   309 (* FROMNTIMES *)
 
   309 apply(simp only: der.simps)
 
   310 apply(simp only: der.simps)
 
   310 apply(simp only: L.simps)
 
   311 apply(simp only: L.simps)
 
   311 apply(simp)
 
   312 apply(simp)
 
   312 using Der_star Star_def2 apply auto[1]
 
   313 using Der_star Star_def apply auto[1]
 
   313 apply(simp only: der.simps)
 
   314 apply(simp only: der.simps)
 
   314 apply(simp only: L.simps)
 
   315 apply(simp only: L.simps)
 
   315 apply(simp add: Der_UNION)
 
   316 apply(simp add: Der_UNION)
 
   316 apply(smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1)
 
   317 apply(subst Sequ_UNION[symmetric])
 
       
   318 apply(subst test2[symmetric])
 
       
   319 apply(subgoal_tac "(Suc ` {n..}) = {Suc n..}")
 
       
   320 apply simp
 
       
   321 apply(auto simp add: image_def)[1]
 
       
   322 using Suc_le_D apply blast
 
   317 (* NMTIMES *)
 
   323 (* NMTIMES *)
 
   318 apply(case_tac "n \<le> m")
 
   324 apply(case_tac "n \<le> m")
 
   319 prefer 2
 
   325 prefer 2
 
   320 apply(simp only: der.simps if_True)
 
   326 apply(simp only: der.simps if_True)
 
   321 apply(simp only: L.simps)
 
   327 apply(simp only: L.simps)
 
   322 apply(simp)
 
   328 apply(simp)
 
   323 apply(auto)
 
   329 apply(auto)
 
   324 apply(subst (asm) Seq_UNION[symmetric])
 
   330 apply(subst (asm) Sequ_UNION[symmetric])
 
   325 apply(subst (asm) test[symmetric])
 
   331 apply(subst (asm) test[symmetric])
 
   326 apply(auto simp add: Der_UNION)[1]
 
   332 apply(auto simp add: Der_UNION)[1]
 
   327 apply(auto simp add: Der_UNION)[1]
 
   333 apply(auto simp add: Der_UNION)[1]
 
   328 apply(subst Seq_UNION[symmetric])
 
   334 apply(subst Sequ_UNION[symmetric])
 
   329 apply(subst test[symmetric])
 
   335 apply(subst test[symmetric])
 
   330 apply(auto)[1]
 
   336 apply(auto)[1]
 
   331 apply(subst (asm) Seq_UNION[symmetric])
 
   337 apply(subst (asm) Sequ_UNION[symmetric])
 
   332 apply(subst (asm) test2[symmetric])
 
   338 apply(subst (asm) test2[symmetric])
 
   333 apply(auto simp add: Der_UNION)[1]
 
   339 apply(auto simp add: Der_UNION)[1]
 
   334 apply(subst Seq_UNION[symmetric])
 
   340 apply(subst Sequ_UNION[symmetric])
 
   335 apply(subst test2[symmetric])
 
   341 apply(subst test2[symmetric])
 
   336 apply(auto simp add: Der_UNION)[1]
 
   342 apply(auto simp add: Der_UNION)[1]
 
   337 done
 
   343 done
 
   338 
   344 
   339 lemma ders_correctness:
 
   345 lemma ders_correctness:
 
   457 apply(rule Prf_Pow)
 
   463 apply(rule Prf_Pow)
 
   458 apply(simp)
 
   464 apply(simp)
 
   459 apply(simp)
 
   465 apply(simp)
 
   460 done
 
   466 done
 
   461 
   467 
       
   468 lemma Star_Pow:
 
       
   469   assumes "s \<in> A \<up> n"
 
       
   470   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)"
 
       
   471 using assms
 
       
   472 apply(induct n arbitrary: s)
 
       
   473 apply(auto simp add: Sequ_def)
 
       
   474 apply(drule_tac x="s2" in meta_spec)
 
       
   475 apply(auto)
 
       
   476 apply(rule_tac x="s1#ss" in exI)
 
       
   477 apply(simp)
 
       
   478 done
 
       
   479 
   462 lemma Star_string:
 
   480 lemma Star_string:
 
   463   assumes "s \<in> A\<star>"
 
   481   assumes "s \<in> A\<star>"
 
   464   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
 
   482   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
 
   465 using assms
 
   483 using assms
 
   466 apply(induct rule: Star.induct)
 
   484 apply(auto simp add: Star_def)
 
   467 apply(auto)
 
   485 using Star_Pow by blast
 
   468 apply(rule_tac x="[]" in exI)
 
   486 
   469 apply(simp)
 
       
   470 apply(rule_tac x="s1#ss" in exI)
 
       
   471 apply(simp)
 
       
   472 done
 
       
   473 
   487 
   474 lemma Star_val:
 
   488 lemma Star_val:
 
   475   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
 
   489   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
 
   476   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
 
   490   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
 
   477 using assms
 
   491 using assms
 
   487 apply(induct ss)
 
   501 apply(induct ss)
 
   488 apply(auto)
 
   502 apply(auto)
 
   489 by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD)
 
   503 by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD)
 
   490 
   504 
   491 
   505 
   492 lemma Star_Pow:
 
   506 
   493   assumes "s \<in> A \<up> n"
 
       
   494   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)"
 
       
   495 using assms
 
       
   496 apply(induct n arbitrary: s)
 
       
   497 apply(auto simp add: Sequ_def)
 
       
   498 apply(drule_tac x="s2" in meta_spec)
 
       
   499 apply(auto)
 
       
   500 apply(rule_tac x="s1#ss" in exI)
 
       
   501 apply(simp)
 
       
   502 done
 
       
   503 
   507 
   504 
   508 
   505 lemma L_flat_Prf2:
 
   509 lemma L_flat_Prf2:
 
   506   assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 
   510   assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 
   507 using assms
 
   511 using assms
 
   762 apply (induct s r v rule: Posix.induct)
 
   766 apply (induct s r v rule: Posix.induct)
 
   763 apply(auto simp add: Sequ_def)
 
   767 apply(auto simp add: Sequ_def)
 
   764 apply(rule_tac x="Suc x" in bexI)
 
   768 apply(rule_tac x="Suc x" in bexI)
 
   765 apply(auto simp add: Sequ_def)
 
   769 apply(auto simp add: Sequ_def)
 
   766 apply(rule_tac x="Suc x" in bexI)
 
   770 apply(rule_tac x="Suc x" in bexI)
 
   767 apply(auto simp add: Sequ_def)
 
   771 using Sequ_def apply auto[2]
 
   768 apply(simp add: Star_in_Pow)
 
   772 apply(simp add: Star_def)
 
   769 apply(rule_tac x="Suc x" in bexI)
 
   773 apply(rule_tac x="Suc x" in bexI)
 
   770 apply(auto simp add: Sequ_def)
 
   774 apply(auto simp add: Sequ_def)
 
   771 done
 
   775 done
 
   772 
   776 
   773 
   777 
  1391       apply(simp)
 
  1395       apply(simp)
 
  1392       apply(rotate_tac 4)
 
  1396       apply(rotate_tac 4)
 
  1393       apply(erule Posix.cases)
 
  1397       apply(erule Posix.cases)
 
  1394       apply(simp_all)
 
  1398       apply(simp_all)
 
  1395       apply (simp add: Posix1a Prf_injval_flat)
 
  1399       apply (simp add: Posix1a Prf_injval_flat)
 
  1396       apply(simp only: Star_def2)
 
  1400       apply(simp only: Star_def)
 
  1397       apply(simp only: der_correctness Der_def)
 
  1401       apply(simp only: der_correctness Der_def)
 
  1398       apply(simp)
 
  1402       apply(simp)
 
  1399       done
 
  1403       done
 
  1400       then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp
 
  1404       then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp
 
  1401     qed
 
  1405     qed
lexing