# HG changeset patch
# User Chengsong
# Date 1656067265 -3600
# Node ID 3ea82d8f0aa4a8813ca722ef03f4e5bde5670d98
# Parent  1243a031966cd36303fe39091d579cac988be97e
start of day

diff -r 1243a031966c -r 3ea82d8f0aa4 thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Thu Jun 23 21:04:43 2022 +0100
+++ b/thys3/BlexerSimp.thy	Fri Jun 24 11:41:05 2022 +0100
@@ -252,9 +252,35 @@
   using assms
   by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
 
+(*harmless sorry*)
+lemma existing_preimage :
+  shows "f a \<in> f ` set rs1 \<Longrightarrow> \<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> f x = f a "
+  apply(induct rs1)
+   apply simp
+  apply(case_tac "f a = f aa")
+  
+  sorry
+
+
+lemma deletes_dB:
+  shows " \<lbrakk>erase a \<in> erase ` set rs1\<rbrakk> \<Longrightarrow> (rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)"
+  apply(subgoal_tac "\<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> erase x = erase a")
+  prefer 2
+
+
+  sorry
+
 lemma ss6_stronger_aux:
   shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))"
   apply(induct rs2 arbitrary: rs1)
+   apply simp
+  apply(case_tac "erase a \<in> erase ` set rs1")
+   apply(simp)
+   apply(drule_tac x = "rs1" in meta_spec)
+  apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)")
+  using srewrites_trans apply blast
+  using deletes_dB apply presburger
+
   apply(auto)
   prefer 2
   apply(drule_tac x="rs1 @ [a]" in meta_spec)