diff -r 86e0203db2da -r 988e92a70704 thys4/posix/FBound.thy
--- a/thys4/posix/FBound.thy	Wed Aug 31 12:51:53 2022 +0100
+++ b/thys4/posix/FBound.thy	Wed Aug 31 23:57:42 2022 +0100
@@ -241,8 +241,8 @@
 | "AZERO \<le>1 ASEQ bs AZERO r" 
 | "AZERO \<le>1 ASEQ bs r AZERO"
 | "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"
-| " AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"
-| "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs1 (rsa @ (AALTs bs1 rs1) # rsb)"
+| "AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"
+| "AALTs bs (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs (rsa @ (AALTs bs1 rs1) # rsb)"
 | "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "
 | "r1 \<le>1 r2 \<Longrightarrow> r1  \<le>1 ASEQ bs (AONE bs1) r2"
 | "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"
@@ -252,6 +252,42 @@
 | "AZERO \<le>1 AALTs bs []"
 | "fuse bs r \<le>1 AALTs bs [r]"
 | "\<lbrakk>r1' \<le>1 r1;  r2' \<le>1 r2\<rbrakk> \<Longrightarrow> bsimp_ASEQ bs1 r1' r2' \<le>1 ASEQ bs1 r1 r2"
+| "\<lbrakk>AALTs bs rs1 \<le>1 AALTs bs rs2; r1 \<le>1 r2 \<rbrakk> \<Longrightarrow> AALTs bs (r1 # rs1) \<le>1 AALTs bs (r2 # rs2)"
+| "\<lbrakk>r1 \<le>1 r2; r2 \<le>1 r3 \<rbrakk> \<Longrightarrow> r1 \<le>1 r3"
+
+
+lemma leq1_6_variant1:
+  shows "AALTs bs ( (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs ((AALTs bs1 rs1) # rsb)"
+  by (metis leq1.intros(6) self_append_conv2)
+
+
+
+lemma flts_leq1:
+  shows "AALTs bs (flts rs) \<le>1 AALTs bs rs"
+  apply(induct rule: flts.induct)
+         apply (simp add: leq1.intros(1))
+        apply simp
+  apply (metis append_Nil leq1.intros(17) leq1.intros(5))
+       apply simp
+       apply(subgoal_tac "AALTs bs (map (fuse bsa) rs1 @ flts rs) \<le>1 AALTs bs (AALTs bsa rs1 # flts rs)")
+        apply (meson leq1.intros(1) leq1.intros(16) leq1.intros(17))
+  using leq1_6_variant1 apply presburger
+  apply (simp add: leq1.intros(1) leq1.intros(16))
+  using leq1.intros(1) leq1.intros(16) apply auto[1]
+  using leq1.intros(1) leq1.intros(16) apply force
+   apply (simp add: leq1.intros(1) leq1.intros(16))
+  using leq1.intros(1) leq1.intros(16) by force
+
+lemma dB_leq12:
+  shows "AALTs bs (distinctWith rs1 eq1 (set rs2)) \<le>1 AALTs bs (rs1 @ rs2)"
+  sorry
+
+
+lemma dB_leq1:
+  shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs"
+  by (metis append.right_neutral dB_leq12 list.set(1))
+
+
 
 lemma stupid_leq1_1:
   shows " rerase  r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))"
@@ -276,7 +312,8 @@
    apply(erule exE)
    apply simp
   apply (metis asize_rsize le_SucI rerase_fuse trans_le_add2)
-  by (smt (verit, best) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral add_cancel_right_right add_mono_thms_linordered_semiring(1) asize.simps(5) asize_rsize nat_add_left_cancel_le order.trans order_trans plus_1_eq_Suc rSEQ_mono rerase_bsimp_ASEQ rsize.simps(5))
+  apply (smt (verit, best) Suc_eq_plus1 ab_semigroup_add_class.add_ac(1) add.commute add.right_neutral add_cancel_right_right add_mono_thms_linordered_semiring(1) asize.simps(5) asize_rsize nat_add_left_cancel_le order.trans order_trans plus_1_eq_Suc rSEQ_mono rerase_bsimp_ASEQ rsize.simps(5))
+  sorry
 
 
 
@@ -316,9 +353,9 @@
   apply force
   apply simp
   apply(simp add: asize_rsize)
-  by (simp add: rerase_fuse size_deciding_equality4)
-
-  
+  apply (simp add: rerase_fuse size_deciding_equality4)
+  apply (metis Suc_n_not_le_n asize_rsize leq1.intros(15) leq1_size rsize.simps(5) trans_le_add2)
+  sorry
 
   
 
@@ -344,9 +381,11 @@
      apply simp
     apply simp
    apply simp
-  apply simp
-  using r_finite1 rerase_fuse by auto
+   apply simp
 
+  using r_finite1 rerase_fuse apply auto[1]
+  apply (smt (verit, best) BlexerSimp.bsimp_ASEQ0 BlexerSimp.bsimp_ASEQ2 bsimp_ASEQ.simps(1) bsimp_ASEQ1 leq1_trans1 rerase.simps(5) rerase_bsimp_ASEQ rerase_fuse rrexp.inject(2) rsimp_SEQ.simps(22))
+  sorry
 
 
 
@@ -419,7 +458,16 @@
   shows "bsimp r \<le>1 r"
   apply(induct rule: bsimp.induct)
         apply simp
+        apply (simp add: leq1.intros(15))
+       apply simp
+  apply(case_tac rs)
+        apply simp
   
+  apply (simp add: leq1.intros(13))
+       apply(case_tac list)
+        apply simp
+  
+
   sorry