lexing: comparison thys/ReStar.thy

equal deleted inserted replaced

-:97735ef233be
+:da81ffac4b10
 section {* Our Alternative Posix definition *}
 inductive
-PMatch :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
+Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
 where
 "[] \<in> ONE \<rightarrow> Void"
 | "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
 | "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
 | "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
 | "[] \<in> STAR r \<rightarrow> Stars []"
-inductive_cases PMatch_elims:
+inductive_cases Posix_elims:
 "s \<in> ONE \<rightarrow> v"
 "s \<in> CHAR c \<rightarrow> v"
 "s \<in> ALT r1 r2 \<rightarrow> v"
 "s \<in> SEQ r1 r2 \<rightarrow> v"
 "s \<in> STAR r \<rightarrow> v"
-lemma PMatch1:
+lemma Posix1:
 assumes "s \<in> r \<rightarrow> v"
 shows "s \<in> L r" "flat v = s"
 using assms
-by (induct s r v rule: PMatch.induct)
+by (induct s r v rule: Posix.induct)
 (auto simp add: Sequ_def)
-lemma PMatch1a:
+lemma Posix1a:
 assumes "s \<in> r \<rightarrow> v"
 shows "\<turnstile> v : r"
 using assms
-apply(induct s r v rule: PMatch.induct)
+apply(induct s r v rule: Posix.induct)
 apply(auto intro: Prf.intros)
 done
-lemma PMatch_mkeps:
+lemma Posix_mkeps:
 assumes "nullable r"
 shows "[] \<in> r \<rightarrow> mkeps r"
 using assms
 apply(induct r)
-apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def)
+apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
 apply(subst append.simps(1)[symmetric])
-apply(rule PMatch.intros)
+apply(rule Posix.intros)
 apply(auto)
 done
-lemma PMatch_determ:
+lemma Posix_determ:
 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
 shows "v1 = v2"
 using assms
-apply(induct s r v1 arbitrary: v2 rule: PMatch.induct)
+apply(induct s r v1 arbitrary: v2 rule: Posix.induct)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all)[7]
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all)[7]
 apply(rotate_tac 2)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
 apply(clarify)
 apply(force)
 apply(clarify)
-apply(drule PMatch1(1))
+apply(drule Posix1(1))
 apply(simp)
 apply(rotate_tac 3)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
-apply(drule PMatch1(1))+
+apply(drule Posix1(1))+
 apply(simp)
 apply(simp)
 apply(rotate_tac 5)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
 apply(clarify)
 apply(subgoal_tac "s1 = s1a")
 apply(blast)
 apply(simp add: append_eq_append_conv2)
 apply(clarify)
-apply (metis PMatch1(1) append_self_conv)
+apply (metis Posix1(1) append_self_conv)
 apply(rotate_tac 6)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
 apply(clarify)
 apply(subgoal_tac "s1 = s1a")
 apply(simp)
 apply(blast)
 apply(simp  (no_asm_use) add: append_eq_append_conv2)
 apply(clarify)
-apply (metis L.simps(6) PMatch1(1) append_self_conv)
+apply (metis L.simps(6) Posix1(1) append_self_conv)
 apply(clarify)
 apply(rotate_tac 2)
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
-using PMatch1(2) apply auto[1]
+using Posix1(2) apply auto[1]
-using PMatch1(2) apply blast
+using Posix1(2) apply blast
-apply(erule PMatch.cases)
+apply(erule Posix.cases)
 apply(simp_all (no_asm_use))[7]
 apply(clarify)
-apply (simp add: PMatch1(2))
+apply (simp add: Posix1(2))
 apply(simp)
 done
 (* a proof that does not need proj *)
-lemma PMatch2_roy_version:
+lemma Posix2_roy_version:
 assumes "s \<in> (der c r) \<rightarrow> v"
 shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 using assms
 proof(induct r arbitrary: s v rule: rexp.induct)
 case ZERO
 case eq
 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
 then have "s \<in> ONE \<rightarrow> v" using eq by simp
 then have eqs: "s = [] \<and> v = Void" by cases simp
 show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs
-by (auto intro: PMatch.intros)
+by (auto intro: Posix.intros)
 next
 case ineq
 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
 then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
 then have "False" by cases
 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v"
 proof (cases)
 case left
 have "s \<in> der c r1 \<rightarrow> v'" by fact
 then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
-then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: PMatch.intros)
+then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)
 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
 next
 case right
 have "s \<notin> L (der c r1)" by fact
 then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def)
 moreover
 have "s \<in> der c r2 \<rightarrow> v'" by fact
 then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
 ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')"
-by (auto intro: PMatch.intros)
+by (auto intro: Posix.intros)
 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
 qed
 next
 case (SEQ r1 r2)
 have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
 "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)"
 | (not_nullable) v1 v2 s1 s2 where
 "v = Seq v1 v2" "s = s1 @ s2"
 "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1"
 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"
-by (force split: if_splits elim!: PMatch_elims simp add: Sequ_def der_correctness Der_def)
+by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def)
 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v"
 proof (cases)
 case left_nullable
 have "s1 \<in> der c r1 \<rightarrow> v1" by fact
 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
 moreover
 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
-ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac PMatch.intros)
+ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp
 next
 case right_nullable
 have "nullable r1" by fact
-then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule PMatch_mkeps)
+then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
 moreover
 have "s \<in> der c r2 \<rightarrow> v1" by fact
 then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
 moreover
 have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact
 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable
 by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)
 ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
-by(rule PMatch.intros)
+by(rule Posix.intros)
 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
 next
 case not_nullable
 have "s1 \<in> der c r1 \<rightarrow> v1" by fact
 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
 moreover
 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
 ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable
-by (rule_tac PMatch.intros) (simp_all)
+by (rule_tac Posix.intros) (simp_all)
 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
 qed
 next
 case (STAR r)
 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
 then consider
 (cons) v1 vs s1 s2 where
 "v = Seq v1 (Stars vs)" "s = s1 @ s2"
 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
-apply(auto elim!: PMatch_elims(1-4) simp add: der_correctness Der_def intro: PMatch.intros)
+apply(auto elim!: Posix_elims(1-4) simp add: der_correctness Der_def intro: Posix.intros)
 apply(rotate_tac 3)
-apply(erule_tac PMatch_elims(5))
+apply(erule_tac Posix_elims(5))
-apply (simp add: PMatch.intros(6))
+apply (simp add: Posix.intros(6))
-using PMatch.intros(7) by blast
+using Posix.intros(7) by blast
 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v"
 proof (cases)
 case cons
 have "s1 \<in> der c r \<rightarrow> v1" by fact
 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
 moreover
 have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
 moreover
 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
-then have "flat (injval r c v1) = (c # s1)" by (rule PMatch1)
+then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
 then have "flat (injval r c v1) \<noteq> []" by simp
 moreover
 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
 by (simp add: der_correctness Der_def)
 ultimately
-have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule PMatch.intros)
+have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
 qed
 qed
 assumes "s \<in> L r"
 shows "\<exists>v. lexer 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 (metis Posix_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(drule meta_mp)
 apply(simp add: der_correctness Der_def)
 apply(auto)
-by (metis PMatch2_roy_version)
+by (metis Posix2_roy_version)
 lemma lex_correct3a:
 shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer 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 (metis Posix_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(auto)
-apply(metis PMatch2_roy_version)
+apply(metis Posix2_roy_version)
 apply(simp add: der_correctness Der_def)
 using lex_correct1a
 apply fastforce
 apply(simp add: der_correctness Der_def)
 by (simp add: lex_correct1a)
 lemma lex_correct3b:
 shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. lexer 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 (metis Posix_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(simp add: der_correctness Der_def)
 apply(case_tac "lexer (der a r) s = None")
 apply(simp)
 apply(simp)
 apply(clarify)
 apply(rule iffI)
 apply(auto)
-apply(rule PMatch2_roy_version)
+apply(rule Posix2_roy_version)
 apply(simp)
-using PMatch1(1) by auto
+using Posix1(1) by auto
 section {* Lexer including simplifications *}
 fun F_RIGHT where

changeset 146	da81ffac4b10
parent 145	97735ef233be
child 149	ec3d221bfc45