lexing: comparison thys/ReStar.thy

equal deleted inserted replaced

-:80218dddbb15
+:489dfa0d7ec9
 theory ReStar
 imports "Main"
 begin
-section {* Sequential Composition of Sets *}
+section {* Sequential Composition of Languages *}
 definition
 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where
 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"
-fun spow where
-"spow s 0 = []"
-| "spow s (Suc n) = s @ spow s n"
 text {* Two Simple Properties about Sequential Composition *}
 lemma seq_empty [simp]:
 shows "A ;; {[]} = A"
 and   "{[]} ;; A = A"
 lemma seq_null [simp]:
 shows "A ;; {} = {}"
 and   "{} ;; A = {}"
 by (simp_all add: Sequ_def)
+section {* Semantic Derivatives of Languages *}
 definition
 Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 where
 "Der c A \<equiv> {s. [c] @ s \<in> A}"
 lemma Der_union [simp]:
 shows "Der c (A \<union> B) = Der c A \<union> Der c B"
 unfolding Der_def
 by auto
-lemma Der_seq [simp]:
+lemma Der_Sequ [simp]:
 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
 unfolding Der_def Sequ_def
-apply (auto simp add: Cons_eq_append_conv)
+by (auto simp add: Cons_eq_append_conv)
-done
-lemma seq_image:
+section {* Kleene Star for Languages *}
-assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
-shows "f ` (A ;; B) = (f ` A) ;; (f ` B)"
-apply(auto simp add: Sequ_def image_def)
-apply(rule_tac x="f s1" in exI)
-apply(rule_tac x="f s2" in exI)
-using assms
-apply(auto)
-apply(rule_tac x="xa @ xb" in exI)
-using assms
-apply(auto)
-done
-section {* Kleene Star for Sets *}
 inductive_set
 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
 for A :: "string set"
 where
 lemma star_cases:
 shows "A\<star> = {[]} \<union> A ;; A\<star>"
 unfolding Sequ_def
 by (auto) (metis Star.simps)
-fun
-pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [100,100] 100)
-where
-"A \<up> 0 = {[]}"
-| "A \<up> (Suc n) = A ;; (A \<up> n)"
-lemma star1:
-shows "s \<in> A\<star> \<Longrightarrow> \<exists>n. s \<in> A \<up> n"
-apply(induct rule: Star.induct)
-apply (metis pow.simps(1) insertI1)
-apply(auto)
-apply(rule_tac x="Suc n" in exI)
-apply(auto simp add: Sequ_def)
-done
-lemma star2:
-shows "s \<in> A \<up> n \<Longrightarrow> s \<in> A\<star>"
-apply(induct n arbitrary: s)
-apply (metis pow.simps(1) Star.simps empty_iff insertE)
-apply(auto simp add: Sequ_def)
-done
-lemma star3:
-shows "A\<star> = (\<Union>i. A \<up> i)"
-using star1 star2
-apply(auto)
-done
-lemma star4:
-shows "s \<in> A \<up> n \<Longrightarrow> \<exists>ss. s = concat ss \<and> (\<forall>s' \<in> set ss. s' \<in> A)"
-apply(induct n arbitrary: s)
-apply(auto simp add: Sequ_def)
-apply(rule_tac x="[]" in exI)
-apply(auto)
-apply(drule_tac x="s2" in meta_spec)
-apply(auto)
-by (metis concat.simps(2) insertE set_simps(2))
-lemma star5:
-assumes "f [] = []"
-assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
-shows "(f ` A) \<up> n = f ` (A \<up> n)"
-apply(induct n)
-apply(simp add: assms)
-apply(simp)
-apply(subst seq_image[OF assms(2)])
-apply(simp)
-done
-lemma star6:
-assumes "f [] = []"
-assumes "\<forall>s1 s2. f (s1 @ s2) = (f s1) @ (f s2)"
-shows "(f ` A)\<star> = f ` (A\<star>)"
-apply(simp add: star3)
-apply(simp add: image_UN)
-apply(subst star5[OF assms])
-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>"
 using a
 by (auto dest: star_decomp)
 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 qed
 section {* Regular Expressions *}
 datatype rexp =
 NULL
 | EMPTY
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
 lemma nullable_correctness:
 shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-apply (induct r)
+by (induct r) (auto simp add: Sequ_def)
-apply(auto simp add: Sequ_def)
-done
 section {* Values *}
 datatype val =
 | "flat (Right v) = flat v"
 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
 | "flat (Stars []) = []"
 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))"
-lemma [simp]:
+lemma flat_Stars [simp]:
 "flat (Stars vs) = concat (map flat vs)"
-apply(induct vs)
+by (induct vs) (auto)
-apply(auto)
-done
 section {* Relation between values and regular expressions *}
-(* non-problematic values...needed in order to fix the *)
-(* proj lemma in Sulzmann & lu *)
-inductive
-NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
-where
-"\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
-| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
-| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
-| "\<Turnstile> Void : EMPTY"
-| "\<Turnstile> Char c : CHAR c"
-| "\<Turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
 inductive
 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
 where
 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
 | "\<turnstile> Void : EMPTY"
 | "\<turnstile> Char c : CHAR c"
 | "\<turnstile> Stars [] : STAR r"
 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
-lemma NPrf_imp_Prf:
-assumes "\<Turnstile> v : r"
-shows "\<turnstile> v : r"
-using assms
-apply(induct)
-apply(auto intro: Prf.intros)
-done
-lemma NPrf_Prf_val:
-shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
-and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
-using assms
-apply(induct v and vs arbitrary: r and r rule: val.inducts)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule_tac x="Void" in exI)
-apply(simp)
-apply(rule NPrf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule_tac x="Char c" in exI)
-apply(simp)
-apply(rule NPrf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(drule_tac x="r1" in meta_spec)
-apply(drule_tac x="r2" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Seq v' v'a" in exI)
-apply(simp)
-apply (metis NPrf.intros(1))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(drule_tac x="r2" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Right v'" in exI)
-apply(simp)
-apply (metis NPrf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(drule_tac x="r1" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Left v'" in exI)
-apply(simp)
-apply (metis NPrf.intros)
-apply(drule_tac x="r" in meta_spec)
-apply(simp)
-apply(auto)[1]
-apply(rule_tac x="Stars vs'" in exI)
-apply(simp)
-apply(rule_tac x="[]" in exI)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis NPrf.intros(6))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)[1]
-apply(drule_tac x="ra" in meta_spec)
-apply(simp)
-apply(drule_tac x="STAR ra" in meta_spec)
-apply(simp)
-apply(auto)
-apply(case_tac "flat v = []")
-apply(rule_tac x="vs'" in exI)
-apply(simp)
-apply(rule_tac x="v' # vs'" in exI)
-apply(simp)
-apply(rule NPrf.intros)
-apply(auto)
-done
-lemma NPrf_Prf:
-shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"
-apply(auto)
-apply (metis NPrf_Prf_val(1))
-by (metis NPrf_imp_Prf)
 lemma not_nullable_flat:
-assumes "\<turnstile> v : r" "\<not>nullable r"
+assumes "\<turnstile> v : r" "\<not> nullable r"
 shows "flat v \<noteq> []"
 using assms
-apply(induct)
+by (induct) (auto)
-apply(auto)
-done
 lemma Prf_flat_L:
 assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
 apply(induct v r rule: Prf.induct)
 apply(auto simp add: Sequ_def)
 done
-lemma NPrf_flat_L:
-assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
-using assms
-by (metis NPrf_imp_Prf Prf_flat_L)
 lemma Prf_Stars:
 assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
 shows "\<turnstile> Stars vs : STAR r"
 using assms
 apply(induct ss)
 apply(auto)
 apply (metis empty_iff list.set(1))
 by (metis concat.simps(2) list.simps(9) set_ConsD)
-lemma Star_valN:
-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 (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}"
 apply(induct r)
 apply(auto dest: Prf_flat_L simp add: Sequ_def)
 apply(auto)
 apply(rule Star_val)
 apply(simp)
 done
-lemma L_flat_NPrf:
-"L(r) = {flat v | v. \<Turnstile> v : r}"
-by (metis L_flat_Prf NPrf_Prf)
 section {* Values Sets *}
 definition prefix :: "string \<Rightarrow> string \<Rightarrow> bool" ("_ \<sqsubseteq> _" [100, 100] 100)
 where
 definition Values :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
 "Values r s \<equiv> {v. \<turnstile> v : r \<and> flat v \<sqsubseteq> s}"
-definition SValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
-"SValues r s \<equiv> {v. \<turnstile> v : r \<and> flat v = s}"
-definition NValues :: "rexp \<Rightarrow> string \<Rightarrow> val set" where
-"NValues r s \<equiv> {v. \<Turnstile> v : r \<and> flat v \<sqsubseteq> s}"
-lemma NValues_STAR_Nil:
-"NValues (STAR r) [] = {Stars []}"
-apply(auto simp add: NValues_def prefix_def)
-apply(erule NPrf.cases)
-apply(auto)
-by (metis NPrf.intros(6))
 definition rest :: "val \<Rightarrow> string \<Rightarrow> string" where
 "rest v s \<equiv> drop (length (flat v)) s"
 lemma rest_Nil:
 "rest v [] = []"
 lemma rest_Suffixes:
 "rest v s \<in> Suffixes s"
 unfolding rest_def
 by (metis Suffixes_in append_take_drop_id)
-lemma rest_SSuffixes:
-assumes "flat v \<noteq> []" "s \<noteq> []"
-shows "rest v s \<in> SSuffixes s"
-using assms
-unfolding rest_def
-thm SSuffixes_in
-apply(rule_tac SSuffixes_in)
-apply(rule_tac x="take (length (flat v)) s" in exI)
-apply(simp add: sprefix_def)
-done
 lemma Values_recs:
 "Values (NULL) s = {}"
 "Values (EMPTY) s = {Void}"
 "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})"
 apply (metis Prf.intros(6))
 apply (metis append_Nil prefix_def)
 apply (metis Prf.intros(7))
 by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
-lemma NValues_recs:
-"NValues (NULL) s = {}"
-"NValues (EMPTY) s = {Void}"
-"NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})"
-"NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
-"NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
-"NValues (STAR r) s =
-{Stars []} \<union> {Stars (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Stars vs \<in> NValues (STAR r) (rest v s)}"
-unfolding NValues_def
-apply(auto)
-(*NULL*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-(*EMPTY*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply(rule NPrf.intros)
-apply (metis append_Nil prefix_def)
-(*CHAR*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply(rule NPrf.intros)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-(*ALT*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply (metis NPrf.intros(2))
-apply (metis NPrf.intros(3))
-(*SEQ*)
-apply(erule NPrf.cases)
-apply(simp_all)[7]
-apply (simp add: append_eq_conv_conj prefix_def rest_def)
-apply (metis NPrf.intros(1))
-apply (simp add: append_eq_conv_conj prefix_def rest_def)
-(*STAR*)
-apply(erule NPrf.cases)
-apply(simp_all)
-apply(rule conjI)
-apply(simp add: prefix_def)
-apply(auto)[1]
-apply(simp add: prefix_def)
-apply(auto)[1]
-apply (metis append_eq_conv_conj rest_def)
-apply (metis NPrf.intros(6))
-apply (metis append_Nil prefix_def)
-apply (metis NPrf.intros(7))
-by (metis append_eq_conv_conj prefix_append prefix_def rest_def)
-lemma SValues_recs:
-"SValues (NULL) s = {}"
-"SValues (EMPTY) s = (if s = [] then {Void} else {})"
-"SValues (CHAR c) s = (if [c] = s then {Char c} else {})"
-"SValues (ALT r1 r2) s = {Left v | v. v \<in> SValues r1 s} \<union> {Right v | v. v \<in> SValues r2 s}"
-"SValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. \<exists>s1 s2. s = s1 @ s2 \<and> v1 \<in> SValues r1 s1 \<and> v2 \<in> SValues r2 s2}"
-"SValues (STAR r) s = (if s = [] then {Stars []} else {}) \<union>
-{Stars (v # vs) | v vs. \<exists>s1 s2. s = s1 @ s2 \<and> v \<in> SValues r s1 \<and> Stars vs \<in> SValues (STAR r) s2}"
-unfolding SValues_def
-apply(auto)
-(*NULL*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*EMPTY*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*CHAR*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis Prf.intros(5))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-(*ALT*)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply metis
-apply(erule Prf.intros)
-apply(erule Prf.intros)
-(* SEQ case *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis Prf.intros(1))
-(* STAR case *)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(rule Prf.intros)
-apply (metis Prf.intros(7))
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply (metis Prf.intros(7))
-by (metis Prf.intros(7))
 lemma finite_image_set2:
 "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {(x, y) | x y. P x \<and> Q y}"
 by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {(x, y)}"]) auto
-lemma NValues_finite_aux:
-"(\<lambda>(r, s). finite (NValues r s)) (r, s)"
-apply(rule wf_induct[of "measure size <*lex*> measure length",where P="\<lambda>(r, s). finite (NValues r s)"])
-apply (metis wf_lex_prod wf_measure)
-apply(auto)
-apply(case_tac a)
-apply(simp_all)
-apply(simp add: NValues_recs)
-apply(simp add: NValues_recs)
-apply(simp add: NValues_recs)
-apply(simp add: NValues_recs)
-apply(rule_tac f="\<lambda>(x, y). Seq x y" and
-A="{(v1, v2) | v1 v2. v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 (rest v1 b)}" in finite_surj)
-prefer 2
-apply(auto)[1]
-apply(rule_tac B="\<Union>sp \<in> Suffixes b. {(v1, v2). v1 \<in> NValues rexp1 b \<and> v2 \<in> NValues rexp2 sp}" in finite_subset)
-apply(auto)[1]
-apply (metis rest_Suffixes)
-apply(rule finite_UN_I)
-apply(rule finite_Suffixes)
-apply(simp)
-apply(simp add: NValues_recs)
-apply(clarify)
-apply(subst NValues_recs)
-apply(simp)
-apply(rule_tac f="\<lambda>(v, vs). Stars (v # vs)" and
-A="{(v, vs) | v vs. v \<in> NValues rexp b \<and> (flat v \<noteq> [] \<and> Stars vs \<in> NValues (STAR rexp) (rest v b))}" in finite_surj)
-prefer 2
-apply(auto)[1]
-apply(auto)
-apply(case_tac b)
-apply(simp)
-defer
-apply(rule_tac B="\<Union>sp \<in> SSuffixes b. {(v, vs) | v vs. v \<in> NValues rexp b \<and> Stars vs \<in> NValues (STAR rexp) sp}" in finite_subset)
-apply(auto)[1]
-apply(rule_tac x="rest aa (a # list)" in bexI)
-apply(simp)
-apply (rule rest_SSuffixes)
-apply(simp)
-apply(simp)
-apply(rule finite_UN_I)
-defer
-apply(frule_tac x="rexp" in spec)
-apply(drule_tac x="b" in spec)
-apply(drule conjunct1)
-apply(drule mp)
-apply(simp)
-apply(drule_tac x="STAR rexp" in spec)
-apply(drule_tac x="sp" in spec)
-apply(drule conjunct2)
-apply(drule mp)
-apply(simp)
-apply(simp add: prefix_def SPrefixes_def SSuffixes_def)
-apply(auto)[1]
-apply (metis length_Cons length_rev length_sprefix rev.simps(2))
-apply(simp)
-apply(rule finite_cartesian_product)
-apply(simp)
-apply(rule_tac f="Stars" in finite_imageD)
-prefer 2
-apply(auto simp add: inj_on_def)[1]
-apply (metis finite_subset image_Collect_subsetI)
-apply(simp add: rest_Nil)
-apply(simp add: NValues_STAR_Nil)
-apply(rule_tac B="{(v, vs). v \<in> NValues rexp [] \<and> vs = []}" in finite_subset)
-apply(auto)[1]
-apply(simp)
-apply(rule_tac B="Suffixes b" in finite_subset)
-apply(auto simp add: SSuffixes_def Suffixes_def Prefixes_def SPrefixes_def sprefix_def)[1]
-by (metis finite_Suffixes)
-lemma NValues_finite:
-"finite (NValues r s)"
-using NValues_finite_aux
-apply(simp)
-done
 section {* Sulzmann functions *}
 fun
 mkeps :: "rexp \<Rightarrow> val"
 apply(simp_all)[7]
 apply(auto)
 apply (metis Prf.intros(6) Prf.intros(7))
 by (metis Prf.intros(7))
-lemma v3_proj:
-assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
-shows "\<Turnstile> (projval r c v) : der c r"
-using assms
-apply(induct rule: NPrf.induct)
-prefer 4
-apply(simp)
-prefer 4
-apply(simp)
-apply (metis NPrf.intros(4))
-prefer 2
-apply(simp)
-apply (metis NPrf.intros(2))
-prefer 2
-apply(simp)
-apply (metis NPrf.intros(3))
-apply(auto)
-apply(rule NPrf.intros)
-apply(simp)
-apply (metis NPrf_imp_Prf not_nullable_flat)
-apply(rule NPrf.intros)
-apply(rule NPrf.intros)
-apply (metis Cons_eq_append_conv)
-apply(simp)
-apply(rule NPrf.intros)
-apply (metis Cons_eq_append_conv)
-apply(simp)
-(* Stars case *)
-apply(rule NPrf.intros)
-apply (metis Cons_eq_append_conv)
-apply(auto)
-done
 lemma v4:
 assumes "\<turnstile> v : der c r"
 shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)[7]
 done
-lemma v4_proj:
-assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
-shows "c # flat (projval r c v) = flat v"
-using assms
-apply(induct rule: NPrf.induct)
-prefer 4
-apply(simp)
-prefer 4
-apply(simp)
-prefer 2
-apply(simp)
-prefer 2
-apply(simp)
-apply(auto)
-apply (metis Cons_eq_append_conv)
-apply(simp add: append_eq_Cons_conv)
-apply(auto)
-done
-lemma v4_proj2:
-assumes "\<Turnstile> v : r" and "(flat v) = c # s"
-shows "flat (projval r c v) = s"
-using assms
-by (metis list.inject v4_proj)
 section {* Our Alternative Posix definition *}
 inductive
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply(clarify)
 by (metis PMatch1(2))
-lemma PMatch1N:
-assumes "s \<in> r \<rightarrow> v"
-shows "\<Turnstile> v : r"
-using assms
-apply(induct s r v rule: PMatch.induct)
-apply(auto)
-apply (metis NPrf.intros(4))
-apply (metis NPrf.intros(5))
-apply (metis NPrf.intros(2))
-apply (metis NPrf.intros(3))
-apply (metis NPrf.intros(1))
-apply(rule NPrf.intros)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(rule NPrf.intros)
-done
 lemma PMatch_Values:
 assumes "s \<in> r \<rightarrow> v"
 shows "v \<in> Values r s"
 using assms
 apply(simp add: Values_def PMatch1)
 by (metis append_Nil2 prefix_def)
-lemma PMatch2:
+(* a proof that does not need proj *)
+lemma PMatch2_roy_version:
 assumes "s \<in> (der c r) \<rightarrow> v"
 shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
 using assms
-apply(induct c r arbitrary: s v rule: der.induct)
+apply(induct r arbitrary: s v c rule: rexp.induct)
 apply(auto)
 (* NULL case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 (* EMPTY case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 (* CHAR case *)
-apply(case_tac "c = c'")
+apply(case_tac "c = char")
 apply(simp)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply (metis PMatch.intros(2))
 apply(simp)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 (* ALT case *)
+prefer 2
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply (metis PMatch.intros(3))
 apply(clarify)
 apply(rule PMatch.intros)
 apply metis
 apply(simp add: der_correctness Der_def)
 (* SEQ case *)
-apply(case_tac "nullable r1")
+apply(case_tac "nullable rexp1")
 apply(simp)
 prefer 2
 (* not-nullbale case *)
 apply(simp)
 apply(erule PMatch.cases)
 apply(auto)[1]
 apply(simp add: der_correctness Der_def)
 apply metis
 (* right interesting case *)
 apply(clarify)
-apply(simp)
-apply(subst (asm) L.simps(4)[symmetric])
-apply(simp only: L_flat_Prf)
-apply(simp)
 apply(subst append.simps(1)[symmetric])
 apply(rule PMatch.intros)
 apply (metis PMatch_mkeps)
 apply metis
-apply(auto)
+apply(rule notI)
-apply(simp only: L_flat_NPrf)
+apply(clarify)
 apply(simp)
-apply(auto)
+apply(simp add: der_correctness)
-apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
+apply(simp only: Der_def Sequ_def)
-apply(drule mp)
-apply(simp)
-apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
-apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
-apply (metis NPrf_imp_Prf Prf.intros(1))
-apply(rule NPrf_imp_Prf)
-apply(rule v3_proj)
 apply(simp)
 apply (metis Cons_eq_append_conv)
 (* Stars case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply(simp)
 apply(simp)
 apply(simp)
 apply (metis L.simps(6))
 apply(subst v4)
-apply (metis NPrf_imp_Prf PMatch1N)
+apply (metis PMatch1)
 apply(simp)
 apply(auto)[1]
 apply(drule_tac x="s\<^sub>3" in spec)
 apply(drule mp)
 defer
 apply metis
 apply(clarify)
 apply(drule_tac x="s1" in meta_spec)
 apply(drule_tac x="v1" in meta_spec)
+apply(drule_tac x="c" in meta_spec)
 apply(simp)
 apply(rotate_tac 2)
 apply(drule PMatch.intros(6))
 apply(rule PMatch.intros(7))
+(* HERE *)
 apply (metis PMatch1(1) list.distinct(1) v4)
 apply (metis Nil_is_append_conv)
 apply(simp)
 apply(subst der_correctness)
 apply(simp add: Der_def)
 done
 lemma lex_correct1:
 assumes "s \<notin> L r"
 shows "lex r s = None"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
 apply (metis mkeps_flat mkeps_nullable nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
-apply(simp add: L_flat_NPrf)
+apply(simp add: der_correctness Der_def)
 apply(auto)
-apply (metis v3_proj v4_proj2)
 apply (metis v3)
 apply(rule v4)
-by metis
+by simp
 lemma lex_correct3:
 assumes "s \<in> L r"
 shows "\<exists>v. lex r s = Some(v) \<and> s \<in> r \<rightarrow> v"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
 apply (metis PMatch_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
-apply(simp add: L_flat_NPrf)
+apply(simp add: der_correctness Der_def)
 apply(auto)
-apply (metis v3_proj v4_proj2)
+by (metis PMatch2_roy_version)
-apply(rule PMatch2)
-apply(simp)
-done
-lemma lex_correct4:
-assumes "s \<in> L r"
-shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
-using lex_correct3[OF assms]
-apply(auto)
-apply (metis PMatch1N)
-by (metis PMatch1(2))
 lemma lex_correct5:
 assumes "s \<in> L r"
 shows "s \<in> r \<rightarrow> (lex2 r s)"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
 apply (metis PMatch_mkeps nullable_correctness)
 apply(simp)
-apply(rule PMatch2)
+apply(rule PMatch2_roy_version)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
-apply(simp add: L_flat_NPrf)
+apply(simp add: der_correctness Der_def)
 apply(auto)
-apply (metis v3_proj v4_proj2)
 done
 lemma
 "lex2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))"
 apply(simp)
 done
-section {* Sulzmann's Ordering of values *}
+section {* Connection with Sulzmann's Ordering of values *}
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 where
 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')"
 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')"
 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))"
 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))"
 | "(Stars []) \<succ>(STAR r) (Stars [])"
+(* non-problematic values...needed in order to fix the *)
+(* proj lemma in Sulzmann & lu *)
+inductive
+NPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100)
+where
+"\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2"
+| "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2"
+| "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2"
+| "\<Turnstile> Void : EMPTY"
+| "\<Turnstile> Char c : CHAR c"
+| "\<Turnstile> Stars [] : STAR r"
+| "\<lbrakk>\<Turnstile> v : r; \<Turnstile> Stars vs : STAR r; flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (v # vs) : STAR r"
+lemma NPrf_imp_Prf:
+assumes "\<Turnstile> v : r"
+shows "\<turnstile> v : r"
+using assms
+apply(induct)
+apply(auto intro: Prf.intros)
+done
+lemma Star_valN:
+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 (metis empty_iff list.set(1))
+by (metis concat.simps(2) list.simps(9) set_ConsD)
+lemma NPrf_Prf_val:
+shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
+and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
+using assms
+apply(induct v and vs arbitrary: r and r rule: val.inducts)
+apply(auto)[1]
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule_tac x="Void" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(rule_tac x="Char c" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule_tac x="r1" in meta_spec)
+apply(drule_tac x="r2" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Seq v' v'a" in exI)
+apply(simp)
+apply (metis NPrf.intros(1))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule_tac x="r2" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Right v'" in exI)
+apply(simp)
+apply (metis NPrf.intros)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(drule_tac x="r1" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Left v'" in exI)
+apply(simp)
+apply (metis NPrf.intros)
+apply(drule_tac x="r" in meta_spec)
+apply(simp)
+apply(auto)[1]
+apply(rule_tac x="Stars vs'" in exI)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply (metis NPrf.intros(6))
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(auto)[1]
+apply(drule_tac x="ra" in meta_spec)
+apply(simp)
+apply(drule_tac x="STAR ra" in meta_spec)
+apply(simp)
+apply(auto)
+apply(case_tac "flat v = []")
+apply(rule_tac x="vs'" in exI)
+apply(simp)
+apply(rule_tac x="v' # vs'" in exI)
+apply(simp)
+apply(rule NPrf.intros)
+apply(auto)
+done
+lemma NPrf_Prf:
+shows "{flat v | v. \<turnstile> v : r} = {flat v | v. \<Turnstile> v : r}"
+apply(auto)
+apply (metis NPrf_Prf_val(1))
+by (metis NPrf_imp_Prf)
+lemma NPrf_flat_L:
+assumes "\<Turnstile> v : r" shows "flat v \<in> L r"
+using assms
+by (metis NPrf_imp_Prf Prf_flat_L)
+lemma L_flat_NPrf:
+"L(r) = {flat v | v. \<Turnstile> v : r}"
+by (metis L_flat_Prf NPrf_Prf)
+lemma v3_proj:
+assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+shows "\<Turnstile> (projval r c v) : der c r"
+using assms
+apply(induct rule: NPrf.induct)
+prefer 4
+apply(simp)
+prefer 4
+apply(simp)
+apply (metis NPrf.intros(4))
+prefer 2
+apply(simp)
+apply (metis NPrf.intros(2))
+prefer 2
+apply(simp)
+apply (metis NPrf.intros(3))
+apply(auto)
+apply(rule NPrf.intros)
+apply(simp)
+apply (metis NPrf_imp_Prf not_nullable_flat)
+apply(rule NPrf.intros)
+apply(rule NPrf.intros)
+apply (metis Cons_eq_append_conv)
+apply(simp)
+apply(rule NPrf.intros)
+apply (metis Cons_eq_append_conv)
+apply(simp)
+(* Stars case *)
+apply(rule NPrf.intros)
+apply (metis Cons_eq_append_conv)
+apply(auto)
+done
+lemma v4_proj:
+assumes "\<Turnstile> v : r" and "\<exists>s. (flat v) = c # s"
+shows "c # flat (projval r c v) = flat v"
+using assms
+apply(induct rule: NPrf.induct)
+prefer 4
+apply(simp)
+prefer 4
+apply(simp)
+prefer 2
+apply(simp)
+prefer 2
+apply(simp)
+apply(auto)
+apply (metis Cons_eq_append_conv)
+apply(simp add: append_eq_Cons_conv)
+apply(auto)
+done
+lemma v4_proj2:
+assumes "\<Turnstile> v : r" and "(flat v) = c # s"
+shows "flat (projval r c v) = s"
+using assms
+by (metis list.inject v4_proj)
+lemma PMatch1N:
+assumes "s \<in> r \<rightarrow> v"
+shows "\<Turnstile> v : r"
+using assms
+apply(induct s r v rule: PMatch.induct)
+apply(auto)
+apply (metis NPrf.intros(4))
+apply (metis NPrf.intros(5))
+apply (metis NPrf.intros(2))
+apply (metis NPrf.intros(3))
+apply (metis NPrf.intros(1))
+apply(rule NPrf.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(rule NPrf.intros)
+done
+(* this version needs proj *)
+lemma PMatch2:
+assumes "s \<in> (der c r) \<rightarrow> v"
+shows "(c#s) \<in> r \<rightarrow> (injval r c v)"
+using assms
+apply(induct c r arbitrary: s v rule: der.induct)
+apply(auto)
+(* NULL case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* EMPTY case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* CHAR case *)
+apply(case_tac "c = c'")
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply (metis PMatch.intros(2))
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* ALT case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply (metis PMatch.intros(3))
+apply(clarify)
+apply(rule PMatch.intros)
+apply metis
+apply(simp add: der_correctness Der_def)
+(* SEQ case *)
+apply(case_tac "nullable r1")
+apply(simp)
+prefer 2
+(* not-nullbale case *)
+apply(simp)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply metis
+apply(auto)[1]
+apply(simp add: der_correctness Der_def)
+apply(auto)[1]
+(* nullable case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+(* left case *)
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)[4]
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
+apply(clarify)
+apply(simp (no_asm))
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply metis
+apply(erule contrapos_nn)
+apply(erule exE)+
+apply(auto)[1]
+apply(simp add: der_correctness Der_def)
+apply metis
+(* right interesting case *)
+apply(clarify)
+apply(simp)
+apply(subst (asm) L.simps(4)[symmetric])
+apply(simp only: L_flat_Prf)
+apply(simp)
+apply(subst append.simps(1)[symmetric])
+apply(rule PMatch.intros)
+apply (metis PMatch_mkeps)
+apply metis
+apply(auto)
+apply(simp only: L_flat_NPrf)
+apply(simp)
+apply(auto)
+apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
+apply(drule mp)
+apply(simp)
+apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
+apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
+apply (metis NPrf_imp_Prf Prf.intros(1))
+apply(rule NPrf_imp_Prf)
+apply(rule v3_proj)
+apply(simp)
+apply (metis Cons_eq_append_conv)
+(* Stars case *)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(clarify)
+apply(rotate_tac 2)
+apply(frule_tac PMatch1)
+apply(erule PMatch.cases)
+apply(simp_all)[7]
+apply(subst append.simps(2)[symmetric])
+apply(rule PMatch.intros)
+apply metis
+apply(auto)[1]
+apply(rule PMatch.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+apply (metis L.simps(6))
+apply(subst v4)
+apply (metis NPrf_imp_Prf PMatch1N)
+apply(simp)
+apply(auto)[1]
+apply(drule_tac x="s\<^sub>3" in spec)
+apply(drule mp)
+defer
+apply metis
+apply(clarify)
+apply(drule_tac x="s1" in meta_spec)
+apply(drule_tac x="v1" in meta_spec)
+apply(simp)
+apply(rotate_tac 2)
+apply(drule PMatch.intros(6))
+apply(rule PMatch.intros(7))
+apply (metis PMatch1(1) list.distinct(1) v4)
+apply (metis Nil_is_append_conv)
+apply(simp)
+apply(subst der_correctness)
+apply(simp add: Der_def)
+done
+lemma lex_correct4:
+assumes "s \<in> L r"
+shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
+using lex_correct3[OF assms]
+apply(auto)
+apply (metis PMatch1N)
+by (metis PMatch1(2))
 end

changeset 106	489dfa0d7ec9
parent 105	80218dddbb15
child 107	6adda4a667b1