diff -r 256484ef4be4 -r 8927b737936f thys/Positions.thy
--- a/thys/Positions.thy	Mon Jun 26 18:15:26 2017 +0100
+++ b/thys/Positions.thy	Mon Jun 26 18:40:58 2017 +0100
@@ -394,12 +394,11 @@
 apply(auto)
 done
 
+(*
 definition dpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" 
   where
   "dpos v1 v2 p \<equiv> (p \<in> Pos v1 \<union> Pos v2) \<and> (p \<notin> Pos v1 \<inter> Pos v2)"
-
-definition
-  "DPos v1 v2 \<equiv> {p. dpos v1 v2 p}"
+*)
 
 lemma outside_lemma:
   assumes "p \<notin> Pos v1 \<union> Pos v2"
@@ -408,6 +407,7 @@
 apply(auto simp add: pflat_len_def)
 done
 
+(*
 lemma dpos_lemma_aux:
   assumes "p \<in> Pos v1 \<union> Pos v2"
   and "pflat_len v1 p = pflat_len v2 p"
@@ -434,16 +434,7 @@
   shows "pflat_len v1 p \<noteq> pflat_len v2 p"
 using assms
 using dpos_lemma by blast
-
-lemma DPos_lemma:
-  assumes "p \<in> DPos v1 v2"
-  shows "pflat_len v1 p \<noteq> pflat_len v2 p"
-using assms
-unfolding DPos_def 
-apply(auto simp add: pflat_len_def dpos_def)
-apply (smt inlen_bigger)
-by (smt inlen_bigger)
-
+*)
 
 definition val_ord:: "val \<Rightarrow> nat list \<Rightarrow> val \<Rightarrow> bool" ("_ \<sqsubset>val _ _")
 where
@@ -804,36 +795,6 @@
 by (metis IntE Two_to_Three_aux UnCI lex_trans outside_lemma)
 
 
-definition fdpos :: "val \<Rightarrow> val \<Rightarrow> nat list \<Rightarrow> bool" 
-where
-  "fdpos v1 v2 p \<equiv>  ({q. q \<sqsubset>lex p} \<inter> DPos v1 v2 = {})"
-
-
-lemma pos_append:
-  assumes "p @ q \<in> Pos v"
-  shows "q \<in> Pos (at v p)"
-using assms
-apply(induct arbitrary: p q rule: Pos.induct) 
-apply(simp_all)
-apply(auto)[1]
-apply(simp add: append_eq_Cons_conv)
-apply(auto)[1]
-apply(auto)[1]
-apply(simp add: append_eq_Cons_conv)
-apply(auto)[1]
-apply(auto)[1]
-apply(simp add: append_eq_Cons_conv)
-apply(auto)[1]
-apply(simp add: append_eq_Cons_conv)
-apply(auto)[1]
-apply(auto)[1]
-apply(simp add: append_eq_Cons_conv)
-apply(auto)[1]
-apply(simp add: append_eq_Cons_conv)
-apply(auto)[1]
-by (metis append_Cons at.simps(6))
-
-
 lemma Pos_pre:
   assumes "p \<in> Pos v" "q \<sqsubseteq>pre p"
   shows "q \<in> Pos v"
@@ -991,15 +952,7 @@
 apply (simp add: prefix_list_def)
 by (metis L.simps(4) L_flat_Prf1 Prf.intros(1) Prf_CPrf flat.simps(5))
 
-lemma Cond_prefix:
-  assumes "\<forall>s\<^sub>3. s1 @ s\<^sub>3 \<in> L r1 \<longrightarrow> s\<^sub>3 = [] \<or> (\<forall>s\<^sub>4. s1 @ s\<^sub>3 @ s\<^sub>4 \<sqsubseteq>pre s1 @ s2 \<longrightarrow> s\<^sub>4 \<notin> L r2)"
-  and "t1 \<in> L r1" "t2 \<in> L r2" "t1 @ t2 \<sqsubseteq>pre s1 @ s2"
-  shows "t1 \<sqsubseteq>pre s1"
-using assms
-apply(auto simp add: Sequ_def prefix_list_def append_eq_append_conv2)
-done
-
-
+term "{vs. Stars vs \<in> A}"
 
 lemma test: 
   assumes "finite A"
@@ -1049,7 +1002,6 @@
 apply(simp)
 apply(rule finite_subset)
 apply(rule CPTpre_subsets)
-thm finite_subset
 apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2).  v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset)
 apply(auto)[1]
 apply(rule finite_imageI)