diff -r b90ff5abb437 -r 256484ef4be4 thys/Positions.thy
--- a/thys/Positions.thy	Mon Jun 26 17:43:28 2017 +0100
+++ b/thys/Positions.thy	Mon Jun 26 18:15:26 2017 +0100
@@ -13,20 +13,6 @@
 | "at (Seq v1 v2) (Suc 0#ps)= at v2 ps"
 | "at (Stars vs) (n#ps)= at (nth vs n) ps"
 
-(*
-fun 
-  ato :: "val \<Rightarrow> nat list \<Rightarrow> val option"
-where
-  "ato v [] = Some v"
-| "ato (Left v) (0#ps)= ato v ps"
-| "ato (Right v) (Suc 0#ps)= ato v ps"
-| "ato (Seq v1 v2) (0#ps)= ato v1 ps"
-| "ato (Seq v1 v2) (Suc 0#ps)= ato v2 ps"
-| "ato (Stars vs) (n#ps)= (if (n < length vs) then ato (nth vs n) ps else None)"
-| "ato v p = None"
-*)
-
-
 fun Pos :: "val \<Rightarrow> (nat list) set"
 where
   "Pos (Void) = {[]}"
@@ -43,46 +29,6 @@
 apply(auto)
 done
 
-lemma Pos_finite_aux:
-  assumes "\<forall>v \<in> set vs. finite (Pos v)"
-  shows "finite (Pos (Stars vs))"
-using assms
-apply(induct vs)
-apply(simp)
-apply(simp)
-apply(subgoal_tac "finite (Pos (Stars vs) - {[]})")
-apply(rule_tac f="\<lambda>l. Suc (hd l) # tl l" in finite_surj)
-apply(assumption)
-back
-apply(auto simp add: image_def)
-apply(rule_tac x="n#ps" in bexI)
-apply(simp)
-apply(simp)
-done
-
-lemma Pos_finite:
-  shows "finite (Pos v)"
-apply(induct v rule: val.induct)
-apply(auto)
-apply(simp add: Pos_finite_aux)
-done
-
-(*
-lemma ato_test:
-  assumes "p \<in> Pos v"
-  shows "\<exists>v'. ato v p = Some v'"
-using assms
-apply(induct v arbitrary: p rule: Pos.induct)
-apply(auto)
-apply force
-by (metis ato.simps(6) option.distinct(1))
-*)
-
-
-definition pflat :: "val \<Rightarrow> nat list => string option"
-where
-  "pflat v p \<equiv> (if p \<in> Pos v then Some (flat (at v p)) else None)"
-
 fun intlen :: "'a list \<Rightarrow> int"
 where
   "intlen [] = 0"
@@ -157,11 +103,6 @@
 apply (smt inlen_bigger)+
 done
 
-lemma Two_to_Three:
-  assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat v1 p = pflat v2 p"
-  shows "Pos v1 = Pos v2"
-using assms
-by (metis Un_iff option.distinct(1) pflat_def subsetI subset_antisym)
 
 lemma Two_to_Three_orig:
   assumes "\<forall>p \<in> Pos v1 \<union> Pos v2. pflat_len v1 p = pflat_len v2 p"
@@ -169,20 +110,6 @@
 using assms
 by (metis Un_iff inlen_bigger neg_0_le_iff_le not_one_le_zero pflat_len_def subsetI subset_antisym)
 
-lemma set_eq1:
-  assumes "insert [] A = insert [] B" "[] \<notin> A"  "[] \<notin> B"
-  shows "A = B"
-using assms
-by (simp add: insert_ident)
-
-lemma set_eq2:
-  assumes "A \<union> B = A \<union> C"
-  and "A \<inter> B = {}" "A \<inter> C = {}"  
-  shows "B = C"
-using assms
-using Un_Int_distrib sup_bot.left_neutral sup_commute by blast
-
-
 
 lemma Three_to_One:
   assumes "\<turnstile> v1 : r" "\<turnstile> v2 : r" 
@@ -1847,4 +1774,6 @@
 apply(auto simp add: PT_def)
 done
 
+unused_thms
+
 end
\ No newline at end of file