# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1458004238 0
# Node ID 5a1196466a9cfa21b52593cc0d41a2184fa284f2
# Parent  09f81fee11ce20c7086387dd94f34e21e8609a21
updated

diff -r 09f81fee11ce -r 5a1196466a9c thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Mon Mar 14 23:08:58 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 15 01:10:38 2016 +0000
@@ -744,8 +744,8 @@
 
   \begin{theorem}\mbox{}\smallskip\\
   \begin{tabular}{ll}
-  (1) & @{thm (lhs) lex_correct1a} if and only if @{thm (rhs) lex_correct1a}\\
-  (2) & @{thm (lhs) lex_correct3b} if and only if @{thm (rhs) lex_correct3b}\\
+  (1) & @{thm (lhs) lexer_correct_None} if and only if @{thm (rhs) lexer_correct_None}\\
+  (2) & @{thm (lhs) lexer_correct_Some} if and only if @{thm (rhs) lexer_correct_Some}\\
   \end{tabular}
   \end{theorem}
 
diff -r 09f81fee11ce -r 5a1196466a9c thys/ReStar.thy
--- a/thys/ReStar.thy	Mon Mar 14 23:08:58 2016 +0000
+++ b/thys/ReStar.thy	Tue Mar 15 01:10:38 2016 +0000
@@ -342,17 +342,17 @@
 inductive 
   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> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
+  Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
+| Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
+| Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
+| Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
+| Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
     \<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 r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> 
     (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
-| "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
+| Posix_STAR1: "\<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 []"
+| Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
 
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
@@ -389,178 +389,73 @@
 apply(auto)
 done
 
-(*
-lemma Posix_determ:
-  assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
-  shows "v1 = v2"
-using assms
-
-
-
-proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
-  case (1 v2)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: Posix.induct)
-apply(erule Posix.cases)
-apply(simp_all)[7]
-apply(erule Posix.cases)
-apply(simp_all)[7]
-apply(rotate_tac 2)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply(force)
-apply(clarify)
-apply(drule Posix1(1))
-apply(simp)
-apply(rotate_tac 3)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(drule Posix1(1))+
-apply(simp)
-apply(simp)
-apply(rotate_tac 5)
-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 Posix1(1) append_self_conv)
-apply(rotate_tac 6)
-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) Posix1(1) append_self_conv)
-apply(clarify)
-apply(rotate_tac 2)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-using Posix1(2) apply auto[1]
-using Posix1(2) apply blast
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply (simp add: Posix1(2))
-apply(simp)
-done
-  then have "[] \<in> ONE \<rightarrow> v2" by simp
-  then show "Void = v2"
-  apply(auto: elim Posix_elims)[1]  
-
-apply(erule Posix.cases)
-apply(simp_all)[7]
-apply(erule Posix.cases)
-apply(simp_all)[7]
-apply(rotate_tac 2)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply(force)
-apply(clarify)
-apply(drule Posix1(1))
-apply(simp)
-apply(rotate_tac 3)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(drule Posix1(1))+
-apply(simp)
-apply(simp)
-apply(rotate_tac 5)
-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 Posix1(1) append_self_conv)
-apply(rotate_tac 6)
-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) Posix1(1) append_self_conv)
-apply(clarify)
-apply(rotate_tac 2)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-using Posix1(2) apply auto[1]
-using Posix1(2) apply blast
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply (simp add: Posix1(2))
-apply(simp)
-done
-*)
 
 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: Posix.induct)
-apply(erule Posix.cases)
-apply(simp_all)[7]
-apply(erule Posix.cases)
-apply(simp_all)[7]
-apply(rotate_tac 2)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply(force)
-apply(clarify)
-apply(drule Posix1(1))
-apply(simp)
-apply(rotate_tac 3)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(drule Posix1(1))+
-apply(simp)
-apply(simp)
-apply(rotate_tac 5)
-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 Posix1(1) append_self_conv)
-apply(rotate_tac 6)
-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) Posix1(1) append_self_conv)
-apply(clarify)
-apply(rotate_tac 2)
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-using Posix1(2) apply auto[1]
-using Posix1(2) apply blast
-apply(erule Posix.cases)
-apply(simp_all (no_asm_use))[7]
-apply(clarify)
-apply (simp add: Posix1(2))
-apply(simp)
-done
+proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
+  case (Posix_ONE v2)
+  have "[] \<in> ONE \<rightarrow> v2" by fact
+  then show "Void = v2" by cases auto
+next 
+  case (Posix_CHAR c v2)
+  have "[c] \<in> CHAR c \<rightarrow> v2" by fact
+  then show "Char c = v2" by cases auto
+next 
+  case (Posix_ALT1 s r1 v r2 v2)
+  have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
+  moreover
+  have "s \<in> r1 \<rightarrow> v" by fact
+  then have "s \<in> L r1" by (simp add: Posix1)
+  ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto 
+  moreover
+  have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
+  ultimately have "v = v'" by simp
+  then show "Left v = v2" using eq by simp
+next 
+  case (Posix_ALT2 s r2 v r1 v2)
+  have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
+  moreover
+  have "s \<notin> L r1" by fact
+  ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" 
+    by cases (auto simp add: Posix1) 
+  moreover
+  have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
+  ultimately have "v = v'" by simp
+  then show "Right v = v2" using eq by simp
+next
+  case (Posix_SEQ s1 r1 v1 s2 r2 v2 v')
+  have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" 
+       "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2"
+       "\<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 r1 \<and> s\<^sub>4 \<in> L r2)" by fact+
+  then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+  using Posix1(1) by fastforce+
+  moreover
+  have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"
+            "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+
+  ultimately show "Seq v1 v2 = v'" by simp
+next
+  case (Posix_STAR1 s1 r v s2 vs v2)
+  have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" 
+       "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))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+  using Posix1(1) apply fastforce
+  apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2)
+  using Posix1(2) by blast
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto
+next
+  case (Posix_STAR2 r v2)
+  have "[] \<in> STAR r \<rightarrow> v2" by fact
+  then show "Stars [] = v2" by cases (auto simp add: Posix1)
+qed
+
 
 (* a proof that does not need proj *)
 lemma Posix2_roy_version:
@@ -724,18 +619,7 @@
                   | Some(v) \<Rightarrow> Some(injval r c v))"
 
 
-
-lemma lex_correct1:
-  assumes "s \<notin> L r"
-  shows "lexer r s = None"
-using assms
-apply(induct s arbitrary: r)
-apply(simp add: nullable_correctness)
-apply(drule_tac x="der a r" in meta_spec)
-apply(auto simp add: der_correctness Der_def)
-done
-
-lemma lex_correct1a:
+lemma lexer_correct_None:
   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
 using assms
 apply(induct s arbitrary: r)
@@ -744,68 +628,16 @@
 apply(auto simp add: der_correctness Der_def)
 done
 
-lemma lex_correct2:
-  assumes "s \<in> L r"
-  shows "\<exists>v. lexer r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
-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: der_correctness Der_def)
-apply(auto)
-apply (metis Prf_injval)
-apply(rule Prf_injval_flat)
-by simp
-
-lemma lex_correct3:
-  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 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 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 Posix_mkeps nullable_correctness)
-apply(drule_tac x="der a r" in meta_spec)
-apply(auto)
-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:
+lemma lexer_correct_Some:
   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 Posix_mkeps nullable_correctness)
+apply(auto simp add: Posix_mkeps nullable_correctness)[1]
 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 Posix2_roy_version)
-apply(simp)
-using Posix1(1) by auto
-
-
+apply(auto intro: Posix2_roy_version simp add: Posix1(1))
+done 
 
 
 end
\ No newline at end of file
diff -r 09f81fee11ce -r 5a1196466a9c thys/Simplifying.thy
--- a/thys/Simplifying.thy	Mon Mar 14 23:08:58 2016 +0000
+++ b/thys/Simplifying.thy	Tue Mar 15 01:10:38 2016 +0000
@@ -288,7 +288,7 @@
 apply(blast)
 prefer 2
 apply(auto)[1]
-apply (metis L_fst_simp Posix_elims(2) lex_correct3a)
+apply (metis L_fst_simp Posix_elims(2) lexer_correct_Some)
 apply(subst Posix_simp_nullable)
 using Posix.intros(1) Posix1(1) nullable_correctness apply blast
 apply(simp)
@@ -313,9 +313,9 @@
 apply(simp)
 apply(simp)
 apply(auto split: option.split prod.split)
-apply (metis L_fst_simp fst_conv lex_correct1a)
-using L_fst_simp lex_correct1a apply fastforce
-by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv)
+apply (metis L_fst_simp fst_conv lexer_correct_None)
+using L_fst_simp lexer_correct_None apply fastforce
+by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv)
 
 
 
diff -r 09f81fee11ce -r 5a1196466a9c thys/paper.pdf
Binary file thys/paper.pdf has changed