diff -r 80e1114d6421 -r 86e0203db2da thys4/posix/FBound.thy
--- a/thys4/posix/FBound.thy	Tue Aug 30 12:41:52 2022 +0100
+++ b/thys4/posix/FBound.thy	Wed Aug 31 12:51:53 2022 +0100
@@ -184,23 +184,8 @@
 
 thm bsimp_rerase
 
-lemma cant1:
-  shows "\<lbrakk> bsimp a = b; rerase a = rerase b; a = ASEQ bs r1 r2 \<rbrakk> \<Longrightarrow>
-        \<exists>bs' r1' r2'. b = ASEQ bs' r1' r2' \<and> rerase r1' = rerase r1 \<and> rerase r2' = rerase r2"
-  sorry
 
 
-
-(*"part is less than whole" thm for rrexp, since rrexp is always finite*)
-lemma rrexp_finite1:
-  shows "\<lbrakk> bsimp_ASEQ bs1 (bsimp ra1) (bsimp ra2) = ASEQ bs2 rb1 rb2; ra1 ~1 rb1; ra2 ~1 rb2 \<rbrakk> \<Longrightarrow> rerase ra1 = rerase (bsimp ra1) "
-  apply(case_tac ra1 )
-        apply simp+
-     apply(case_tac rb1)
-           apply simp+
-
-  sorry
-
 lemma unsure_unchanging:
   assumes "bsimp a = bsimp b"
 and "a ~1 b"
@@ -257,33 +242,115 @@
 | "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))"
-| "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"
 | "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs1 (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)"
+| "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r  r2 \<le>1 ASEQ bs r r1"
+| "r2 \<le>1 r1 \<Longrightarrow> ASEQ bs r2 r  \<le>1 ASEQ bs r1 r"
+| "r \<le>1 r' \<Longrightarrow> ASTAR bs r \<le>1 ASTAR bs r'"
+| "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"
+
+lemma stupid_leq1_1:
+  shows " rerase  r2 \<noteq> RSEQ r (RSEQ RONE (rerase r2))"
+  apply(induct r2)
+        apply simp+
+  done
+
+lemma leq1_size:
+  shows "r1 \<le>1 r2 \<Longrightarrow> asize r1 \<le> asize r2"
+  apply (induct rule: leq1.induct)
+               apply simp+
+  apply (metis asize_rsize le_SucI le_add2 plus_1_eq_Suc rerase_fuse)
+           apply simp
+          apply simp
+  
+          apply (metis (mono_tags, lifting) asize_rsize comp_apply dual_order.eq_iff le_SucI map_eq_conv rerase_fuse)
+  apply simp+
+  apply (metis Suc_n_not_le_n asize_rsize linorder_le_cases rerase_fuse)
+  apply(case_tac "r1' = AZERO")
+   apply simp
+  apply(case_tac "\<exists>bs1. r1' = AONE bs1")
+   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))
+
+
+
+lemma size_deciding_equality:
+  shows "asize r1 \<noteq> asize r2 \<Longrightarrow> r1 \<noteq> r2 "
+  apply auto
+  done
+
+lemma size_deciding_equality2:
+  shows "rerase r1 = rerase r2 \<Longrightarrow> asize r1 = asize r2"
+  by (metis asize_rsize)
+
+lemma size_deciding_equality3:
+  shows "asize r1 \<noteq> asize r2 \<Longrightarrow> rerase r1 \<noteq> rerase r2"
+  by (metis asize_rsize)
+
+lemma size_deciding_equality4:
+  shows "rerase a1 = r2 \<Longrightarrow> asize a1 = rsize r2"
+  by (metis asize_rsize)
+
+lemma size_deciding_equality5:
+  shows "asize a1 \<noteq> rsize r2 \<Longrightarrow>rerase a1 \<noteq> r2"
+  by (metis asize_rsize)
+
+lemma leq1_trans1:
+  shows " r1 \<le>1 r2 \<Longrightarrow>  rerase r1 \<noteq> RSEQ r (rerase r2)"
+  apply(induct rule: leq1.induct)
+               apply simp+
+  using rerase_fuse stupid_leq1_1 apply presburger
+           apply simp+
+        apply(subgoal_tac "asize r1 \<noteq> rsize (RSEQ r (RSEQ RONE (rerase r2)))")
+  using size_deciding_equality5 apply blast
+  using asize_rsize leq1_size apply fastforce
+       apply simp+
+  apply(subgoal_tac "rsize (rerase (fuse bs ra)) \<noteq> rsize (RSEQ r (RALTS [rerase ra]))")
+  
+  apply force
+  apply simp
+  apply(simp add: asize_rsize)
+  by (simp add: rerase_fuse size_deciding_equality4)
+
+  
+
+  
 
 lemma leq1_less_or_equal: shows
 "r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
   apply(induct rule: leq1.induct)
-          apply simp+
-  sorry
-
-lemma bsimp_leq1:
-  shows "bsimp r \<le>1 r"
-
-  sorry
+               apply simp
+              apply simp
+  apply simp
+            apply (simp add: rerase_fuse)
+           apply simp
+  apply simp
+  using r_finite1 rerase_fuse apply force
+         apply simp
+        apply simp
+        apply(case_tac "r1 = r2")
+         apply simp
+        apply simp
+  
+  using leq1_trans1 apply presburger
+       apply simp
+      apply simp
+     apply simp
+    apply simp
+   apply simp
+  apply simp
+  using r_finite1 rerase_fuse by auto
 
 
-lemma arexpfiniteaux4_aux:
-  shows" \<lbrakk>rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs) \<rbrakk>
-       \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
-  apply(induct rs)
-   apply simp
-  apply simp
-  apply auto
-   prefer 2
+
 
-  sorry
+
 
 lemma arexpfiniteaux4:
   shows"
@@ -348,6 +415,15 @@
 
 
 
+lemma bsimp_reduces:
+  shows "bsimp r \<le>1 r"
+  apply(induct rule: bsimp.induct)
+        apply simp
+  
+  sorry
+
+
+
 lemma bitcodes_unchanging:
   shows "\<lbrakk>bsimp a = b; rerase a = rerase b \<rbrakk> \<Longrightarrow> a = b"
   apply(induction a arbitrary: b)
@@ -376,6 +452,7 @@
   shows "bsimp (bsimp a) = bsimp a"
   using bitcodes_unchanging bsimp_rerase rsimp_idem by auto
 
+
 unused_thms
 
 end