# HG changeset patch
# User Chengsong
# Date 1649363881 -3600
# Node ID feacb89b784ca71e76a4ca9b4ed62c6532ee50f8
# Parent  574749f5190bc93d0b168be80a6d3c7cc13d83e6
christian's

diff -r 574749f5190b -r feacb89b784c thys2/BasicIdentities.thy
--- a/thys2/BasicIdentities.thy	Thu Apr 07 21:31:29 2022 +0100
+++ b/thys2/BasicIdentities.thy	Thu Apr 07 21:38:01 2022 +0100
@@ -93,9 +93,22 @@
   apply simp
   using distinct_not_exist by fastforce
 
+
 lemma distinct_rdistinct_append:
-  shows "distinct rs1 \<Longrightarrow> rdistinct (rs1 @ rsa) {} = rs1 @ (rdistinct rsa (set rs1))"
-  sorry
+  assumes "distinct rs1" "\<forall>r \<in> set rs1. r \<notin> acc"
+  shows "rdistinct (rs1 @ rsa) acc = rs1 @ (rdistinct rsa (acc \<union> set rs1))"
+  using assms
+  apply(induct rs1 arbitrary: rsa acc)
+   apply(auto)[1]
+  apply(auto)[1]
+  apply(drule_tac x="rsa" in meta_spec)
+  apply(drule_tac x="{a} \<union> acc" in meta_spec)
+  apply(simp)
+  apply(drule meta_mp)
+   apply(auto)[1]
+  apply(simp)
+  done
+  
 
 lemma rdistinct_concat_general:
   shows "rdistinct (rs1 @ rs2) {} = (rdistinct rs1 {}) @ (rdistinct rs2 (set rs1))"