Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hi
authorChengsong
Fri, 11 Mar 2022 23:32:44 +0000
changeset 448 3bc0f0069d06
parent 447 7fb1e3dd5ae6
child 449 09d7cd8e5ef8
hi
thys2/ClosedFormsBounds.thy file | annotate | diff | comparison | revisions 
--- a/thys2/ClosedFormsBounds.thy	Fri Mar 11 21:25:08 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Fri Mar 11 23:32:44 2022 +0000
@@ -115,10 +115,19 @@
   by (metis empty_iff flts_vs_nflts sup_bot_left)
 
 
+lemma distinct_simp_ineq_general:
+  shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
+    \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"
+  sorry
+
+
 lemma distinct_simp_ineq:
   shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))
     \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
-  sorry
+  
+  using distinct_simp_ineq_general by blast
+  
+
 
 
 lemma alts_simp_control:
lexing