--- a/thys/LexerExt.thy	Thu Mar 02 00:56:40 2017 +0000
+++ b/thys/LexerExt.thy	Thu Mar 02 12:39:27 2017 +0000
@@ -13,23 +13,28 @@
 
 text {* Two Simple Properties about Sequential Composition *}
 
-lemma seq_empty [simp]:
+lemma Sequ_empty [simp]:
   shows "A ;; {[]} = A"
   and   "{[]} ;; A = A"
 by (simp_all add: Sequ_def)
 
-lemma seq_null [simp]:
+lemma Sequ_null [simp]:
   shows "A ;; {} = {}"
   and   "{} ;; A = {}"
 by (simp_all add: Sequ_def)
 
-lemma seq_assoc: 
+lemma Sequ_assoc: 
   shows "A ;; (B ;; C) = (A ;; B) ;; C"
 apply(auto simp add: Sequ_def)
 apply(metis append_assoc)
 apply(metis)
 done
 
+lemma Sequ_UNION: 
+  shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)"
+by (auto simp add: Sequ_def)
+
+
 section {* Semantic Derivative (Left Quotient) of Languages *}
 
 definition
@@ -84,26 +89,104 @@
   shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
 by(induct n) (auto simp add: Sequ_def)
 
+lemma Der_Pow [simp]:
+  shows "Der c (A \<up> (Suc n)) = 
+     (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
+unfolding Der_def Sequ_def 
+by(auto simp add: Cons_eq_append_conv Sequ_def)
+
+lemma Der_Pow_subseteq:
+  assumes "[] \<in> A"  
+  shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
+using assms
+apply(induct n)
+apply(simp add: Sequ_def Der_def)
+apply(simp)
+apply(rule conjI)
+apply (smt Sequ_def append_Nil2 mem_Collect_eq Sequ_assoc subsetI)
+apply(subgoal_tac "((Der c A) ;; (A \<up> n)) \<subseteq> ((Der c A) ;; (A ;; (A \<up> n)))")
+apply(auto)[1]
+by (smt Sequ_def append_Nil2 mem_Collect_eq Sequ_assoc subsetI)
+
+lemma test:
+  shows "(\<Union>x\<le>Suc n. Der c (A \<up> x)) = (\<Union>x\<le>n. Der c A ;; A \<up> x)"
+apply(induct n)
+apply(simp)
+apply(auto)[1]
+apply(case_tac xa)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(case_tac "[] \<in> A")
+apply(simp)
+apply(simp)
+by (smt Der_Pow Der_Pow_subseteq UN_insert atMost_Suc sup.orderE sup_bot.right_neutral)
+
+lemma test2:
+  shows "(\<Union>x\<in>(Suc ` A). Der c (B \<up> x)) = (\<Union>x\<in>A. Der c B ;; B \<up> x)"
+apply(auto)[1]
+apply(case_tac "[] \<in> B")
+apply(simp)
+using Der_Pow_subseteq apply blast
+apply(simp)
+done
+
+
 section {* Kleene Star for Languages *}
 
-inductive_set
-  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
-  for A :: "string set"
-where
-  start[intro]: "[] \<in> A\<star>"
-| step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
+definition 
+  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) where
+  "A\<star> = (\<Union>n. A \<up> n)"
+
+lemma Star_empty [intro]:
+  shows "[] \<in> A\<star>"
+unfolding Star_def
+by auto
+
+lemma Star_step [intro]:
+  assumes "s1 \<in> A" "s2 \<in> A\<star>"
+  shows "s1 @ s2 \<in> A\<star>"
+proof -
+  from assms obtain n where "s1 \<in>A" "s2 \<in> A \<up> n"
+  unfolding Star_def by auto
+  then have "s1 @ s2 \<in> A ;; (A \<up> n)"
+  by (auto simp add: Sequ_def)
+  then have "s1 @ s2 \<in> A \<up> (Suc n)"
+  by simp
+  then show "s1 @ s2 \<in> A\<star>" 
+  unfolding Star_def 
+  by (auto simp del: Pow.simps)
+qed
 
 lemma star_cases:
   shows "A\<star> = {[]} \<union> A ;; A\<star>"
-unfolding Sequ_def
-by (auto) (metis Star.simps)
+unfolding Star_def
+apply(simp add: Sequ_def)
+apply(auto)
+apply(case_tac xa)
+apply(auto simp add: Sequ_def)
+apply(rule_tac x="Suc xa" in exI)
+apply(auto simp add: Sequ_def)
+done
 
-lemma star_decomp: 
-  assumes a: "c # x \<in> A\<star>" 
-  shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
-using a
-by (induct x\<equiv>"c # x" rule: Star.induct) 
-   (auto simp add: append_eq_Cons_conv)
+lemma Der_Star1:
+  shows "Der c (A ;; A\<star>) = (Der c A) ;; A\<star>"
+proof -
+  have "(Der c A) ;; A\<star> = (Der c A) ;; (\<Union>n. A \<up> n)"
+  unfolding Star_def by simp
+  also have "... = (\<Union>n. Der c A ;; A \<up> n)"
+  unfolding Sequ_UNION by simp
+  also have "... = (\<Union>x\<in>(Suc ` UNIV). Der c (A \<up> x))"
+  unfolding test2 by simp
+  also have "... = (\<Union>n. Der c (A \<up> (Suc n)))"
+  by (simp)
+  also have "... = Der c (\<Union>n. A \<up> (Suc n))"
+  unfolding Der_UNION by simp
+  also have "... = Der c (A ;; (\<Union>n. A \<up> n))"
+  by (simp only: Pow.simps Sequ_UNION)
+  finally show "Der c (A ;; A\<star>) = (Der c A) ;; A\<star>"
+  unfolding Star_def[symmetric] by blast 
+qed
 
 lemma Der_star [simp]:
   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
@@ -112,35 +195,12 @@
     by (simp only: star_cases[symmetric])
   also have "... = Der c (A ;; A\<star>)"
     by (simp only: Der_union Der_empty) (simp)
-  also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
-    by simp
   also have "... =  (Der c A) ;; A\<star>"
-    unfolding Sequ_def Der_def
-    by (auto dest: star_decomp)
+    using Der_Star1 by simp
   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 qed
 
-lemma Star_in_Pow:
-  assumes a: "s \<in> A\<star>"
-  shows "\<exists>n. s \<in> A \<up> n"
-using a
-apply(induct)
-apply(auto)
-apply(rule_tac x="Suc n" in exI)
-apply(auto simp add: Sequ_def)
-done
 
-lemma Pow_in_Star:
-  assumes a: "s \<in> A \<up> n"
-  shows "s \<in> A\<star>"
-using a
-by (induct n arbitrary: s) (auto simp add: Sequ_def)
-
-
-lemma Star_def2: 
-  shows "A\<star> = (\<Union>n. A \<up> n)"
-using Star_in_Pow Pow_in_Star
-by (auto)
 
 
 section {* Regular Expressions *}
@@ -208,8 +268,10 @@
 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)"
 | "der c (NMTIMES r n m) = 
-     (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 
-                               SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
+     (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 
+                           SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -224,67 +286,6 @@
 apply(auto simp add: Sequ_def) 
 done
 
-
-lemma Suc_reduce_Union2:
-  "(\<Union>x\<in>{Suc n..}. B x) = (\<Union>x\<in>{n..}. B (Suc x))"
-apply(auto)
-apply(rule_tac x="xa - 1" in bexI)
-apply(simp)
-apply(simp)
-done
-
-lemma Seq_UNION: 
-  shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)"
-by (auto simp add: Sequ_def)
-
-lemma Der_Pow [simp]:
-  shows "Der c (A \<up> (Suc n)) = 
-     (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
-unfolding Der_def Sequ_def 
-by(auto simp add: Cons_eq_append_conv Sequ_def)
-
-lemma Suc_Union:
-  "(\<Union>x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union>x\<le>m. B x))"
-by (metis UN_insert atMost_Suc)
-
-
-lemma Der_Pow_subseteq:
-  assumes "[] \<in> A"  
-  shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
-using assms
-apply(induct n)
-apply(simp add: Sequ_def Der_def)
-apply(simp)
-apply(rule conjI)
-apply (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI)
-apply(subgoal_tac "((Der c A) ;; (A \<up> n)) \<subseteq> ((Der c A) ;; (A ;; (A \<up> n)))")
-apply(auto)[1]
-by (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI)
-
-lemma test:
-  shows "(\<Union>x\<le>Suc n. Der c (L r \<up> x)) = (\<Union>x\<le>n. Der c (L r) ;; L r \<up> x)"
-apply(induct n)
-apply(simp)
-apply(auto)[1]
-apply(case_tac xa)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(case_tac "[] \<in> L r")
-apply(simp)
-apply(simp)
-by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem)
-
-lemma test2:
-  shows "(\<Union>x\<in>(Suc ` A). Der c (L r \<up> x)) = (\<Union>x\<in>A. Der c (L r) ;; L r \<up> x)"
-apply(auto)[1]
-apply(case_tac "[] \<in> L r")
-apply(simp)
-defer
-apply(simp)
-using Der_Pow_subseteq by blast
-
-
 lemma Der_Pow_notin:
   assumes "[] \<notin> A"
   shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
@@ -297,7 +298,7 @@
 apply(simp_all add: nullable_correctness)[7]
 apply(simp only: der.simps L.simps)
 apply(simp only: Der_UNION)
-apply(simp only: Seq_UNION[symmetric])
+apply(simp only: Sequ_UNION[symmetric])
 apply(simp add: test)
 apply(simp)
 (* NTIMES *)
@@ -309,11 +310,16 @@
 apply(simp only: der.simps)
 apply(simp only: L.simps)
 apply(simp)
-using Der_star Star_def2 apply auto[1]
+using Der_star Star_def apply auto[1]
 apply(simp only: der.simps)
 apply(simp only: L.simps)
 apply(simp add: Der_UNION)
-apply(smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1)
+apply(subst Sequ_UNION[symmetric])
+apply(subst test2[symmetric])
+apply(subgoal_tac "(Suc ` {n..}) = {Suc n..}")
+apply simp
+apply(auto simp add: image_def)[1]
+using Suc_le_D apply blast
 (* NMTIMES *)
 apply(case_tac "n \<le> m")
 prefer 2
@@ -321,17 +327,17 @@
 apply(simp only: L.simps)
 apply(simp)
 apply(auto)
-apply(subst (asm) Seq_UNION[symmetric])
+apply(subst (asm) Sequ_UNION[symmetric])
 apply(subst (asm) test[symmetric])
 apply(auto simp add: Der_UNION)[1]
 apply(auto simp add: Der_UNION)[1]
-apply(subst Seq_UNION[symmetric])
+apply(subst Sequ_UNION[symmetric])
 apply(subst test[symmetric])
 apply(auto)[1]
-apply(subst (asm) Seq_UNION[symmetric])
+apply(subst (asm) Sequ_UNION[symmetric])
 apply(subst (asm) test2[symmetric])
 apply(auto simp add: Der_UNION)[1]
-apply(subst Seq_UNION[symmetric])
+apply(subst Sequ_UNION[symmetric])
 apply(subst test2[symmetric])
 apply(auto simp add: Der_UNION)[1]
 done
@@ -459,17 +465,25 @@
 apply(simp)
 done
 
+lemma Star_Pow:
+  assumes "s \<in> A \<up> n"
+  shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)"
+using assms
+apply(induct n arbitrary: s)
+apply(auto simp add: Sequ_def)
+apply(drule_tac x="s2" in meta_spec)
+apply(auto)
+apply(rule_tac x="s1#ss" in exI)
+apply(simp)
+done
+
 lemma Star_string:
   assumes "s \<in> A\<star>"
   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
 using assms
-apply(induct rule: Star.induct)
-apply(auto)
-apply(rule_tac x="[]" in exI)
-apply(simp)
-apply(rule_tac x="s1#ss" in exI)
-apply(simp)
-done
+apply(auto simp add: Star_def)
+using Star_Pow by blast
+
 
 lemma Star_val:
   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
@@ -489,17 +503,7 @@
 by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD)
 
 
-lemma Star_Pow:
-  assumes "s \<in> A \<up> n"
-  shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)"
-using assms
-apply(induct n arbitrary: s)
-apply(auto simp add: Sequ_def)
-apply(drule_tac x="s2" in meta_spec)
-apply(auto)
-apply(rule_tac x="s1#ss" in exI)
-apply(simp)
-done
+
 
 
 lemma L_flat_Prf2:
@@ -764,8 +768,8 @@
 apply(rule_tac x="Suc x" in bexI)
 apply(auto simp add: Sequ_def)
 apply(rule_tac x="Suc x" in bexI)
-apply(auto simp add: Sequ_def)
-apply(simp add: Star_in_Pow)
+using Sequ_def apply auto[2]
+apply(simp add: Star_def)
 apply(rule_tac x="Suc x" in bexI)
 apply(auto simp add: Sequ_def)
 done
@@ -1393,7 +1397,7 @@
       apply(erule Posix.cases)
       apply(simp_all)
       apply (simp add: Posix1a Prf_injval_flat)
-      apply(simp only: Star_def2)
+      apply(simp only: Star_def)
       apply(simp only: der_correctness Der_def)
       apply(simp)
       done