# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1498755461 -3600
# Node ID 146b4817aebdc3cd7ce7631d27681d4fb727c8d5
# Parent  222ed43892ea1e71f6e511ae70d188c871c0c0ba
updated

diff -r 222ed43892ea -r 146b4817aebd thys/Lexer.thy
--- a/thys/Lexer.thy	Wed Jun 28 10:37:05 2017 +0100
+++ b/thys/Lexer.thy	Thu Jun 29 17:57:41 2017 +0100
@@ -13,12 +13,12 @@
 
 text {* Two Simple Properties about Sequential Composition *}
 
-lemma seq_empty [simp]:
+lemma Sequ_empty_string [simp]:
   shows "A ;; {[]} = A"
   and   "{[]} ;; A = A"
 by (simp_all add: Sequ_def)
 
-lemma seq_null [simp]:
+lemma Sequ_empty [simp]:
   shows "A ;; {} = {}"
   and   "{} ;; A = {}"
 by (simp_all add: Sequ_def)
@@ -71,12 +71,14 @@
   start[intro]: "[] \<in> A\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
 
-lemma star_cases:
+(* Arden's lemma *)
+
+lemma Star_cases:
   shows "A\<star> = {[]} \<union> A ;; A\<star>"
 unfolding Sequ_def
 by (auto) (metis Star.simps)
 
-lemma star_decomp: 
+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
@@ -87,14 +89,14 @@
   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
 proof -    
   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"  
-    by (simp only: star_cases[symmetric])
+    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)
+    by (auto dest: Star_decomp)
   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
 qed
 
@@ -291,12 +293,14 @@
 
 
 lemma L_flat_Prf1:
-  assumes "\<turnstile> v : r" shows "flat v \<in> L r"
+  assumes "\<turnstile> v : r" 
+  shows "flat v \<in> L r"
 using assms
 by (induct)(auto simp add: Sequ_def)
 
 lemma L_flat_Prf2:
-  assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
+  assumes "s \<in> L r" 
+  shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 using assms
 apply(induct r arbitrary: s)
 apply(auto simp add: Sequ_def intro: Prf.intros)
@@ -324,7 +328,6 @@
 using assms
 apply(drule_tac Star_string)
 apply(auto)
-
 by (metis L_flat_Prf2 Prf_Stars Star_val)
 
 
diff -r 222ed43892ea -r 146b4817aebd thys/Positions.thy
--- a/thys/Positions.thy	Wed Jun 28 10:37:05 2017 +0100
+++ b/thys/Positions.thy	Thu Jun 29 17:57:41 2017 +0100
@@ -55,6 +55,17 @@
 by (induct xs arbitrary: ys) (auto)
 
 lemma intlen_length:
+  shows "intlen xs < intlen ys \<longleftrightarrow> length xs < length ys"
+apply(induct xs arbitrary: ys)
+apply(auto)
+apply(case_tac ys)
+apply(simp_all)
+apply (smt intlen_bigger)
+(* HERE *)
+oops
+
+
+lemma intlen_length:
   assumes "length xs < length ys"
   shows "intlen xs < intlen ys"
 using assms
@@ -185,6 +196,9 @@
 where
   "v1 :\<sqsubset>val v2 \<equiv> (\<exists>p. v1 \<sqsubset>val p v2)"
 
+
+
+
 definition val_ord_ex1:: "val \<Rightarrow> val \<Rightarrow> bool" ("_ :\<sqsubseteq>val _")
 where
   "v1 :\<sqsubseteq>val v2 \<equiv> v1 :\<sqsubset>val v2 \<or> v1 = v2"
@@ -219,6 +233,7 @@
 by (metis append_eq_conv_conj le_less_linear prefix_list_def sprefix_list_def take_all)
 
 
+
 lemma val_ord_LeftI:
   assumes "v :\<sqsubset>val v'" "flat v = flat v'"
   shows "(Left v) :\<sqsubset>val (Left v')" 
@@ -501,6 +516,49 @@
 apply(auto)[1]
 by (smt intlen_bigger lex_trans outside_lemma pflat_len_def)
 
+lemma val_ord_irrefl:
+  assumes "v :\<sqsubset>val v"
+  shows "False"
+using assms
+by(auto simp add: val_ord_ex_def val_ord_def)
+
+lemma val_ord_almost_trichotomous:
+  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (intlen (flat v1) = intlen (flat v2))"
+apply(auto simp add: val_ord_ex_def)
+apply(auto simp add: val_ord_def)
+apply(rule_tac x="[]" in exI)
+apply(auto simp add: Pos_empty pflat_len_simps)
+apply(drule_tac x="[]" in spec)
+apply(auto simp add: Pos_empty pflat_len_simps)
+done
+
+lemma WW1:
+  assumes "v1 :\<sqsubset>val v2" "v2 :\<sqsubset>val v1"
+  shows "False"
+using assms
+apply(auto simp add: val_ord_ex_def val_ord_def)
+using assms(1) assms(2) val_ord_irrefl val_ord_trans by blast
+
+lemma WW2:
+  assumes "\<not>(v1 :\<sqsubset>val v2)" 
+  shows "v1 = v2 \<or> v2 :\<sqsubset>val v1"
+using assms
+oops
+
+lemma val_ord_SeqE2:
+  assumes "(Seq v1 v2) :\<sqsubset>val (Seq v1' v2')" 
+  shows "v1 :\<sqsubset>val v1' \<or> (v1 = v1' \<and> v2 :\<sqsubset>val v2')"
+using assms 
+apply(frule_tac val_ord_SeqE)
+apply(erule disjE)
+apply(simp)
+apply(auto)
+apply(case_tac "v1 :\<sqsubset>val v1'")
+apply(simp)
+apply(auto simp add: val_ord_ex_def)
+apply(case_tac "v1 = v1'")
+apply(simp)
+oops
 
 section {* CPT and CPTpre *}
 
@@ -522,6 +580,62 @@
 using assms
 by (induct) (auto intro: Prf.intros)
 
+lemma pflat_len_equal_iff:
+  assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
+  and "\<forall>p. pflat_len v1 p = pflat_len v2 p"
+  shows "v1 = v2"
+using assms
+apply(induct v1 r arbitrary: v2 rule: CPrf.induct)
+apply(rotate_tac 4)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis pflat_len_simps(1) pflat_len_simps(2))
+apply(rotate_tac 2)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis pflat_len_simps(3))
+apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
+apply(rotate_tac 2)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis intlen.simps(1) intlen_length length_greater_0_conv list.size(3) neg_0_le_iff_le not_less not_less_iff_gr_or_eq not_one_le_zero pflat_len_simps(3) pflat_len_simps(6) pflat_len_simps(9))
+apply (metis pflat_len_simps(5))
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv neq_Nil_conv not_less_iff_gr_or_eq pflat_len_simps(9))
+apply(rotate_tac 5)
+apply(erule CPrf.cases)
+apply(simp_all)[7]
+apply (metis append_Cons flat.simps(6) flat.simps(7) intlen_length length_greater_0_conv list.distinct(1) list.exhaust not_less_iff_gr_or_eq pflat_len_simps(9))
+apply(auto)
+apply (metis pflat_len_simps(8))
+apply(subgoal_tac "v = va")
+prefer 2
+apply (metis pflat_len_simps(8))
+apply(simp)
+apply(rotate_tac 3)
+apply(drule_tac x="Stars vsa" in meta_spec)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(rule allI)
+apply(case_tac p)
+apply(simp add: pflat_len_simps)
+apply(drule_tac x="[]" in spec)
+apply(simp add: pflat_len_simps intlen_append)
+apply(drule_tac x="Suc a#list" in spec)
+apply(simp add: pflat_len_simps intlen_append)
+apply(simp)
+done
+
+lemma val_ord_trichotomous_stronger:
+  assumes "\<Turnstile> v1 : r" "\<Turnstile> v2 : r"
+  shows "v1 :\<sqsubset>val v2 \<or> v2 :\<sqsubset>val v1 \<or> (v1 = v2)"
+oops
+
 lemma CPrf_stars:
   assumes "\<Turnstile> Stars vs : STAR r"
   shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r"
diff -r 222ed43892ea -r 146b4817aebd thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Wed Jun 28 10:37:05 2017 +0100
+++ b/thys/Sulzmann.thy	Thu Jun 29 17:57:41 2017 +0100
@@ -118,6 +118,10 @@
 apply(simp)
 oops
 
+lemma QQ: 
+  shows "x \<le> (y::nat) \<longleftrightarrow> x = y \<or> x < y"
+  by auto
+
 lemma Posix_CPT2:
   assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s"
   shows "v1 \<prec> v2"
@@ -149,10 +153,13 @@
 apply(erule CPrf.cases)
 apply(simp_all)[7]
 apply(clarify)
+apply(frule val_ord_shorterE)
+apply(subst (asm) QQ)
+apply(erule disjE)
 apply(drule val_ord_SeqE)
 apply(erule disjE)
 apply(drule_tac x="v1a" in meta_spec)
-apply(rotate_tac 7)
+apply(rotate_tac 8)
 apply(drule_tac x="v1b" in meta_spec)
 apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec)
 apply(simp)
@@ -160,7 +167,19 @@
 apply(auto simp add: CPTpre_def)[1]
 apply(drule meta_mp)
 apply(auto simp add: CPTpre_def)[1]
+apply(rule ValOrd.intros(2))
+apply(assumption)
+apply(frule val_ord_shorterE)
+apply(subst (asm) append_eq_append_conv_if)
+apply(simp)
+apply (metis append_assoc append_eq_append_conv_if length_append)
+
+
+thm le
+apply(clarify)
 apply(rule ValOrd.intros)
+apply(simp)
+
 apply(subst (asm) (3) CPTpre_def)
 apply(subst (asm) (3) CPTpre_def)
 apply(auto)[1]