Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/boolean_algebra_cancel.ML
changeset 70490 c42a0a0a9a8d
parent 67149 e61557884799 
--- a/src/HOL/Tools/boolean_algebra_cancel.ML	Thu Aug 08 11:40:42 2019 +0200
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML	Thu Aug 08 12:11:40 2019 +0200
@@ -13,27 +13,18 @@
 
 structure Boolean_Algebra_Cancel: BOOLEAN_ALGEBRA_CANCEL =
 struct
-val sup1 = @{lemma "(A::'a::semilattice_sup) == sup k a ==> sup A b == sup k (sup a b)"
-      by (simp only: ac_simps)}
-val sup2 = @{lemma "(B::'a::semilattice_sup) == sup k b ==> sup a B == sup k (sup a b)"
-      by (simp only: ac_simps)}
-val sup0 = @{lemma "(a::'a::bounded_semilattice_sup_bot) == sup a bot" by (simp)}
-
-val inf1 = @{lemma "(A::'a::semilattice_inf) == inf k a ==> inf A b == inf k (inf a b)"
-      by (simp only: ac_simps)}
-val inf2 = @{lemma "(B::'a::semilattice_inf) == inf k b ==> inf a B == inf k (inf a b)"
-      by (simp only: ac_simps)}
-val inf0 = @{lemma "(a::'a::bounded_semilattice_inf_top) == inf a top" by (simp)}
 
 fun move_to_front rule path = Conv.rewr_conv (Library.foldl (op RS) (rule, path))
 
 fun add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.sup\<close>, _) $ x $ y) =
     if sup then
-      add_atoms sup pos (sup1::path) x #> add_atoms sup pos (sup2::path) y
+      add_atoms sup pos (@{thm boolean_algebra_cancel.sup1}::path) x #>
+      add_atoms sup pos (@{thm boolean_algebra_cancel.sup2}::path) y
     else cons ((pos, t), path)
   | add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.inf\<close>, _) $ x $ y) =
     if not sup then
-      add_atoms sup pos (inf1::path) x #> add_atoms sup pos (inf2::path) y
+      add_atoms sup pos (@{thm boolean_algebra_cancel.inf1}::path) x #>
+      add_atoms sup pos (@{thm boolean_algebra_cancel.inf2}::path) y
     else cons ((pos, t), path)
   | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.bot\<close>, _)) = I
   | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.top\<close>, _)) = I
@@ -59,7 +50,8 @@
 
 fun cancel_conv sup rule ct =
   let
-    val rule0 = if sup then sup0 else inf0
+    val rule0 =
+      if sup then @{thm boolean_algebra_cancel.sup0} else @{thm boolean_algebra_cancel.inf0}
     fun cancel1_conv (pos, lpath, rpath) =
       let
         val lconv = move_to_front rule0 lpath
isabelle