diff -r d028c662a3df -r bc1df466150a thys4/posix/BasicIdentities.thy
--- a/thys4/posix/BasicIdentities.thy	Mon Oct 03 13:32:25 2022 +0100
+++ b/thys4/posix/BasicIdentities.thy	Tue Oct 04 00:25:09 2022 +0100
@@ -120,6 +120,71 @@
   by (simp add: rdistinct_set_equality1)
 
 
+lemma distinct_removes_middle:
+  shows  "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
+and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
+   apply(induct as arbitrary: rset rset1 ab as2 as3 a)
+     apply simp
+    apply simp
+   apply(case_tac "a \<in> rset")
+    apply simp
+    apply metis
+   apply simp
+   apply (metis insertI1)
+  apply(case_tac "a = ab")
+   apply simp
+   apply(case_tac "ab \<in> rset")
+    apply simp
+    apply presburger
+   apply (meson insertI1)
+  apply(case_tac "a \<in> rset")
+  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
+  apply(case_tac "ab \<in> rset")
+  apply simp
+   apply (meson insert_iff)
+  apply simp
+  by (metis insertI1)
+
+lemma distinct_removes_middle3:
+  shows  "\<lbrakk>a \<in> set as\<rbrakk>
+    \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
+  using distinct_removes_middle(1) by fastforce
+
+lemma last_elem_out:
+  shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
+  apply(induct xs arbitrary: rset)
+  apply simp+
+  done
+
+
+
+
+lemma rdistinct_concat_general:
+  shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
+  apply(induct rs1 arbitrary: rs2 rule: rev_induct)
+   apply simp
+  apply(drule_tac x = "x # rs2" in meta_spec)
+  apply simp
+  apply(case_tac "x \<in> set xs")
+   apply simp
+  
+   apply (simp add: distinct_removes_middle3 insert_absorb)
+  apply simp
+  by (simp add: last_elem_out)
+
+
+lemma distinct_once_enough:
+  shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
+  apply(subgoal_tac "distinct (rdistinct rs {})")
+   apply(subgoal_tac 
+" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
+  apply(simp only:)
+  using rdistinct_concat_general apply blast
+  apply (simp add: distinct_rdistinct_append rdistinct_set_equality1)
+  by (simp add: rdistinct_does_the_job)
+  
+
 fun rflts :: "rrexp list \<Rightarrow> rrexp list"
   where 
   "rflts [] = []"
@@ -923,37 +988,8 @@
   by (metis append_Cons insert_iff insert_is_Un rdistinct.simps(2))
 
 
-lemma distinct_removes_middle:
-  shows  "\<lbrakk>a \<in> set as\<rbrakk>
-    \<Longrightarrow> rdistinct (as @ as2) rset = rdistinct (as @ [a] @ as2) rset"
-and "rdistinct (ab # as @ [ab] @ as3) rset1 = rdistinct (ab # as @ as3) rset1"
-   apply(induct as arbitrary: rset rset1 ab as2 as3 a)
-     apply simp
-    apply simp
-   apply(case_tac "a \<in> rset")
-    apply simp
-    apply metis
-   apply simp
-   apply (metis insertI1)
-  apply(case_tac "a = ab")
-   apply simp
-   apply(case_tac "ab \<in> rset")
-    apply simp
-    apply presburger
-   apply (meson insertI1)
-  apply(case_tac "a \<in> rset")
-  apply (metis (no_types, opaque_lifting) Un_insert_left append_Cons insert_iff rdistinct.simps(2) sup_bot_left)
-  apply(case_tac "ab \<in> rset")
-  apply simp
-   apply (meson insert_iff)
-  apply simp
-  by (metis insertI1)
 
 
-lemma distinct_removes_middle3:
-  shows  "\<lbrakk>a \<in> set as\<rbrakk>
-    \<Longrightarrow> rdistinct (as @ a #as2) rset = rdistinct (as @ as2) rset"
-  using distinct_removes_middle(1) by fastforce
 
 
 lemma distinct_removes_list:
@@ -1038,41 +1074,9 @@
    apply (metis append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims)
    by (metis (no_types, opaque_lifting) append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims)
 
-lemma last_elem_out:
-  shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
-  apply(induct xs arbitrary: rset)
-  apply simp+
-  done
-
 
 
 
-lemma rdistinct_concat_general:
-  shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"
-  apply(induct rs1 arbitrary: rs2 rule: rev_induct)
-   apply simp
-  apply(drule_tac x = "x # rs2" in meta_spec)
-  apply simp
-  apply(case_tac "x \<in> set xs")
-   apply simp
-  
-   apply (simp add: distinct_removes_middle3 insert_absorb)
-  apply simp
-  by (simp add: last_elem_out)
-
-
-  
-
-lemma distinct_once_enough:
-  shows "rdistinct (rs @ rsa) {} = rdistinct (rdistinct rs {} @ rsa) {}"
-  apply(subgoal_tac "distinct (rdistinct rs {})")
-   apply(subgoal_tac 
-" rdistinct (rdistinct rs {} @ rsa) {} = rdistinct rs {} @ (rdistinct rsa (set rs))")
-  apply(simp only:)
-  using rdistinct_concat_general apply blast
-  apply (simp add: distinct_rdistinct_append rdistinct_set_equality1)
-  by (simp add: rdistinct_does_the_job)
-  
 
 lemma simp_flatten:
   shows "rsimp (RALTS ((RALTS rsa) # rsb)) = rsimp (RALTS (rsa @ rsb))"