--- a/thys2/ClosedFormsBounds.thy	Sat Mar 12 14:04:57 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Sat Mar 12 14:33:54 2022 +0000
@@ -51,12 +51,6 @@
 
   sorry
 
-lemma not_mentioned_elem_distinct:
-  shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs {})) = (r \<in> set (rdistinct rs {a}))"
-  sorry
-
-
-
 lemma flts_vs_nflts:
   shows "\<forall>r \<in> noalts_set. \<forall>xs. r \<noteq> RALTS xs
  \<and> (\<forall>a \<in> alts_set. \<exists>xs. a = RALTS xs \<and> set xs \<subseteq> corr_set)  
@@ -68,12 +62,39 @@
   sorry
 
 lemma distinct_simp_ineq_general:
-  shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
+  shows "rsimp ` no_simp = has_simp \<and> finite no_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
     \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"
+  apply(induct rs arbitrary: no_simp has_simp)
+   apply simp
+  apply(case_tac "a \<in> no_simp")
+  apply(subgoal_tac "rsimp a \<in> has_simp")
+    apply auto[1]
+  apply blast
+  apply(case_tac "rsimp a \<in> no_simp")
+   apply(subgoal_tac "rsimp a \<in> has_simp")
+  prefer 2
+  apply (simp add: rev_image_eqI rsimp_idem)
+  sledgehammer[timeout = 100]
 
   sorry
 
 
+lemma not_mentioned_elem_distinct_strong:
+  shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs rset)) = (r \<in> set (rdistinct rs (insert a rset)))"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  by force
+
+lemma not_mentioned_elem_distinct:
+  shows "r \<noteq> a \<Longrightarrow> (r \<in> set (rdistinct rs {})) = (r \<in> set (rdistinct rs (insert a {})))"
+  by (metis not_mentioned_elem_distinct_strong)
+
+
+
+
+
+
+
 lemma without_flts_ineq:
   shows " Suc (sum_list (map rsize (rdistinct (rflts rs) {}) )) \<le> 
          Suc (sum_list (map rsize (rdistinct (    rs  ) {}  )))"