# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1454159556 0
# Node ID 3c8cfdf95252b4c0426b3af18e4a40de8867d19b
# Parent  9613e6ace30fa463675cd0d2907ba896a9e6a345
proved some lemmas about star and mkeps (injval etc not yet done)

diff -r 9613e6ace30f -r 3c8cfdf95252 thys/ReStar.thy
--- a/thys/ReStar.thy	Thu Jan 21 12:47:20 2016 +0000
+++ b/thys/ReStar.thy	Sat Jan 30 13:12:36 2016 +0000
@@ -108,7 +108,6 @@
 apply(simp)
 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>"
@@ -116,6 +115,22 @@
 by (induct x\<equiv>"c # x" rule: Star.induct) 
    (auto simp add: append_eq_Cons_conv)
 
+(*
+lemma star_induct[consumes 1, case_names Nil append, induct set: Star]:
+assumes "w \<in> A\<star>"
+  and "P []"
+  and step: "\<And>u v. u \<in> A \<Longrightarrow> v \<in> A\<star> \<Longrightarrow> P v \<Longrightarrow> P (u @ v)"
+shows "P w"
+proof -
+  { fix n have "w \<in> A \<up> n \<Longrightarrow> P w"
+      apply(induct n arbitrary: w) 
+      apply(auto intro: `P []` step star2 simp add: Sequ_def)
+      done
+  }
+  with `w \<in> A\<star>` show "P w" by (auto simp: star3)
+qed
+*)
+
 section {* Regular Expressions *}
 
 datatype rexp =
@@ -177,6 +192,12 @@
 | "flat (Star []) = []"
 | "flat (Star (v#vs)) = (flat v) @ (flat (Star vs))" 
 
+lemma [simp]:
+ "flat (Star vs) = concat (map flat vs)"
+apply(induct vs)
+apply(auto)
+done
+
 section {* Relation between values and regular expressions *}
 
 inductive 
@@ -205,20 +226,34 @@
 apply(auto simp add: Sequ_def)
 done
 
+lemma Prf_Star:
+  assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
+  shows "\<turnstile> Star vs : STAR r"
+using assms
+apply(induct vs)
+apply (metis Prf.intros(6))
+by (metis Prf.intros(7) insert_iff set_simps(2))
 
-lemma Prf_Star_flat_L:
-  assumes "\<turnstile> v : STAR r" shows "flat v \<in> (L r)\<star>"
+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 v r\<equiv>"STAR r" arbitrary: r rule: Prf.induct)
+apply(induct rule: Star.induct)
 apply(auto)
-apply(simp add: star3)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(rule_tac x="s1#ss" in exI)
+apply(simp)
+done
+
+lemma Star_val:
+  assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
+  shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
+using assms
+apply(induct ss)
 apply(auto)
-apply(rule_tac x="Suc x" in exI)
-apply(auto simp add: Sequ_def)
-apply(rule_tac x="flat v" in exI)
-apply(rule_tac x="flat (Star vs)" in exI)
-apply(auto)
-by (metis Prf_flat_L)
+apply (metis empty_iff list.set(1))
+by (metis concat.simps(2) list.simps(9) set_ConsD)
 
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
@@ -231,150 +266,18 @@
 apply (metis Prf.intros(3) flat.simps(4))
 apply(erule Prf.cases)
 apply(auto)
-apply(simp add: star3)
+apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
+apply(auto)[1]
+apply(rule_tac x="Star vs" in exI)
+apply(simp)
+apply(rule Prf_Star)
+apply(simp)
+apply(drule Star_string)
 apply(auto)
-sorry
-
-section {* Greedy Ordering according to Frisch/Cardelli *}
-
-inductive 
-  GrOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ gr\<succ> _")
-where 
-  "v1 gr\<succ> v1' \<Longrightarrow> (Seq v1 v2) gr\<succ> (Seq v1' v2')"
-| "v2 gr\<succ> v2' \<Longrightarrow> (Seq v1 v2) gr\<succ> (Seq v1 v2')"
-| "v1 gr\<succ> v2 \<Longrightarrow> (Left v1) gr\<succ> (Left v2)"
-| "v1 gr\<succ> v2 \<Longrightarrow> (Right v1) gr\<succ> (Right v2)"
-| "(Left v2) gr\<succ>(Right v1)"
-| "(Char c) gr\<succ> (Char c)"
-| "(Void) gr\<succ> (Void)"
-
-lemma Gr_refl:
-  assumes "\<turnstile> v : r"
-  shows "v gr\<succ> v"
-using assms
-apply(induct)
-apply(auto intro: GrOrd.intros)
-done
-
-lemma Gr_total:
-  assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r"
-  shows "v1 gr\<succ> v2 \<or> v2 gr\<succ> v1"
-using assms
-apply(induct v1 r arbitrary: v2 rule: Prf.induct)
-apply(rotate_tac 4)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis GrOrd.intros(1) GrOrd.intros(2))
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(clarify)
-apply (metis GrOrd.intros(3))
-apply(clarify)
-apply (metis GrOrd.intros(5))
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(clarify)
-apply (metis GrOrd.intros(5))
-apply(clarify)
-apply (metis GrOrd.intros(4))
-apply(erule Prf.cases)
-apply(simp_all)
-apply (metis GrOrd.intros(7))
-apply(erule Prf.cases)
-apply(simp_all)
-apply (metis GrOrd.intros(6))
+apply(rule Star_val)
+apply(simp)
 done
 
-lemma Gr_trans: 
-  assumes "v1 gr\<succ> v2" "v2 gr\<succ> v3" 
-  and     "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<turnstile> v3 : r"
-  shows "v1 gr\<succ> v3"
-using assms
-apply(induct r arbitrary: v1 v2 v3)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-defer
-(* ALT case *)
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply (metis GrOrd.intros(3))
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply (metis GrOrd.intros(5))
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply (metis GrOrd.intros(5))
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply (metis GrOrd.intros(4))
-(* SEQ case *)
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[5]
-apply(clarify)
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply (metis GrOrd.intros(1))
-apply (metis GrOrd.intros(1))
-apply(erule GrOrd.cases)
-apply(simp_all (no_asm_use))[7]
-apply (metis GrOrd.intros(1))
-by (metis GrOrd.intros(1) Gr_refl)
-
 
 section {* Values Sets *}
 
@@ -458,31 +361,32 @@
 apply(auto)
 (*NULL*)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 (*EMPTY*)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(rule Prf.intros)
 apply (metis append_Nil prefix_def)
 (*CHAR*)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(rule Prf.intros)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 (*ALT*)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis Prf.intros(2))
 apply (metis Prf.intros(3))
 (*SEQ*)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 apply (metis Prf.intros(1))
 apply (simp add: append_eq_conv_conj prefix_def rest_def)
 done
 
+(* This lemma needs to be adapted to Star
 lemma Values_finite:
   "finite (Values r s)"
 apply(induct r arbitrary: s)
@@ -499,6 +403,7 @@
 apply(rule finite_Suffixes)
 apply(simp)
 done
+*)
 
 section {* Sulzmann functions *}
 
@@ -508,6 +413,7 @@
   "mkeps(EMPTY) = Void"
 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
+| "mkeps(STAR r) = Star []"
 
 section {* Derivatives *}
 
@@ -522,6 +428,7 @@
      (if nullable r1
       then ALT (SEQ (der c r1) r2) (der c r2)
       else SEQ (der c r1) r2)"
+| "der c (STAR r) = SEQ (der c r) (STAR r)"
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -589,6 +496,8 @@
 apply(auto)
 done
 
+(* HERE *)
+
 lemma v3:
   assumes "\<turnstile> v : der c r" 
   shows "\<turnstile> (injval r c v) : r"