--- a/NEWS Fri Jan 17 20:30:01 2025 +0100
+++ b/NEWS Fri Jan 17 21:30:08 2025 +0100
@@ -235,6 +235,9 @@
types by target-language operations; this is also used by
HOL-Library.Code_Target_Numeral.
+* Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic rewrites certain
+arithmetic operations on numerals to bit shifts.
+
* Sledgehammer:
- Update of bundled provers:
. E 3.1 -- with patch on Windows/Cygwin for proper interrupts
--- a/etc/options Fri Jan 17 20:30:01 2025 +0100
+++ b/etc/options Fri Jan 17 21:30:08 2025 +0100
@@ -234,6 +234,9 @@
option build_schedule_inactive_delay : real = 300.0
-- "delay removing inactive hosts"
+option build_schedule_history : int = 150
+ -- "length of history relevant for scheduling (in days)"
+
section "Build Manager"
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jan 17 21:30:08 2025 +0100
@@ -322,7 +322,7 @@
shows "P a"
by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
-lemma suc_underS:
+lemma suc_underS':
assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
shows "b \<in> underS (suc B)"
using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy Fri Jan 17 21:30:08 2025 +0100
@@ -26,163 +26,4 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
- by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in GHC
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
- by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in GHC
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
- by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in GHC
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
- by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in GHC
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
- by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in GHC
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
- by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in GHC
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
- by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in GHC
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
- by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in GHC
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
- by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in GHC
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
- by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in GHC
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
- by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in GHC
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in GHC
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
- by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in GHC
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in GHC
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
- by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in GHC
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
- by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in GHC
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
- by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in GHC
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in GHC
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
- by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in GHC
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
- by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in GHC
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in GHC
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in GHC
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
- by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in GHC
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
- by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in GHC
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in GHC
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in GHC
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
- by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in GHC
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
- by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in GHC
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in GHC
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in GHC
-
end
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy Fri Jan 17 21:30:08 2025 +0100
@@ -26,163 +26,4 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in OCaml
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
- by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in OCaml
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
- by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in OCaml
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
- by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in OCaml
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
- by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in OCaml
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
- by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in OCaml
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
- by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in OCaml
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
- by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in OCaml
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
- by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in OCaml
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
- by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in OCaml
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
- by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in OCaml
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
- by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in OCaml
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in OCaml
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
- by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in OCaml
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in OCaml
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
- by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in OCaml
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
- by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in OCaml
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
- by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in OCaml
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in OCaml
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
- by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in OCaml
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
- by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in OCaml
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in OCaml
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in OCaml
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
- by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in OCaml
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
- by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in OCaml
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in OCaml
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in OCaml
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
- by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in OCaml
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
- by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in OCaml
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in OCaml
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in OCaml
-
end
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy Fri Jan 17 21:30:08 2025 +0100
@@ -16,163 +16,4 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
- by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in PolyML
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
- by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in PolyML
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
- by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in PolyML
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
- by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in PolyML
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
- by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in PolyML
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
- by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in PolyML
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
- by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in PolyML
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
- by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in PolyML
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
- by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in PolyML
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
- by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in PolyML
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
- by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in PolyML
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in PolyML
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
- by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in PolyML
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in PolyML
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
- by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in PolyML
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
- by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in PolyML
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
- by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in PolyML
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in PolyML
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
- by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in PolyML
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
- by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in PolyML
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in PolyML
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in PolyML
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
- by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in PolyML
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
- by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in PolyML
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in PolyML
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in PolyML
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
- by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in PolyML
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
- by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in PolyML
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in PolyML
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in PolyML
-
end
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy Fri Jan 17 21:30:08 2025 +0100
@@ -26,163 +26,4 @@
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala
-text \<open>Test cases for bit operations on target language numerals\<close>
-
-unbundle bit_operations_syntax
-
-lemma \<open>bit (473514 :: integer) 5\<close>
- by normalization
-
-test_code \<open>bit (473514 :: integer) 5\<close> in Scala
-
-lemma \<open>bit (- 805167 :: integer) 7\<close>
- by normalization
-
-test_code \<open>bit (- 805167 :: integer) 7\<close> in Scala
-
-lemma \<open>473514 AND (767063 :: integer) = 208898\<close>
- by normalization
-
-test_code \<open>473514 AND (767063 :: integer) = 208898\<close> in Scala
-
-lemma \<open>- 805167 AND (767063 :: integer) = 242769\<close>
- by normalization
-
-test_code \<open>- 805167 AND (767063 :: integer) = 242769\<close> in Scala
-
-lemma \<open>473514 AND (- 314527 :: integer) = 209184\<close>
- by normalization
-
-test_code \<open>473514 AND (- 314527 :: integer) = 209184\<close> in Scala
-
-lemma \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close>
- by normalization
-
-test_code \<open>- 805167 AND (- 314527 :: integer) = - 839103\<close> in Scala
-
-lemma \<open>473514 OR (767063 :: integer) = 1031679\<close>
- by normalization
-
-test_code \<open>473514 OR (767063 :: integer) = 1031679\<close> in Scala
-
-lemma \<open>- 805167 OR (767063 :: integer) = - 280873\<close>
- by normalization
-
-test_code \<open>- 805167 OR (767063 :: integer) = - 280873\<close> in Scala
-
-lemma \<open>473514 OR (- 314527 :: integer) = - 50197\<close>
- by normalization
-
-test_code \<open>473514 OR (- 314527 :: integer) = - 50197\<close> in Scala
-
-lemma \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close>
- by normalization
-
-test_code \<open>- 805167 OR (- 314527 :: integer) = - 280591\<close> in Scala
-
-lemma \<open>473514 XOR (767063 :: integer) = 822781\<close>
- by normalization
-
-test_code \<open>473514 XOR (767063 :: integer) = 822781\<close> in Scala
-
-lemma \<open>- 805167 XOR (767063 :: integer) = - 523642\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (767063 :: integer) = - 523642\<close> in Scala
-
-lemma \<open>473514 XOR (- 314527 :: integer) = - 259381\<close>
- by normalization
-
-test_code \<open>473514 XOR (- 314527 :: integer) = - 259381\<close> in Scala
-
-lemma \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close>
- by normalization
-
-test_code \<open>- 805167 XOR (- 314527 :: integer) = 558512\<close> in Scala
-
-lemma \<open>NOT (473513 :: integer) = - 473514\<close>
- by normalization
-
-test_code \<open>NOT (473513 :: integer) = - 473514\<close> in Scala
-
-lemma \<open>NOT (- 805167 :: integer) = 805166\<close>
- by normalization
-
-test_code \<open>NOT (- 805167 :: integer) = 805166\<close> in Scala
-
-lemma \<open>(mask 39 :: integer) = 549755813887\<close>
- by normalization
-
-test_code \<open>(mask 39 :: integer) = 549755813887\<close> in Scala
-
-lemma \<open>set_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>set_bit 15 (473514 :: integer) = 506282\<close> in Scala
-
-lemma \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close>
- by normalization
-
-test_code \<open>set_bit 11 (- 805167 :: integer) = - 803119\<close> in Scala
-
-lemma \<open>unset_bit 13 (473514 :: integer) = 465322\<close>
- by normalization
-
-test_code \<open>unset_bit 13 (473514 :: integer) = 465322\<close> in Scala
-
-lemma \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>unset_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
-
-lemma \<open>flip_bit 15 (473514 :: integer) = 506282\<close>
- by normalization
-
-test_code \<open>flip_bit 15 (473514 :: integer) = 506282\<close> in Scala
-
-lemma \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close>
- by normalization
-
-test_code \<open>flip_bit 12 (- 805167 :: integer) = - 809263\<close> in Scala
-
-lemma \<open>push_bit 12 (473514 :: integer) = 1939513344\<close>
- by normalization
-
-test_code \<open>push_bit 12 (473514 :: integer) = 1939513344\<close> in Scala
-
-lemma \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close>
- by normalization
-
-test_code \<open>push_bit 12 (- 805167 :: integer) = - 3297964032\<close> in Scala
-
-lemma \<open>drop_bit 12 (473514 :: integer) = 115\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (473514 :: integer) = 115\<close> in Scala
-
-lemma \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close>
- by normalization
-
-test_code \<open>drop_bit 12 (- 805167 :: integer) = - 197\<close> in Scala
-
-lemma \<open>take_bit 12 (473514 :: integer) = 2474\<close>
- by normalization
-
-test_code \<open>take_bit 12 (473514 :: integer) = 2474\<close> in Scala
-
-lemma \<open>take_bit 12 (- 805167 :: integer) = 1745\<close>
- by normalization
-
-test_code \<open>take_bit 12 (- 805167 :: integer) = 1745\<close> in Scala
-
-lemma \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (473514 :: integer) = - 1622\<close> in Scala
-
-lemma \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close>
- by normalization
-
-test_code \<open>signed_take_bit 12 (- 805167 :: integer) = - 2351\<close> in Scala
-
end
--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Fri Jan 17 21:30:08 2025 +0100
@@ -60,4 +60,24 @@
test_code check in GHC
test_code check in Scala
+text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close>
+
+definition \<open>check_max = ()\<close>
+
+definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+
+code_printing
+ code_module Check_Max \<rightharpoonup>
+ (SML) \<open>
+fun check_max max =
+ let
+ val _ = IntInf.~>> (0, max);
+ val _ = ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); raise Fail "Bad max") handle Size => ())
+ in () end;
+\<close>
+ | constant check_max \<rightharpoonup>
+ (SML) "check'_max Bit'_Shifts.word'_max'_index"
+
+test_code \<open>snd anchor = ()\<close> in PolyML
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy Fri Jan 17 21:30:08 2025 +0100
@@ -0,0 +1,62 @@
+(* Title: HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Rewrite arithmetic operations to bit-shifts if feasible\<close>
+
+theory Code_Bit_Shifts_for_Arithmetic
+ imports Main
+begin
+
+context semiring_bit_operations
+begin
+
+context
+ includes bit_operations_syntax
+begin
+
+lemma [code_unfold]:
+ \<open>of_bool (odd a) = a AND 1\<close>
+ by (simp add: and_one_eq mod2_eq_if)
+
+lemma [code_unfold]:
+ \<open>even a \<longleftrightarrow> a AND 1 = 0\<close>
+ by (simp add: and_one_eq mod2_eq_if)
+
+lemma [code_unfold]:
+ \<open>2 * a = push_bit 1 a\<close>
+ by (simp add: ac_simps)
+
+lemma [code_unfold]:
+ \<open>a * 2 = push_bit 1 a\<close>
+ by simp
+
+lemma [code_unfold]:
+ \<open>2 ^ n * a = push_bit n a\<close>
+ by (simp add: push_bit_eq_mult ac_simps)
+
+lemma [code_unfold]:
+ \<open>a * 2 ^ n = push_bit n a\<close>
+ by (simp add: push_bit_eq_mult)
+
+lemma [code_unfold]:
+ \<open>a div 2 = drop_bit 1 a\<close>
+ by (simp add: drop_bit_eq_div)
+
+lemma [code_unfold]:
+ \<open>a div 2 ^ n = drop_bit n a\<close>
+ by (simp add: drop_bit_eq_div)
+
+lemma [code_unfold]:
+ \<open>a mod 2 = take_bit 1 a\<close>
+ by (simp add: take_bit_eq_mod)
+
+lemma [code_unfold]:
+ \<open>a mod 2 ^ n = take_bit n a\<close>
+ by (simp add: take_bit_eq_mod)
+
+end
+
+end
+
+end
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy Fri Jan 17 21:30:08 2025 +0100
@@ -41,6 +41,7 @@
type int = IntInf.int
val push : int -> int -> int
val drop : int -> int -> int
+ val word_max_index : Word.word (*only for validation*)
end = struct
type int = IntInf.int;
--- a/src/HOL/Library/Complete_Partial_Order2.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Fri Jan 17 21:30:08 2025 +0100
@@ -13,48 +13,48 @@
lemma chain_transfer [transfer_rule]:
includes lifting_syntax
shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
-unfolding chain_def[abs_def] by transfer_prover
-
+ unfolding chain_def[abs_def] by transfer_prover
+
lemma linorder_chain [simp, intro!]:
fixes Y :: "_ :: linorder set"
shows "Complete_Partial_Order.chain (\<le>) Y"
-by(auto intro: chainI)
+ by(auto intro: chainI)
lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)"
-by(simp add: fun_lub_def image_def)
+ by(simp add: fun_lub_def image_def)
lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. lub {})"
-by(rule ext)(simp add: fun_lub_apply)
+ by(rule ext)(simp add: fun_lub_apply)
lemma chain_fun_ordD:
assumes "Complete_Partial_Order.chain (fun_ord le) Y"
shows "Complete_Partial_Order.chain le ((\<lambda>f. f x) ` Y)"
-by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
+ by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
lemma chain_Diff:
"Complete_Partial_Order.chain ord A
\<Longrightarrow> Complete_Partial_Order.chain ord (A - B)"
-by(erule chain_subset) blast
+ by(erule chain_subset) blast
lemma chain_rel_prodD1:
"Complete_Partial_Order.chain (rel_prod orda ordb) Y
\<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)"
-by(auto 4 3 simp add: chain_def)
+ by(auto 4 3 simp add: chain_def)
lemma chain_rel_prodD2:
"Complete_Partial_Order.chain (rel_prod orda ordb) Y
\<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)"
-by(auto 4 3 simp add: chain_def)
+ by(auto 4 3 simp add: chain_def)
context ccpo begin
lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord (\<le>)) (mk_less (fun_ord (\<le>)))"
by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
- intro: order.trans order.antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
+ intro: order.trans order.antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain (\<le>) Y \<Longrightarrow> Sup Y \<le> x \<longleftrightarrow> (\<forall>y\<in>Y. y \<le> x)"
-by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
+ by (meson local.ccpo_Sup_least local.ccpo_Sup_upper local.dual_order.trans)
lemma Sup_minus_bot:
assumes chain: "Complete_Partial_Order.chain (\<le>) A"
@@ -152,11 +152,9 @@
proof(rule ccpo_Sup_least)
fix y
assume "y \<in> (\<lambda>x. f x x) ` Y"
- then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
- also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
- by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
- also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
- finally show "y \<le> ?lhs" .
+ then obtain x where "x \<in> Y" and "y = f x x" by blast
+ then show "y \<le> ?lhs"
+ by (metis (no_types, lifting) chain1 chain2 imageI ccpo_Sup_upper order.trans)
qed
qed
@@ -180,6 +178,7 @@
finally show "x \<le> \<dots>" .
qed
+
lemma swap_Sup:
fixes le_b (infix \<open>\<sqsubseteq>\<close> 60)
assumes Y: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
@@ -222,11 +221,10 @@
proof(rule ccpo_Sup_least)
fix x'
assume "x' \<in> (\<lambda>f. f x) ` Z"
- then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
- also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
- also have "f y \<le> ?rhs" using chain3
- by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
- finally show "x' \<le> ?rhs" .
+ then obtain f where "f \<in> Z" "x' = f x" by blast
+ then show "x' \<le> ?rhs"
+ by (metis (mono_tags, lifting) \<open>x \<sqsubseteq> y\<close> chain3 imageI ccpo_Sup_upper
+ order_trans mono monotoneD)
qed
qed
@@ -239,11 +237,10 @@
proof(rule ccpo_Sup_least)
fix x'
assume "x' \<in> f ` Y"
- then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
- also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
- by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
- also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
- finally show "x' \<le> ?rhs" .
+ then obtain y where "y \<in> Y" "x' = f y" by blast
+ then show "x' \<le> ?rhs"
+ by (metis (mono_tags, lifting) \<open>f \<in> Z\<close> chain3 chain4 imageI local.ccpo_Sup_upper
+ order.trans)
qed
finally show "x \<le> ?rhs" .
qed
@@ -257,12 +254,10 @@
proof(rule ccpo_Sup_least)
fix x'
assume "x' \<in> (\<lambda>f. f y) ` Z"
- then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
- also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
- by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
- also have "\<dots> \<le> ?lhs" using chain2
- by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
- finally show "x' \<le> ?lhs" .
+ then obtain f where "f \<in> Z" "x' = f y" by blast
+ then show "x' \<le> ?lhs"
+ by (metis (mono_tags, lifting) \<open>y \<in> Y\<close> ccpo_Sup_below_iff chain1 chain2 imageI
+ ccpo_Sup_upper)
qed
finally show "x \<le> ?lhs" .
qed
@@ -411,47 +406,47 @@
declare if_mono[simp]
lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"
-by(simp add: monotone_def)
+ by(simp add: monotone_def)
lemma monotone_applyI:
"monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))"
-by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
+ by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
lemma monotone_if_fun [partial_function_mono]:
"\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk>
\<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)"
-by(simp add: monotone_def fun_ord_def)
+ by(simp add: monotone_def fun_ord_def)
lemma monotone_fun_apply_fun [partial_function_mono]:
"monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\<lambda>f n. f t (g n))"
-by(rule monotoneI)(simp add: fun_ord_def)
+ by(rule monotoneI)(simp add: fun_ord_def)
lemma monotone_fun_ord_apply:
"monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))"
-by(auto simp add: monotone_def fun_ord_def)
+ by(auto simp add: monotone_def fun_ord_def)
context preorder begin
declare transp_on_le[cont_intro]
lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)"
-by(rule monotoneI) simp
+ by(rule monotoneI) simp
end
lemma transp_le [cont_intro, simp]:
"class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
-by(rule preorder.transp_on_le)
+ by(rule preorder.transp_on_le)
context partial_function_definitions begin
declare const_mono [cont_intro, simp]
lemma transp_le [cont_intro, simp]: "transp leq"
-by(rule transpI)(rule leq_trans)
+ by(rule transpI)(rule leq_trans)
lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"
-by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
+ by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
declare ccpo[cont_intro, simp]
@@ -460,91 +455,91 @@
lemma contI [intro?]:
"(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y))
\<Longrightarrow> cont luba orda lubb ordb f"
-unfolding cont_def by blast
+ unfolding cont_def by blast
lemma contD:
"\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>
\<Longrightarrow> f (luba Y) = lubb (f ` Y)"
-unfolding cont_def by blast
+ unfolding cont_def by blast
lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id"
-by(rule contI) simp
+ by(rule contI) simp
lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)"
-using cont_id[unfolded id_def] .
+ using cont_id[unfolded id_def] .
lemma cont_applyI [cont_intro]:
assumes cont: "cont luba orda lubb ordb g"
shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))"
-by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
+ by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
-by(simp add: cont_def fun_lub_apply)
+ by(simp add: cont_def fun_lub_apply)
lemma cont_if [cont_intro]:
"\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk>
\<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
-by(cases c) simp_all
+ by(cases c) simp_all
lemma mcontI [intro?]:
- "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
-by(simp add: mcont_def)
+ "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
+ by(simp add: mcont_def)
lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f"
-by(simp add: mcont_def)
+ by(simp add: mcont_def)
lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f"
-by(simp add: mcont_def)
+ by(simp add: mcont_def)
lemma mcont_monoD:
"\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)"
-by(auto simp add: mcont_def dest: monotoneD)
+ by(auto simp add: mcont_def dest: monotoneD)
lemma mcont_contD:
"\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>
\<Longrightarrow> f (luba Y) = lubb (f ` Y)"
-by(auto simp add: mcont_def dest: contD)
+ by(auto simp add: mcont_def dest: contD)
lemma mcont_call [cont_intro, simp]:
"mcont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
-by(simp add: mcont_def call_mono call_cont)
+ by(simp add: mcont_def call_mono call_cont)
lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)"
-by(simp add: mcont_def monotone_id')
+ by(simp add: mcont_def monotone_id')
lemma mcont_applyI:
"mcont luba orda lubb ordb (\<lambda>x. F x) \<Longrightarrow> mcont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. F (f x))"
-by(simp add: mcont_def monotone_applyI cont_applyI)
+ by(simp add: mcont_def monotone_applyI cont_applyI)
lemma mcont_if [cont_intro, simp]:
"\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk>
\<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
-by(simp add: mcont_def cont_if)
+ by(simp add: mcont_def cont_if)
lemma cont_fun_lub_apply:
"cont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>y. f y x))"
-by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
+ by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
lemma mcont_fun_lub_apply:
"mcont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>y. f y x))"
-by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
+ by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
context ccpo begin
lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
-by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
+ by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
lemma mcont_const [cont_intro, simp]:
"mcont luba orda Sup (\<le>) (\<lambda>x. c)"
-by(simp add: mcont_def)
+ by(simp add: mcont_def)
lemma cont_apply:
assumes 2: "\<And>x. cont lubb ordb Sup (\<le>) (\<lambda>y. f x y)"
- and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
- and 1: "\<And>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y)"
- and mono: "monotone orda ordb (\<lambda>x. t x)"
- and mono2: "\<And>x. monotone ordb (\<le>) (\<lambda>y. f x y)"
- and mono1: "\<And>y. monotone orda (\<le>) (\<lambda>x. f x y)"
+ and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
+ and 1: "\<And>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y)"
+ and mono: "monotone orda ordb (\<lambda>x. t x)"
+ and mono2: "\<And>x. monotone ordb (\<le>) (\<lambda>y. f x y)"
+ and mono1: "\<And>y. monotone orda (\<le>) (\<lambda>x. f x y)"
shows "cont luba orda Sup (\<le>) (\<lambda>x. f x (t x))"
proof
fix Y
@@ -561,16 +556,16 @@
\<And>y. mcont lub ord Sup (\<le>) (\<lambda>x. f x y);
mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x (t x))"
-unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
+ unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
lemma mcont2mcont:
"\<lbrakk>mcont lub' ord' Sup (\<le>) (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f (t x))"
-by(rule mcont2mcont'[OF _ mcont_const])
+ by(rule mcont2mcont'[OF _ mcont_const])
context
fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix \<open>\<sqsubseteq>\<close> 60)
- and lub :: "'b set \<Rightarrow> 'b" (\<open>\<Or>\<close>)
+ and lub :: "'b set \<Rightarrow> 'b" (\<open>\<Or>\<close>)
begin
lemma cont_fun_lub_Sup:
@@ -818,42 +813,42 @@
lemma admissible_disj' [simp, cont_intro]:
"\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk>
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"
-by(rule ccpo.admissible_disj)
+ by(rule ccpo.admissible_disj)
lemma admissible_imp' [cont_intro]:
"\<lbrakk> class.ccpo lub ord (mk_less ord);
ccpo.admissible lub ord (\<lambda>x. \<not> P x);
ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk>
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)"
-unfolding imp_conv_disj by(rule ccpo.admissible_disj)
+ unfolding imp_conv_disj by(rule ccpo.admissible_disj)
lemma admissible_imp [cont_intro]:
"(Q \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x))
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)"
-by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
+ by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]:
shows admissible_not_mem: "ccpo.admissible Union (\<subseteq>) (\<lambda>A. x \<notin> A)"
-by(rule ccpo.admissibleI) auto
+ by(rule ccpo.admissibleI) auto
lemma admissible_eqI:
assumes f: "cont luba orda lub ord (\<lambda>x. f x)"
- and g: "cont luba orda lub ord (\<lambda>x. g x)"
+ and g: "cont luba orda lub ord (\<lambda>x. g x)"
shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)"
-apply(rule ccpo.admissibleI)
-apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
-done
+ apply(rule ccpo.admissibleI)
+ apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
+ done
corollary admissible_eq_mcontI [cont_intro]:
"\<lbrakk> mcont luba orda lub ord (\<lambda>x. f x);
mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk>
\<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)"
-by(rule admissible_eqI)(auto simp add: mcont_def)
+ by(rule admissible_eqI)(auto simp add: mcont_def)
lemma admissible_iff [cont_intro, simp]:
"\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk>
\<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)"
-by(subst iff_conv_conj_imp)(rule admissible_conj)
+ by(subst iff_conv_conj_imp)(rule admissible_conj)
context ccpo begin
@@ -999,35 +994,35 @@
and bot: "P (\<lambda>_. lub {})"
and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> P (U (F f'))"
shows "P (U f)"
-unfolding eq inverse
-apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
-apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
-apply (rule_tac f'5="C x" in step)
-apply (simp_all add: inverse eq)
-done
+ unfolding eq inverse
+ apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
+ apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
+ apply (rule_tac f'5="C x" in step)
+ apply (simp_all add: inverse eq)
+ done
end
subsection \<open>\<^term>\<open>(=)\<close> as order\<close>
definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
-where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
+ where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
definition the_Sup :: "'a set \<Rightarrow> 'a"
-where "the_Sup A = (THE a. a \<in> A)"
+ where "the_Sup A = (THE a. a \<in> A)"
lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup"
-by(simp add: lub_singleton_def the_Sup_def)
+ by(simp add: lub_singleton_def the_Sup_def)
lemma (in ccpo) lub_singleton: "lub_singleton Sup"
-by(simp add: lub_singleton_def)
+ by(simp add: lub_singleton_def)
lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub"
-by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
+ by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
lemma preorder_eq [cont_intro, simp]:
"class.preorder (=) (mk_less (=))"
-by(unfold_locales)(simp_all add: mk_less_def)
+ by(unfold_locales)(simp_all add: mk_less_def)
lemma monotone_eqI [cont_intro]:
assumes "class.preorder ord (mk_less ord)"
@@ -1052,23 +1047,23 @@
lemma mcont_eqI [cont_intro, simp]:
"\<lbrakk> class.preorder ord (mk_less ord); lub_singleton lub \<rbrakk>
\<Longrightarrow> mcont the_Sup (=) lub ord f"
-by(simp add: mcont_def cont_eqI monotone_eqI)
+ by(simp add: mcont_def cont_eqI monotone_eqI)
subsection \<open>ccpo for products\<close>
definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
-where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
+ where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
lemma lub_singleton_prod_lub [cont_intro, simp]:
"\<lbrakk> lub_singleton luba; lub_singleton lubb \<rbrakk> \<Longrightarrow> lub_singleton (prod_lub luba lubb)"
-by(simp add: lub_singleton_def prod_lub_def)
+ by(simp add: lub_singleton_def prod_lub_def)
lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})"
-by(simp add: prod_lub_def)
+ by(simp add: prod_lub_def)
lemma preorder_rel_prodI [cont_intro, simp]:
assumes "class.preorder orda (mk_less orda)"
- and "class.preorder ordb (mk_less ordb)"
+ and "class.preorder ordb (mk_less ordb)"
shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
proof -
interpret a: preorder orda "mk_less orda" by fact
@@ -1078,9 +1073,9 @@
lemma order_rel_prodI:
assumes a: "class.order orda (mk_less orda)"
- and b: "class.order ordb (mk_less ordb)"
+ and b: "class.order ordb (mk_less ordb)"
shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
- (is "class.order ?ord ?ord'")
+ (is "class.order ?ord ?ord'")
proof(intro class.order.intro class.order_axioms.intro)
interpret a: order orda "mk_less orda" by(fact a)
interpret b: order ordb "mk_less ordb" by(fact b)
@@ -1093,10 +1088,10 @@
lemma monotone_rel_prodI:
assumes mono2: "\<And>a. monotone ordb ordc (\<lambda>b. f (a, b))"
- and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
- and a: "class.preorder orda (mk_less orda)"
- and b: "class.preorder ordb (mk_less ordb)"
- and c: "class.preorder ordc (mk_less ordc)"
+ and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
+ and a: "class.preorder orda (mk_less orda)"
+ and b: "class.preorder ordb (mk_less ordb)"
+ and c: "class.preorder ordc (mk_less ordc)"
shows "monotone (rel_prod orda ordb) ordc f"
proof -
interpret a: preorder orda "mk_less orda" by(rule a)
@@ -1108,7 +1103,7 @@
lemma monotone_rel_prodD1:
assumes mono: "monotone (rel_prod orda ordb) ordc f"
- and preorder: "class.preorder ordb (mk_less ordb)"
+ and preorder: "class.preorder ordb (mk_less ordb)"
shows "monotone orda ordc (\<lambda>a. f (a, b))"
proof -
interpret preorder ordb "mk_less ordb" by(rule preorder)
@@ -1117,7 +1112,7 @@
lemma monotone_rel_prodD2:
assumes mono: "monotone (rel_prod orda ordb) ordc f"
- and preorder: "class.preorder orda (mk_less orda)"
+ and preorder: "class.preorder orda (mk_less orda)"
shows "monotone ordb ordc (\<lambda>b. f (a, b))"
proof -
interpret preorder orda "mk_less orda" by(rule preorder)
@@ -1129,68 +1124,68 @@
class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb);
class.preorder ordc (mk_less ordc) \<rbrakk>
\<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)"
-by(rule monotone_rel_prodI) simp_all
+ by(rule monotone_rel_prodI) simp_all
lemma monotone_case_prodD1:
assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
- and preorder: "class.preorder ordb (mk_less ordb)"
+ and preorder: "class.preorder ordb (mk_less ordb)"
shows "monotone orda ordc (\<lambda>a. f a b)"
-using monotone_rel_prodD1[OF assms] by simp
+ using monotone_rel_prodD1[OF assms] by simp
lemma monotone_case_prodD2:
assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
- and preorder: "class.preorder orda (mk_less orda)"
+ and preorder: "class.preorder orda (mk_less orda)"
shows "monotone ordb ordc (f a)"
-using monotone_rel_prodD2[OF assms] by simp
+ using monotone_rel_prodD2[OF assms] by simp
context
fixes orda ordb ordc
assumes a: "class.preorder orda (mk_less orda)"
- and b: "class.preorder ordb (mk_less ordb)"
- and c: "class.preorder ordc (mk_less ordc)"
+ and b: "class.preorder ordb (mk_less ordb)"
+ and c: "class.preorder ordc (mk_less ordc)"
begin
lemma monotone_rel_prod_iff:
"monotone (rel_prod orda ordb) ordc f \<longleftrightarrow>
(\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and>
(\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))"
-using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
+ using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
lemma monotone_case_prod_iff [simp]:
"monotone (rel_prod orda ordb) ordc (case_prod f) \<longleftrightarrow>
(\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))"
-by(simp add: monotone_rel_prod_iff)
+ by(simp add: monotone_rel_prod_iff)
end
lemma monotone_case_prod_apply_iff:
"monotone orda ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: monotone_def)
+ by(simp add: monotone_def)
lemma monotone_case_prod_applyD:
"monotone orda ordb (\<lambda>x. (case_prod f x) y)
\<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: monotone_case_prod_apply_iff)
+ by(simp add: monotone_case_prod_apply_iff)
lemma monotone_case_prod_applyI:
"monotone orda ordb (case_prod (\<lambda>a b. f a b y))
\<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)"
-by(simp add: monotone_case_prod_apply_iff)
+ by(simp add: monotone_case_prod_apply_iff)
lemma cont_case_prod_apply_iff:
"cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: cont_def split_def)
+ by(simp add: cont_def split_def)
lemma cont_case_prod_applyI:
"cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))
\<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)"
-by(simp add: cont_case_prod_apply_iff)
+ by(simp add: cont_case_prod_apply_iff)
lemma cont_case_prod_applyD:
"cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)
\<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: cont_case_prod_apply_iff)
+ by(simp add: cont_case_prod_apply_iff)
lemma mcont_case_prod_apply_iff [simp]:
"mcont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow>
@@ -1307,13 +1302,8 @@
and t: "monotone orda ordb (\<lambda>x. t x)"
and t': "monotone orda ordc (\<lambda>x. t' x)"
shows "monotone orda leq (\<lambda>x. f (t x) (t' x))"
-proof(rule monotoneI)
- fix x y
- assume "orda x y"
- hence "rel_prod ordb ordc (t x, t' x) (t y, t' y)"
- using t t' by(auto dest: monotoneD)
- from monotoneD[OF f this] show "leq (f (t x) (t' x)) (f (t y) (t' y))" by simp
-qed
+ by (metis (mono_tags, lifting) case_prod_conv monotoneD monotoneI rel_prod.intros
+ assms)
lemma cont_case_prodI [cont_intro]:
"\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
@@ -1322,7 +1312,7 @@
class.preorder orda (mk_less orda);
class.preorder ordb (mk_less ordb) \<rbrakk>
\<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f)"
-by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
+ by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
lemma cont_case_prod_iff:
"\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
@@ -1330,39 +1320,39 @@
class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
\<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
(\<forall>x. cont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. cont luba orda lub leq (\<lambda>x. f x y))"
-by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
+ by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
lemma mcont_case_prod_iff [simp]:
"\<lbrakk> class.preorder orda (mk_less orda); lub_singleton luba;
class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
\<Longrightarrow> mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
(\<forall>x. mcont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. mcont luba orda lub leq (\<lambda>x. f x y))"
-unfolding mcont_def by(auto simp add: cont_case_prod_iff)
+ unfolding mcont_def by(auto simp add: cont_case_prod_iff)
end
lemma mono2mono_case_prod [cont_intro]:
assumes "\<And>x y. monotone orda ordb (\<lambda>f. pair f x y)"
shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
-by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
+ by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
subsection \<open>Complete lattices as ccpo\<close>
context complete_lattice begin
lemma complete_lattice_ccpo: "class.ccpo Sup (\<le>) (<)"
-by(unfold_locales)(fast intro: Sup_upper Sup_least)+
+ by(unfold_locales)(fast intro: Sup_upper Sup_least)+
lemma complete_lattice_ccpo': "class.ccpo Sup (\<le>) (mk_less (\<le>))"
-by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
+ by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
lemma complete_lattice_partial_function_definitions:
"partial_function_definitions (\<le>) Sup"
-by(unfold_locales)(auto intro: Sup_least Sup_upper)
+ by(unfold_locales)(auto intro: Sup_least Sup_upper)
lemma complete_lattice_partial_function_definitions_dual:
"partial_function_definitions (\<ge>) Inf"
-by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
+ by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
lemmas [cont_intro, simp] =
Partial_Function.ccpo[OF complete_lattice_partial_function_definitions]
@@ -1370,18 +1360,18 @@
lemma mono2mono_inf:
assumes f: "monotone ord (\<le>) (\<lambda>x. f x)"
- and g: "monotone ord (\<le>) (\<lambda>x. g x)"
+ and g: "monotone ord (\<le>) (\<lambda>x. g x)"
shows "monotone ord (\<le>) (\<lambda>x. f x \<sqinter> g x)"
-by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
+ by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
lemma mcont_const [simp]: "mcont lub ord Sup (\<le>) (\<lambda>_. c)"
-by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
+ by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
lemma mono2mono_sup:
assumes f: "monotone ord (\<le>) (\<lambda>x. f x)"
- and g: "monotone ord (\<le>) (\<lambda>x. g x)"
+ and g: "monotone ord (\<le>) (\<lambda>x. g x)"
shows "monotone ord (\<le>) (\<lambda>x. f x \<squnion> g x)"
-by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
+ by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
lemma Sup_image_sup:
assumes "Y \<noteq> {}"
@@ -1408,16 +1398,16 @@
qed
lemma mcont_sup1: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. x \<squnion> y)"
-by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
+ by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
lemma mcont_sup2: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>x. x \<squnion> y)"
-by(subst sup_commute)(rule mcont_sup1)
+ by(subst sup_commute)(rule mcont_sup1)
lemma mcont2mcont_sup [cont_intro, simp]:
"\<lbrakk> mcont lub ord Sup (\<le>) (\<lambda>x. f x);
mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<squnion> g x)"
-by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
+ by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
end
@@ -1426,59 +1416,59 @@
context complete_distrib_lattice begin
lemma mcont_inf1: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. x \<sqinter> y)"
-by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
+ by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
lemma mcont_inf2: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>x. x \<sqinter> y)"
-by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
+ by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
lemma mcont2mcont_inf [cont_intro, simp]:
"\<lbrakk> mcont lub ord Sup (\<le>) (\<lambda>x. f x);
mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<sqinter> g x)"
-by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
+ by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
end
interpretation lfp: partial_function_definitions "(\<le>) :: _ :: complete_lattice \<Rightarrow> _" Sup
-by(rule complete_lattice_partial_function_definitions)
+ by(rule complete_lattice_partial_function_definitions)
declaration \<open>Partial_Function.init "lfp" \<^term>\<open>lfp.fixp_fun\<close> \<^term>\<open>lfp.mono_body\<close>
@{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
interpretation gfp: partial_function_definitions "(\<ge>) :: _ :: complete_lattice \<Rightarrow> _" Inf
-by(rule complete_lattice_partial_function_definitions_dual)
+ by(rule complete_lattice_partial_function_definitions_dual)
declaration \<open>Partial_Function.init "gfp" \<^term>\<open>gfp.fixp_fun\<close> \<^term>\<open>gfp.mono_body\<close>
@{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
lemma insert_mono [partial_function_mono]:
- "monotone (fun_ord (\<subseteq>)) (\<subseteq>) A \<Longrightarrow> monotone (fun_ord (\<subseteq>)) (\<subseteq>) (\<lambda>y. insert x (A y))"
-by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
+ "monotone (fun_ord (\<subseteq>)) (\<subseteq>) A \<Longrightarrow> monotone (fun_ord (\<subseteq>)) (\<subseteq>) (\<lambda>y. insert x (A y))"
+ by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
lemma mono2mono_insert [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_insert: "monotone (\<subseteq>) (\<subseteq>) (insert x)"
-by(rule monotoneI) blast
+ by(rule monotoneI) blast
lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_insert: "mcont Union (\<subseteq>) Union (\<subseteq>) (insert x)"
-by(blast intro: mcontI contI monotone_insert)
+ by(blast intro: mcontI contI monotone_insert)
lemma mono2mono_image [THEN lfp.mono2mono, cont_intro, simp]:
shows monotone_image: "monotone (\<subseteq>) (\<subseteq>) ((`) f)"
-by(rule monotoneI) blast
+ by(rule monotoneI) blast
lemma cont_image: "cont Union (\<subseteq>) Union (\<subseteq>) ((`) f)"
-by(rule contI)(auto)
+ by(rule contI)(auto)
lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]:
shows mcont_image: "mcont Union (\<subseteq>) Union (\<subseteq>) ((`) f)"
-by(blast intro: mcontI monotone_image cont_image)
+ by(blast intro: mcontI monotone_image cont_image)
context complete_lattice begin
lemma monotone_Sup [cont_intro, simp]:
"monotone ord (\<subseteq>) f \<Longrightarrow> monotone ord (\<le>) (\<lambda>x. \<Squnion>f x)"
-by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
+ by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
lemma cont_Sup:
assumes "cont lub ord Union (\<subseteq>) f"
@@ -1694,21 +1684,21 @@
for P
lemma monotone_fst: "monotone (rel_prod orda ordb) orda fst"
-by(auto intro: monotoneI)
+ by(auto intro: monotoneI)
lemma mcont_fst: "mcont (prod_lub luba lubb) (rel_prod orda ordb) luba orda fst"
-by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
+ by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
lemma mcont2mcont_fst [cont_intro, simp]:
"mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
\<Longrightarrow> mcont lub ord luba orda (\<lambda>x. fst (t x))"
-by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
+ by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
lemma monotone_snd: "monotone (rel_prod orda ordb) ordb snd"
-by(auto intro: monotoneI)
+ by(auto intro: monotoneI)
lemma mcont_snd: "mcont (prod_lub luba lubb) (rel_prod orda ordb) lubb ordb snd"
-by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
+ by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
lemma mcont2mcont_snd [cont_intro, simp]:
"mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
@@ -1718,19 +1708,20 @@
lemma monotone_Pair:
"\<lbrakk> monotone ord orda f; monotone ord ordb g \<rbrakk>
\<Longrightarrow> monotone ord (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(simp add: monotone_def)
+ by(simp add: monotone_def)
lemma cont_Pair:
"\<lbrakk> cont lub ord luba orda f; cont lub ord lubb ordb g \<rbrakk>
\<Longrightarrow> cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
+ by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
lemma mcont_Pair:
"\<lbrakk> mcont lub ord luba orda f; mcont lub ord lubb ordb g \<rbrakk>
\<Longrightarrow> mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
+ by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
-context partial_function_definitions begin
+context partial_function_definitions
+begin
text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
--- a/src/HOL/Library/Extended_Nat.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Fri Jan 17 21:30:08 2025 +0100
@@ -191,10 +191,10 @@
by (simp_all add: eSuc_plus_1 ac_simps)
lemma iadd_Suc: "eSuc m + n = eSuc (m + n)"
- by (simp_all add: eSuc_plus_1 ac_simps)
+ by (simp add: eSuc_plus_1 ac_simps)
lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
- by (simp only: add.commute[of m] iadd_Suc)
+ by (metis add.commute iadd_Suc)
subsection \<open>Multiplication\<close>
@@ -216,29 +216,12 @@
instance
proof
fix a b c :: enat
- show "(a * b) * c = a * (b * c)"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
- show comm: "a * b = b * a"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
- show "1 * a = a"
- unfolding times_enat_def zero_enat_def one_enat_def
- by (simp split: enat.split)
show distr: "(a + b) * c = a * c + b * c"
unfolding times_enat_def zero_enat_def
by (simp split: enat.split add: distrib_right)
- show "0 * a = 0"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
- show "a * 0 = 0"
- unfolding times_enat_def zero_enat_def
- by (simp split: enat.split)
show "a * (b + c) = a * b + a * c"
by (cases a b c rule: enat3_cases) (auto simp: times_enat_def zero_enat_def distrib_left)
- show "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
- by (cases a b rule: enat2_cases) (auto simp: times_enat_def zero_enat_def)
-qed
+qed (auto simp: times_enat_def zero_enat_def one_enat_def split: enat.split)
end
@@ -246,13 +229,10 @@
unfolding eSuc_plus_1 by (simp add: algebra_simps)
lemma mult_eSuc_right: "m * eSuc n = m + m * n"
- unfolding eSuc_plus_1 by (simp add: algebra_simps)
+ by (metis mult.commute mult_eSuc)
lemma of_nat_eq_enat: "of_nat n = enat n"
- apply (induct n)
- apply (simp add: enat_0)
- apply (simp add: plus_1_eSuc eSuc_enat)
- done
+ by (induct n) (auto simp: enat_0 plus_1_eSuc eSuc_enat)
instance enat :: semiring_char_0
proof
@@ -267,7 +247,7 @@
lemma numeral_eq_enat:
"numeral k = enat (numeral k)"
- using of_nat_eq_enat [of "numeral k"] by simp
+ by (metis of_nat_eq_enat of_nat_numeral)
lemma enat_numeral [code_abbrev]:
"enat (numeral k) = numeral k"
@@ -349,11 +329,11 @@
lemma numeral_le_enat_iff[simp]:
shows "numeral m \<le> enat n \<longleftrightarrow> numeral m \<le> n"
-by (auto simp: numeral_eq_enat)
+ by (auto simp: numeral_eq_enat)
lemma numeral_less_enat_iff[simp]:
shows "numeral m < enat n \<longleftrightarrow> numeral m < n"
-by (auto simp: numeral_eq_enat)
+ by (auto simp: numeral_eq_enat)
lemma enat_ord_code [code]:
"enat m \<le> enat n \<longleftrightarrow> m \<le> n"
@@ -472,17 +452,15 @@
by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all
lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j \<Longrightarrow> \<exists>j. enat k < Y j"
-apply (induct_tac k)
- apply (simp (no_asm) only: enat_0)
- apply (fast intro: le_less_trans [OF zero_le])
-apply (erule exE)
-apply (drule spec)
-apply (erule exE)
-apply (drule ileI1)
-apply (rule eSuc_enat [THEN subst])
-apply (rule exI)
-apply (erule (1) le_less_trans)
-done
+proof (induction k)
+ case 0
+ then show ?case
+ using enat_0 zero_less_iff_neq_zero by fastforce
+next
+ case (Suc k)
+ then show ?case
+ by (meson Suc_ile_eq order_le_less_trans)
+qed
lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
by (simp add: eSuc_def split: enat.split)
@@ -490,10 +468,7 @@
lemma eSuc_Max:
assumes "finite A" "A \<noteq> {}"
shows "eSuc (Max A) = Max (eSuc ` A)"
-using assms proof induction
- case (insert x A)
- thus ?case by(cases "A = {}")(simp_all add: eSuc_max)
-qed simp
+ by (simp add: assms mono_Max_commute mono_eSuc)
instantiation enat :: "{order_bot, order_top}"
begin
@@ -511,19 +486,16 @@
shows "finite A"
proof (rule finite_subset)
show "finite (enat ` {..n})" by blast
- have "A \<subseteq> {..enat n}" using le_fin by fastforce
- also have "\<dots> \<subseteq> enat ` {..n}"
- apply (rule subsetI)
- subgoal for x by (cases x) auto
- done
- finally show "A \<subseteq> enat ` {..n}" .
+ have "A \<subseteq> enat ` {..n}"
+ using enat_ile le_fin by fastforce
+ then show "A \<subseteq> enat ` {..n}" .
qed
subsection \<open>Cancellation simprocs\<close>
lemma add_diff_cancel_enat[simp]: "x \<noteq> \<infinity> \<Longrightarrow> x + y - x = (y::enat)"
-by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
+ by (metis add.commute add.right_neutral add_diff_assoc_enat idiff_self order_refl)
lemma enat_add_left_cancel: "a + b = a + c \<longleftrightarrow> a = (\<infinity>::enat) \<or> b = c"
unfolding plus_enat_def by (simp split: enat.split)
@@ -535,7 +507,7 @@
unfolding plus_enat_def by (simp split: enat.split)
lemma plus_eq_infty_iff_enat: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
-using enat_add_left_cancel by fastforce
+ using enat_add_left_cancel by fastforce
ML \<open>
structure Cancel_Enat_Common =
@@ -605,32 +577,21 @@
subsection \<open>Well-ordering\<close>
lemma less_enatE:
- "[| n < enat m; !!k. n = enat k ==> k < m ==> P |] ==> P"
-by (induct n) auto
+ "\<lbrakk>n < enat m; \<And>k. \<lbrakk>n = enat k; k < m\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ using enat_iless enat_ord_simps(2) by blast
lemma less_infinityE:
- "[| n < \<infinity>; !!k. n = enat k ==> P |] ==> P"
-by (induct n) auto
+ "\<lbrakk>n < \<infinity>; \<And>k. n = enat k \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ by auto
lemma enat_less_induct:
- assumes prem: "\<And>n. \<forall>m::enat. m < n \<longrightarrow> P m \<Longrightarrow> P n" shows "P n"
+ assumes "\<And>n. \<forall>m::enat. m < n \<longrightarrow> P m \<Longrightarrow> P n"
+ shows "P n"
proof -
- have P_enat: "\<And>k. P (enat k)"
- apply (rule nat_less_induct)
- apply (rule prem, clarify)
- apply (erule less_enatE, simp)
- done
- show ?thesis
- proof (induct n)
- fix nat
- show "P (enat nat)" by (rule P_enat)
- next
- show "P \<infinity>"
- apply (rule prem, clarify)
- apply (erule less_infinityE)
- apply (simp add: P_enat)
- done
- qed
+ have "P (enat k)" for k
+ by (induction k rule: less_induct) (metis less_enatE assms)
+ then show ?thesis
+ by (metis enat.exhaust less_infinityE assms)
qed
instance enat :: wellorder
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jan 17 21:30:08 2025 +0100
@@ -16,20 +16,17 @@
lemma Limsup_const_add:
fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
shows "F \<noteq> bot \<Longrightarrow> Limsup F (\<lambda>x. c + f x) = c + Limsup F f"
- by (rule Limsup_compose_continuous_mono)
- (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
+ by (intro Limsup_compose_continuous_mono monoI add_mono continuous_intros) auto
lemma Liminf_const_add:
fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. c + f x) = c + Liminf F f"
- by (rule Liminf_compose_continuous_mono)
- (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
+ by (intro Liminf_compose_continuous_mono monoI add_mono continuous_intros) auto
lemma Liminf_add_const:
fixes c :: "'a::{complete_linorder, linorder_topology, topological_monoid_add, ordered_ab_semigroup_add}"
shows "F \<noteq> bot \<Longrightarrow> Liminf F (\<lambda>x. f x + c) = Liminf F f + c"
- by (rule Liminf_compose_continuous_mono)
- (auto intro!: monoI add_mono continuous_on_add continuous_on_id continuous_on_const)
+ by (intro Liminf_compose_continuous_mono monoI add_mono continuous_intros) auto
lemma sums_offset:
fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
@@ -96,9 +93,7 @@
by (induction i) (auto simp: bot eq f_le_lfp intro!: le_lfp mg)
then show "\<alpha> (lfp f) \<le> lfp g"
unfolding sup_continuous_lfp[OF f]
- by (subst \<alpha>[THEN sup_continuousD])
- (auto intro!: mono_funpow sup_continuous_mono[OF f] SUP_least)
-
+ by (simp add: SUP_least \<alpha>[THEN sup_continuousD] mf mono_funpow)
show "lfp g \<le> \<alpha> (lfp f)"
by (rule lfp_lowerbound) (simp add: eq[symmetric] lfp_fixpoint[OF mf])
qed
@@ -337,16 +332,17 @@
lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
proof -
+ have [simp]: "max 0 (SUP x\<in>{n..}. enn2ereal (y x)) = (SUP x\<in>{n..}. enn2ereal (y x))" for n::nat and y
+ by (meson SUP_upper atLeast_iff enn2ereal_nonneg max.absorb2 nle_le order_trans)
have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i\<in>{n..}. x i)) limsup"
unfolding limsup_INF_SUP[abs_def] by (transfer_prover_start, transfer_step+; simp)
- then show ?thesis
- unfolding limsup_INF_SUP[abs_def]
- apply (subst (asm) (2) rel_fun_def)
- apply (subst (2) rel_fun_def)
- apply (auto simp: comp_def max.absorb2 Sup_upper2 rel_fun_eq_pcr_ennreal)
- apply (subst (asm) max.absorb2)
- apply (auto intro: SUP_upper2)
- done
+ moreover
+ have "\<And>x y. \<lbrakk>rel_fun (=) pcr_ennreal x y;
+ pcr_ennreal (INF n::nat. max 0 (Sup (x ` {n..}))) (INF n. Sup (y ` {n..}))\<rbrakk>
+ \<Longrightarrow> pcr_ennreal (INF n. Sup (x ` {n..})) (INF n. Sup (y ` {n..}))"
+ by (auto simp: comp_def rel_fun_eq_pcr_ennreal)
+ ultimately show ?thesis
+ by (simp add: limsup_INF_SUP rel_fun_def)
qed
lemma sum_enn2ereal[simp]: "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Sum>i\<in>I. enn2ereal (f i)) = enn2ereal (sum f I)"
@@ -363,7 +359,7 @@
by (metis enn2ereal_of_nat numeral_eq_ereal of_nat_numeral)
lemma transfer_numeral[transfer_rule]: "pcr_ennreal (numeral a) (numeral a)"
- unfolding cr_ennreal_def pcr_ennreal_def by auto
+ by (metis enn2ereal_numeral pcr_ennreal_enn2ereal)
subsection \<open>Cancellation simprocs\<close>
@@ -654,7 +650,7 @@
fixes a b c :: ennreal
shows "a - b \<le> a - c \<Longrightarrow> a < top \<Longrightarrow> b \<le> a \<Longrightarrow> c \<le> a \<Longrightarrow> c \<le> b"
by transfer
- (auto simp add: max.absorb2 ereal_diff_positive top_ereal_def dest: ereal_mono_minus_cancel)
+ (auto simp add: ereal_diff_positive top_ereal_def dest: ereal_mono_minus_cancel)
lemma ennreal_mono_minus:
fixes a b c :: ennreal
@@ -718,16 +714,13 @@
done
lemma ennreal_inverse_mult: "a < top \<Longrightarrow> b < top \<Longrightarrow> inverse (a * b::ennreal) = inverse a * inverse b"
- apply transfer
- subgoal for a b
- by (cases a b rule: ereal2_cases) (auto simp: top_ereal_def)
- done
+ by (simp add: ennreal_inverse_mult')
lemma ennreal_inverse_1[simp]: "inverse (1::ennreal) = 1"
by transfer simp
lemma ennreal_inverse_eq_0_iff[simp]: "inverse (a::ennreal) = 0 \<longleftrightarrow> a = top"
- by transfer (simp add: ereal_inverse_eq_0 top_ereal_def)
+ by (metis ennreal_inverse_positive not_gr_zero)
lemma ennreal_inverse_eq_top_iff[simp]: "inverse (a::ennreal) = top \<longleftrightarrow> a = 0"
by transfer (simp add: top_ereal_def)
@@ -752,7 +745,7 @@
by (cases "a = 0") simp_all
lemma ennreal_zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < (b::ennreal)"
- by transfer (auto simp add: ereal_zero_less_0_iff le_less)
+ using not_gr_zero by fastforce
lemma less_diff_eq_ennreal:
fixes a b c :: ennreal
@@ -768,7 +761,7 @@
by transfer (metis (no_types) add.commute ereal_diff_positive ereal_ineq_diff_add max_def not_MInfty_nonneg)
lemma ennreal_diff_self[simp]: "a \<noteq> top \<Longrightarrow> a - a = (0::ennreal)"
- by transfer (simp add: top_ereal_def)
+ by (meson ennreal_minus_pos_iff less_imp_neq not_gr_zero top.not_eq_extremum)
lemma ennreal_minus_mono:
fixes a b c :: ennreal
@@ -852,7 +845,7 @@
by (metis e2ennreal_def enn2ereal_inverse ennreal.rep_eq sup_ereal_def)
lemma ennreal_0[simp]: "ennreal 0 = 0"
- by (simp add: ennreal_def max.absorb1 zero_ennreal.abs_eq)
+ by (simp add: ennreal_def zero_ennreal.abs_eq)
lemma ennreal_1[simp]: "ennreal 1 = 1"
by transfer (simp add: max_absorb2)
@@ -926,11 +919,10 @@
by (auto split: split_min)
lemma ennreal_half[simp]: "ennreal (1/2) = inverse 2"
- by transfer (simp add: max.absorb2)
+ by transfer auto
lemma ennreal_minus: "0 \<le> q \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
- by transfer
- (simp add: max.absorb2 zero_ereal_def flip: ereal_max)
+ by transfer (simp add: zero_ereal_def flip: ereal_max)
lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
by (simp add: minus_top_ennreal)
@@ -958,8 +950,7 @@
by (induction n) (auto simp: ennreal_mult)
lemma power_eq_top_ennreal: "x ^ n = top \<longleftrightarrow> (n \<noteq> 0 \<and> (x::ennreal) = top)"
- by (cases x rule: ennreal_cases)
- (auto simp: ennreal_power top_power_ennreal)
+ using not_gr_zero power_eq_top_ennreal_iff by force
lemma inverse_ennreal: "0 < r \<Longrightarrow> inverse (ennreal r) = ennreal (inverse r)"
by transfer (simp add: max.absorb2)
@@ -982,7 +973,7 @@
lemma power_divide_distrib_ennreal [algebra_simps]:
"(x / y) ^ n = x ^ n / (y ^ n :: ennreal)"
- by (simp add: divide_ennreal_def algebra_simps ennreal_inverse_power)
+ by (simp add: divide_ennreal_def ennreal_inverse_power power_mult_distrib)
lemma ennreal_divide_numeral: "0 \<le> x \<Longrightarrow> ennreal x / numeral b = ennreal (x / numeral b)"
by (subst divide_ennreal[symmetric]) auto
@@ -997,11 +988,7 @@
using assms by (induction A rule: infinite_finite_induct) (auto intro!: mult_mono)
lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \<longleftrightarrow> (a = b \<or> c \<le> 0)"
-proof (cases "0 \<le> c")
- case True
- then show ?thesis
- by (metis ennreal_eq_0_iff ennreal_mult_right_cong ennreal_neq_top mult_divide_eq_ennreal)
-qed (use ennreal_neg in auto)
+ by (metis ennreal_eq_0_iff mult_divide_eq_ennreal mult_eq_0_iff top_neq_ennreal)
lemma ennreal_le_epsilon:
"(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
@@ -1166,13 +1153,13 @@
lemma enn2ereal_Iio: "enn2ereal -` {..<a} = (if 0 \<le> a then {..< e2ennreal a} else {})"
using enn2ereal_nonneg
by (cases a rule: ereal_ennreal_cases)
- (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
+ (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def
simp del: enn2ereal_nonneg
intro: le_less_trans less_imp_le)
lemma enn2ereal_Ioi: "enn2ereal -` {a <..} = (if 0 \<le> a then {e2ennreal a <..} else UNIV)"
by (cases a rule: ereal_ennreal_cases)
- (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def max_absorb2
+ (auto simp add: vimage_def set_eq_iff ennreal.enn2ereal_inverse less_ennreal.rep_eq e2ennreal_def
intro: less_le_trans)
instantiation ennreal :: linear_continuum_topology
@@ -1203,25 +1190,23 @@
show "continuous_on ({0..} \<union> {..0}) e2ennreal"
proof (rule continuous_on_closed_Un)
show "continuous_on {0 ..} e2ennreal"
- by (rule continuous_onI_mono)
- (auto simp add: less_eq_ennreal.abs_eq eq_onp_def enn2ereal_range)
+ by (simp add: continuous_onI_mono e2ennreal_mono enn2ereal_range)
show "continuous_on {.. 0} e2ennreal"
- by (subst continuous_on_cong[OF refl, of _ _ "\<lambda>_. 0"])
- (auto simp add: e2ennreal_neg continuous_on_const)
+ by (metis atMost_iff continuous_on_cong continuous_on_const e2ennreal_neg)
qed auto
- show "A \<subseteq> {0..} \<union> {..0::ereal}"
- by auto
-qed
+qed auto
lemma continuous_at_e2ennreal: "continuous (at x within A) e2ennreal"
- by (rule continuous_on_imp_continuous_within[OF continuous_on_e2ennreal, of _ UNIV]) auto
+ using continuous_on_e2ennreal continuous_on_imp_continuous_within top.extremum
+ by blast
lemma continuous_on_enn2ereal: "continuous_on UNIV enn2ereal"
by (rule continuous_on_generate_topology[OF open_generated_order])
(auto simp add: enn2ereal_Iio enn2ereal_Ioi)
lemma continuous_at_enn2ereal: "continuous (at x within A) enn2ereal"
- by (rule continuous_on_imp_continuous_within[OF continuous_on_enn2ereal]) auto
+ by (meson UNIV_I continuous_at_imp_continuous_at_within
+ continuous_on_enn2ereal continuous_on_eq_continuous_within)
lemma sup_continuous_e2ennreal[order_continuous_intros]:
assumes f: "sup_continuous f" shows "sup_continuous (\<lambda>x. e2ennreal (f x))"
@@ -1370,7 +1355,7 @@
unfolding sums_def by (simp add: always_eventually sum_nonneg)
lemma suminf_enn2ereal[simp]: "(\<Sum>i. enn2ereal (f i)) = enn2ereal (suminf f)"
- by (rule sums_unique[symmetric]) (simp add: summable_sums)
+ by (metis summableI summable_sums sums_enn2ereal sums_unique)
lemma transfer_e2ennreal_suminf [transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal suminf suminf"
by (auto simp: rel_funI rel_fun_eq_pcr_ennreal comp_def)
@@ -1565,7 +1550,7 @@
fixes f g :: "nat \<Rightarrow> ennreal"
shows "(\<And>i. g i \<le> f i) \<Longrightarrow> suminf f \<noteq> top \<Longrightarrow> suminf g \<noteq> top \<Longrightarrow> (\<Sum>i. f i - g i) = suminf f - suminf g"
by transfer
- (auto simp add: max.absorb2 ereal_diff_positive suminf_le_pos top_ereal_def intro!: suminf_ereal_minus)
+ (auto simp add: ereal_diff_positive suminf_le_pos top_ereal_def intro!: suminf_ereal_minus)
lemma ennreal_Sup_countable_SUP:
"A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
@@ -1605,7 +1590,7 @@
have "f (SUP i \<in> I. g i) = (SUP i \<in> range M. f i)"
unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by (simp add: image_comp)
also have "\<dots> \<le> (SUP i \<in> I. f (g i))"
- by (insert M, drule SUP_subset_mono) (auto simp add: image_comp)
+ by (smt (verit) M SUP_le_iff dual_order.refl image_iff subsetD)
finally show "f (SUP i \<in> I. g i) \<le> (SUP i \<in> I. f (g i))" .
qed
@@ -1633,8 +1618,9 @@
(* Contributed by Dominique Unruh *)
lemma isCont_ennreal[simp]: \<open>isCont ennreal x\<close>
- apply (auto intro!: sequentially_imp_eventually_within simp: continuous_within tendsto_def)
- by (metis tendsto_def tendsto_ennrealI)
+ unfolding continuous_within tendsto_def
+ using tendsto_ennrealI topological_tendstoD
+ by (blast intro: sequentially_imp_eventually_within)
(* Contributed by Dominique Unruh *)
lemma isCont_ennreal_of_enat[simp]: \<open>isCont ennreal_of_enat x\<close>
@@ -1672,12 +1658,8 @@
define s where \<open>s = {x}\<close>
have \<open>open s\<close>
using False open_enat_iff s_def by blast
- moreover have \<open>x \<in> s\<close>
- using s_def by auto
- moreover have \<open>ennreal_of_enat z \<in> t\<close> if \<open>z \<in> s\<close> for z
- using asm s_def that by blast
- ultimately show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
- by auto
+ then show \<open>\<exists>s. open s \<and> x \<in> s \<and> (\<forall>z\<in>s. ennreal_of_enat z \<in> t)\<close>
+ using asm s_def by blast
qed
qed
@@ -1686,15 +1668,10 @@
lemma INF_approx_ennreal:
fixes x::ennreal and e::real
assumes "e > 0"
- assumes INF: "x = (INF i \<in> A. f i)"
+ assumes "x = (INF i \<in> A. f i)"
assumes "x \<noteq> \<infinity>"
shows "\<exists>i \<in> A. f i < x + e"
-proof -
- have "(INF i \<in> A. f i) < x + e"
- unfolding INF[symmetric] using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
- then show ?thesis
- unfolding INF_less_iff .
-qed
+ using INF_less_iff assms by fastforce
lemma SUP_approx_ennreal:
fixes x::ennreal and e::real
@@ -1751,9 +1728,9 @@
lemma ennreal_approx_unit:
"(\<And>a::ennreal. 0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * z \<le> y) \<Longrightarrow> z \<le> y"
- apply (subst SUP_mult_right_ennreal[of "\<lambda>x. x" "{0 <..< 1}" z, simplified])
- apply (auto intro: SUP_least)
- done
+ using SUP_mult_right_ennreal[of "\<lambda>x. x" "{0 <..< 1}" z]
+ by (smt (verit) SUP_least Sup_greaterThanLessThan greaterThanLessThan_iff
+ image_ident mult_1 zero_less_one)
lemma suminf_ennreal2:
"(\<And>i. 0 \<le> f i) \<Longrightarrow> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal (\<Sum>i. f i)"
@@ -1784,11 +1761,8 @@
lemma ennreal_tendsto_top_eq_at_top:
"((\<lambda>z. ennreal (f z)) \<longlongrightarrow> top) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
unfolding filterlim_at_top_dense tendsto_top_iff_ennreal
- using ennreal_less_iff eventually_mono
- apply (auto simp: ennreal_less_iff)
- subgoal for y
- by (auto elim!: eventually_mono allE[of _ "max 0 y"])
- done
+ using ennreal_less_iff eventually_mono allE[of _ "max 0 _"]
+ by (smt (verit) linorder_not_less order_refl order_trans)
lemma tendsto_0_if_Limsup_eq_0_ennreal:
fixes f :: "_ \<Rightarrow> ennreal"
@@ -1874,10 +1848,7 @@
lemma add_diff_eq_iff_ennreal[simp]:
fixes x y :: ennreal shows "x + (y - x) = y \<longleftrightarrow> x \<le> y"
-proof
- assume *: "x + (y - x) = y" show "x \<le> y"
- by (subst *[symmetric]) simp
-qed (simp add: add_diff_inverse_ennreal)
+ by (metis ennreal_ineq_diff_add le_iff_add)
lemma add_diff_le_ennreal: "a + b - c \<le> a + (b - c::ennreal)"
apply (cases a b c rule: ennreal3_cases)
@@ -1901,7 +1872,8 @@
simp flip: ennreal_plus)
lemma power_less_top_ennreal: fixes x :: ennreal shows "x ^ n < top \<longleftrightarrow> x < top \<or> n = 0"
- using power_eq_top_ennreal[of x n] by (auto simp: less_top)
+ using power_eq_top_ennreal top.not_eq_extremum
+ by blast
lemma ennreal_divide_times: "(a / b) * c = a * (c / b :: ennreal)"
by (simp add: mult.commute ennreal_times_divide)
@@ -1914,7 +1886,7 @@
(auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_less_iff field_simps ennreal_top_mult ennreal_top_divide)
lemma one_less_numeral[simp]: "1 < (numeral n::ennreal) \<longleftrightarrow> (num.One < n)"
- by (simp flip: ennreal_1 ennreal_numeral add: ennreal_less_iff)
+ by simp
lemma divide_eq_1_ennreal: "a / b = (1::ennreal) \<longleftrightarrow> (b \<noteq> top \<and> b \<noteq> 0 \<and> b = a)"
by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm)
--- a/src/HOL/Library/Float.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Float.thy Fri Jan 17 21:30:08 2025 +0100
@@ -113,7 +113,7 @@
by (cases x rule: linorder_cases[of 0]) auto
lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float"
- by (cases x rule: linorder_cases[of 0]) (auto intro!: uminus_float)
+ by (simp add: sgn_real_def)
lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
by (simp add: float_def) (metis of_int_diff of_int_of_nat_eq powr_diff powr_realpow zero_less_numeral times_divide_eq_right)
@@ -144,8 +144,8 @@
from assms obtain m e :: int where "a = m * 2 powr e"
by (auto simp: float_def)
then show ?thesis
- by (auto intro!: floatI[where m="m^b" and e = "e*b"]
- simp: power_mult_distrib powr_realpow[symmetric] powr_powr)
+ by (intro floatI[where m="m^b" and e = "e*b"])
+ (auto simp: powr_powr power_mult_distrib simp flip: powr_realpow)
qed
lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e"
@@ -383,11 +383,10 @@
by (auto simp: float_def)
with \<open>x \<noteq> 0\<close> int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\<not> 2 dvd k"
by auto
- with \<open>\<not> 2 dvd k\<close> x show ?thesis
- apply (rule_tac exI[of _ "k"])
- apply (rule_tac exI[of _ "e + int i"])
- apply (simp add: powr_add powr_realpow)
- done
+ with \<open>\<not> 2 dvd k\<close> x have "x = real_of_int k * 2 powr real_of_int (e + int i) \<and> odd k"
+ by (simp add: powr_add powr_realpow)
+ then show ?thesis
+ by blast
qed
with that show thesis by blast
qed
@@ -799,7 +798,7 @@
apply (metis (no_types, opaque_lifting) Float.rep_eq
add.inverse_inverse compute_real_of_float diff_minus_eq_add
floor_divide_of_int_eq int_of_reals(1) linorder_not_le
- minus_add_distrib of_int_eq_numeral_power_cancel_iff )
+ minus_add_distrib of_int_eq_numeral_power_cancel_iff)
done
next
case False
@@ -1190,7 +1189,7 @@
using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
by (auto intro!: floor_mono)
finally show ?thesis
- by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
+ by (auto simp flip: powr_realpow simp: powr_diff assms)
qed
ultimately show ?thesis
by (metis dual_order.trans truncate_down)
@@ -1264,11 +1263,9 @@
note powr_strict = powr_less_cancel_iff[symmetric, OF \<open>1 < p\<close>, THEN iffD2]
have "floor ?r = (if i \<ge> j * p powr (?fl i - ?fl j) then 0 else -1)" (is "_ = ?if")
using assms
- by (linarith |
- auto
- intro!: floor_eq2
- intro: powr_strict powr
- simp: powr_diff powr_add field_split_simps algebra_simps)+
+ apply simp
+ by (smt (verit, ccfv_SIG) floor_less_iff floor_uminus_of_int le_log_iff mult_powr_eq
+ of_int_1 real_of_int_floor_add_one_gt zero_le_floor)
finally
show ?thesis by simp
qed
@@ -1852,7 +1849,7 @@
(plus_down prec (nprt b * nprt bb)
(plus_down prec (pprt a * pprt ab)
(pprt b * nprt ab)))"
- by (smt (verit, del_insts) mult_mono plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt
+ by (smt (verit, best) mult_mono plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt
pprt_mono mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)
lemma mult_float_mono2:
@@ -1870,7 +1867,7 @@
(plus_up prec (pprt aa * nprt bc)
(plus_up prec (nprt ba * pprt ac)
(nprt aa * nprt ac)))"
- by (smt (verit, del_insts) plus_up_mono add_mono mult_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono
+ by (smt (verit, best) plus_up_mono add_mono mult_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono
mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)
@@ -2164,7 +2161,7 @@
by transfer (simp add: truncate_down_nonneg)
lemma rapprox_rat: "real_of_int x / real_of_int y \<le> real_of_float (rapprox_rat prec x y)"
- by transfer (simp add: truncate_up)
+ by (simp add: rapprox_rat.rep_eq truncate_up)
lemma rapprox_rat_le1:
assumes "0 \<le> x" "0 < y" "x \<le> y"
@@ -2232,7 +2229,7 @@
by transfer (rule real_divl_pos_less1_bound)
lemma float_divr: "real_of_float x / real_of_float y \<le> real_of_float (float_divr prec x y)"
- by transfer (rule real_divr)
+ by (simp add: float_divr.rep_eq real_divr)
lemma real_divr_pos_less1_lower_bound:
assumes "0 < x"
--- a/src/HOL/Library/ListVector.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/ListVector.thy Fri Jan 17 21:30:08 2025 +0100
@@ -3,7 +3,7 @@
section \<open>Lists as vectors\<close>
theory ListVector
-imports Main
+ imports Main
begin
text\<open>\noindent
@@ -13,19 +13,19 @@
text\<open>Multiplication with a scalar:\<close>
abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix \<open>*\<^sub>s\<close> 70)
-where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
+ where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
-by (induct xs) simp_all
+ by (induct xs) simp_all
subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>
fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
-where
-"zipwith0 f [] [] = []" |
-"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
-"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
-"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
+ where
+ "zipwith0 f [] [] = []" |
+ "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
+ "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
+ "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
instantiation list :: ("{zero, plus}") plus
begin
@@ -58,44 +58,44 @@
end
lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
-by(induct ys) simp_all
+ by(induct ys) simp_all
lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
-by (induct xs) (auto simp:list_add_def)
+ by (induct xs) (auto simp:list_add_def)
lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
-by (induct xs) (auto simp:list_add_def)
+ by (induct xs) (auto simp:list_add_def)
lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
-by(auto simp:list_add_def)
+ by(auto simp:list_add_def)
lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
-by (induct xs) (auto simp:list_diff_def list_uminus_def)
+ by (induct xs) (auto simp:list_diff_def list_uminus_def)
lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
-by (induct xs) (auto simp:list_diff_def)
+ by (induct xs) (auto simp:list_diff_def)
lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
-by (induct xs) (auto simp:list_diff_def)
+ by (induct xs) (auto simp:list_diff_def)
lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
-by (induct xs) (auto simp:list_uminus_def)
+ by (induct xs) (auto simp:list_uminus_def)
lemma self_list_diff:
"xs - xs = replicate (length(xs::'a::group_add list)) 0"
-by(induct xs) simp_all
+ by(induct xs) simp_all
-lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
-shows "(xs+ys)+zs = xs+(ys+zs)"
-apply(induct xs arbitrary: ys zs)
- apply simp
-apply(case_tac ys)
- apply(simp)
-apply(simp)
-apply(case_tac zs)
- apply(simp)
-apply(simp add: add.assoc)
-done
+lemma list_add_assoc:
+ fixes xs :: "'a::monoid_add list"
+ shows "(xs+ys)+zs = xs+(ys+zs)"
+proof (induct xs arbitrary: ys zs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs ys zs)
+ show ?case
+ by (cases ys; cases zs; simp add: add.assoc Cons)
+qed
subsection "Inner product"
@@ -103,50 +103,55 @@
where "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
-by(simp add: iprod_def)
+ by(simp add: iprod_def)
lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
-by(simp add: iprod_def)
+ by(simp add: iprod_def)
lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
-by(simp add: iprod_def)
+ by(simp add: iprod_def)
lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
-apply(induct cs arbitrary:xs)
- apply simp
-apply(case_tac xs) apply simp
-apply auto
-done
+proof (induct cs arbitrary: xs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a cs xs)
+ then show ?case
+ by (cases xs; fastforce)
+qed
lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
-by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
+ by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
-apply(induct xs arbitrary: ys zs)
-apply (simp add: o_def split_def)
-apply(case_tac ys)
-apply simp
-apply(case_tac zs)
-apply (simp)
-apply(simp add: distrib_right)
-done
+proof (induct xs arbitrary: ys zs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs ys zs)
+ show ?case
+ by (cases ys; cases zs; simp add: distrib_right Cons)
+qed
lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
-apply(induct xs arbitrary: ys zs)
-apply (simp add: o_def split_def)
-apply(case_tac ys)
-apply simp
-apply(case_tac zs)
-apply (simp)
-apply(simp add: left_diff_distrib)
-done
+proof (induct xs arbitrary: ys zs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs ys zs)
+ show ?case
+ by (cases ys; cases zs; simp add: left_diff_distrib Cons)
+qed
lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
-apply(induct xs arbitrary: ys)
-apply simp
-apply(case_tac ys)
-apply (simp)
-apply (simp add: distrib_left mult.assoc)
-done
+proof (induct xs arbitrary: ys)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs ys)
+ show ?case
+ by (cases ys; simp add: distrib_left mult.assoc Cons)
+qed
end
--- a/src/HOL/Library/Poly_Mapping.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Poly_Mapping.thy Fri Jan 17 21:30:08 2025 +0100
@@ -20,19 +20,13 @@
fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
assumes "finite {a. f a \<noteq> 0}"
shows "finite {a. g a * f a \<noteq> 0}"
-proof -
- have "{a. g a * f a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
- then show ?thesis using assms by (rule finite_subset)
-qed
+ by (metis (mono_tags, lifting) Collect_mono assms mult_zero_right finite_subset)
lemma finite_mult_not_eq_zero_rightI:
fixes f :: "'b \<Rightarrow> 'a :: mult_zero"
assumes "finite {a. f a \<noteq> 0}"
shows "finite {a. f a * g a \<noteq> 0}"
-proof -
- have "{a. f a * g a \<noteq> 0} \<subseteq> {a. f a \<noteq> 0}" by auto
- then show ?thesis using assms by (rule finite_subset)
-qed
+ by (metis (mono_tags, lifting) Collect_mono assms lambda_zero finite_subset)
lemma finite_mult_not_eq_zero_prodI:
fixes f g :: "'a \<Rightarrow> 'b::semiring_0"
@@ -227,10 +221,7 @@
typedef (overloaded) ('a, 'b) poly_mapping (\<open>(_ \<Rightarrow>\<^sub>0 /_)\<close> [1, 0] 0) =
"{f :: 'a \<Rightarrow> 'b::zero. finite {x. f x \<noteq> 0}}"
morphisms lookup Abs_poly_mapping
-proof -
- have "(\<lambda>_::'a. (0 :: 'b)) \<in> ?poly_mapping" by simp
- then show ?thesis by (blast intro!: exI)
-qed
+ using not_finite_existsD by force
declare lookup_inverse [simp]
declare lookup_inject [simp]
@@ -366,9 +357,8 @@
end
-lemma lookup_add:
- "lookup (f + g) k = lookup f k + lookup g k"
- by transfer rule
+lemma lookup_add: "lookup (f + g) k = lookup f k + lookup g k"
+ by (simp add: plus_poly_mapping.rep_eq)
instance poly_mapping :: (type, comm_monoid_add) comm_monoid_add
by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
@@ -435,13 +425,12 @@
end
-lemma lookup_one:
- "lookup 1 k = (1 when k = 0)"
- by transfer rule
+lemma lookup_one: "lookup 1 k = (1 when k = 0)"
+ by (meson one_poly_mapping.rep_eq)
lemma lookup_one_zero [simp]:
"lookup 1 0 = 1"
- by transfer simp
+ by (simp add: one_poly_mapping.rep_eq)
definition prod_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a::monoid_add \<Rightarrow> 'b::semiring_0"
where
@@ -455,8 +444,9 @@
proof -
let ?C = "{a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
from fin_f fin_g have "finite ?C" by blast
- moreover have "{a. \<exists>b. (f a * g b when k = a + b) \<noteq> 0} \<times>
- {b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
+ moreover
+ have "{a. \<exists>b. (f a * g b when k = a + b) \<noteq> 0} \<times>
+ {b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}"
by auto
ultimately show ?thesis using fin_g
by (auto simp: prod_fun_def
@@ -653,7 +643,7 @@
show "1 * a = a"
by transfer (simp add: prod_fun_def [abs_def] when_mult)
show "a * 1 = a"
- apply transfer
+ apply transfer
apply (simp add: prod_fun_def [abs_def] Sum_any_right_distrib Sum_any_left_distrib mult_when)
apply (subst when_commute)
apply simp
@@ -705,11 +695,11 @@
lemma lookup_single_eq [simp]:
"lookup (single k v) k = v"
- by transfer simp
+ by (simp add: single.rep_eq)
lemma lookup_single_not_eq:
"k \<noteq> k' \<Longrightarrow> lookup (single k v) k' = 0"
- by transfer simp
+ by (simp add: single.rep_eq)
lemma single_zero [simp]:
"single k 0 = 0"
@@ -749,11 +739,7 @@
lemma lookup_of_nat:
"lookup (of_nat n) k = (of_nat n when k = 0)"
-proof -
- have "lookup (of_nat n) k = lookup (single 0 (of_nat n)) k"
- by simp
- then show ?thesis unfolding lookup_single by simp
-qed
+ by (metis lookup_single lookup_single_not_eq single_of_nat)
lemma of_nat_single:
"of_nat = single 0 \<circ> of_nat"
@@ -923,14 +909,7 @@
fix f g h :: "'a \<Rightarrow> 'b"
assume *: "less_fun f g \<or> f = g"
have "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k)" if "less_fun f g"
- proof -
- from that obtain k where "f k < g k" "(\<And>k'. k' < k \<Longrightarrow> f k' = g k')"
- by (blast elim!: less_funE)
- then have "h k + f k < h k + g k" "(\<And>k'. k' < k \<Longrightarrow> h k' + f k' = h k' + g k')"
- by simp_all
- then show ?thesis
- by (blast intro: less_funI)
- qed
+ by (metis (no_types, lifting) less_fun_def add_strict_left_mono that)
with * show "less_fun (\<lambda>k. h k + f k) (\<lambda>k. h k + g k) \<or> (\<lambda>k. h k + f k) = (\<lambda>k. h k + g k)"
by (auto simp: fun_eq_iff)
qed
@@ -986,7 +965,7 @@
have "Set.range f - {0} \<subseteq> f ` {x. f x \<noteq> 0}"
by auto
thus "finite (Set.range f - {0})"
- by(rule finite_subset)(rule finite_imageI[OF *])
+ using "*" finite_surj by blast
qed
lemma in_keys_lookup_in_range [simp]:
@@ -994,7 +973,7 @@
by transfer simp
lemma in_keys_iff: "x \<in> (keys s) = (lookup s x \<noteq> 0)"
- by (transfer, simp)
+ by (simp add: lookup_not_eq_zero_eq_in_keys)
lemma keys_zero [simp]:
"keys 0 = {}"
@@ -1221,9 +1200,9 @@
fix g :: "'c \<Rightarrow> 'd" and p :: "'a \<Rightarrow> 'c"
assume "finite {x. p x \<noteq> 0}"
hence "finite (f ` {y. p (f y) \<noteq> 0})"
- by(rule finite_subset[rotated]) auto
+ by (simp add: rev_finite_subset subset_eq)
thus "finite {x. (p \<circ> f) x \<noteq> 0}" unfolding o_def
- by(rule finite_imageD)(rule subset_inj_on[OF inj_f], simp)
+ by (metis finite_imageD injD inj_f inj_on_def)
qed
end
@@ -1402,7 +1381,7 @@
lemma nth_trailing_zeros [simp]:
"nth (xs @ replicate n 0) = nth xs"
- by transfer simp
+ by (simp add: nth.abs_eq)
lemma nth_idem:
"nth (List.map (lookup f) [0..<degree f]) = f"
@@ -1454,7 +1433,7 @@
lemma lookup_the_value:
"lookup (the_value xs) k = (case map_of xs k of None \<Rightarrow> 0 | Some v \<Rightarrow> v)"
- by transfer rule
+ by (simp add: the_value.rep_eq)
lemma items_the_value:
assumes "sorted (List.map fst xs)" and "distinct (List.map fst xs)" and "0 \<notin> snd ` set xs"
@@ -1552,15 +1531,10 @@
proof -
from assms obtain k where *: "lookup m k = v" "v \<noteq> 0"
by transfer blast
- from * have "k \<in> keys m"
+ then have "k \<in> keys m"
by (simp add: in_keys_iff)
- then show ?thesis
- proof (rule poly_mapping_size_estimation)
- from assms * have "y \<le> g (lookup m k)"
- by simp
- then show "y \<le> f k + g (lookup m k)"
- by simp
- qed
+ with * show ?thesis
+ by (simp add: Poly_Mapping.poly_mapping_size_estimation assms(2) trans_le_add2)
qed
end
@@ -1616,15 +1590,7 @@
by (force simp add: lookup_single_not_eq)
lemma frag_of_nonzero [simp]: "frag_of a \<noteq> 0"
-proof -
- let ?f = "\<lambda>x. if x = a then 1 else (0::int)"
- have "?f \<noteq> (\<lambda>x. 0::int)"
- by (auto simp: fun_eq_iff)
- then have "Poly_Mapping.lookup (Abs_poly_mapping ?f) \<noteq> Poly_Mapping.lookup (Abs_poly_mapping (\<lambda>x. 0))"
- by fastforce
- then show ?thesis
- by (metis lookup_single_eq lookup_zero)
-qed
+ by (metis lookup_single_eq lookup_zero zero_neq_one)
definition frag_cmul :: "int \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 int)"
where "frag_cmul c a = Abs_poly_mapping (\<lambda>x. c * Poly_Mapping.lookup a x)"
@@ -1636,7 +1602,7 @@
by (simp add: frag_cmul_def)
lemma frag_cmul_one [simp]: "frag_cmul 1 x = x"
- by (auto simp: frag_cmul_def Poly_Mapping.poly_mapping.lookup_inverse)
+ by (simp add: frag_cmul_def)
lemma frag_cmul_minus_one [simp]: "frag_cmul (-1) x = -x"
by (simp add: frag_cmul_def uminus_poly_mapping_def poly_mapping_eqI)
@@ -1684,13 +1650,7 @@
by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
lemma frag_cmul_distrib2: "frag_cmul c (a+b) = frag_cmul c a + frag_cmul c b"
-proof -
- have "finite {x. poly_mapping.lookup a x + poly_mapping.lookup b x \<noteq> 0}"
- using keys_add [of a b]
- by (metis (no_types, lifting) finite_keys finite_subset keys.rep_eq lookup_add mem_Collect_eq subsetI)
- then show ?thesis
- by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
-qed
+ by (simp add: int_distrib(2) lookup_add poly_mapping_eqI)
lemma frag_cmul_diff_distrib: "frag_cmul (a - b) c = frag_cmul a c - frag_cmul b c"
by (auto simp: left_diff_distrib lookup_minus poly_mapping_eqI)
--- a/src/HOL/Library/Signed_Division.thy Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Library/Signed_Division.thy Fri Jan 17 21:30:08 2025 +0100
@@ -104,8 +104,7 @@
"(a :: int) sdiv 1 = a"
"(a :: int) sdiv 0 = 0"
"(a :: int) sdiv -1 = -a"
- apply (auto simp: signed_divide_int_def sgn_if)
- done
+ by (auto simp: signed_divide_int_def sgn_if)
lemma smod_int_mod_0 [simp]:
"x smod (0 :: int) = x"
@@ -120,33 +119,26 @@
by (auto simp: signed_divide_int_def sgn_div_eq_sgn_mult sgn_mult)
lemma int_sdiv_same_is_1 [simp]:
- "a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = a) = (b = 1)"
- apply (rule iffI)
- apply (clarsimp simp: signed_divide_int_def)
- apply (subgoal_tac "b > 0")
- apply (case_tac "a > 0")
- apply (clarsimp simp: sgn_if)
- apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
- using int_div_less_self [of a b] apply linarith
- apply (metis add.commute add.inverse_inverse group_cancel.rule0 int_div_less_self linorder_neqE_linordered_idom neg_0_le_iff_le not_less verit_comp_simplify1(1) zless_imp_add1_zle)
- apply (metis div_minus_right neg_imp_zdiv_neg_iff neg_le_0_iff_le not_less order.not_eq_order_implies_strict)
- apply (metis abs_le_zero_iff abs_of_nonneg neg_imp_zdiv_nonneg_iff order.not_eq_order_implies_strict)
- done
+ assumes "a \<noteq> 0"
+ shows "((a :: int) sdiv b = a) = (b = 1)"
+proof -
+ have "b = 1" if "a sdiv b = a"
+ proof -
+ have "b>0"
+ by (smt (verit, ccfv_threshold) assms mult_cancel_left2 sgn_if sgn_mult
+ sgn_sdiv_eq_sgn_mult that)
+ then show ?thesis
+ by (smt (verit) assms dvd_eq_mod_eq_0 int_div_less_self of_bool_eq(1,2) sgn_if
+ signed_divide_int_eq_divide_int that zdiv_zminus1_eq_if)
+ qed
+ then show ?thesis
+ by auto
+qed
lemma int_sdiv_negated_is_minus1 [simp]:
"a \<noteq> 0 \<Longrightarrow> ((a :: int) sdiv b = - a) = (b = -1)"
- apply (clarsimp simp: signed_divide_int_def)
- apply (rule iffI)
- apply (subgoal_tac "b < 0")
- apply (case_tac "a > 0")
- apply (clarsimp simp: sgn_if algebra_split_simps not_less)
- apply (case_tac "sgn (a * b) = -1")
- apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
- apply (metis add.inverse_inverse int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
- apply (metis add.inverse_inverse div_minus_right int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
- apply (metis less_le neg_less_0_iff_less not_less pos_imp_zdiv_neg_iff)
- apply (metis div_minus_right dual_order.eq_iff neg_imp_zdiv_nonneg_iff neg_less_0_iff_less)
- done
+ using int_sdiv_same_is_1 [of _ "-b"]
+ using signed_divide_int_def by fastforce
lemma sdiv_int_range:
\<open>a sdiv b \<in> {- \<bar>a\<bar>..\<bar>a\<bar>}\<close> for a b :: int
@@ -178,9 +170,8 @@
"\<lbrakk> 0 \<le> a; b < 0 \<rbrakk> \<Longrightarrow> 0 \<le> (a :: int) smod b"
"\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> (a :: int) smod b \<le> 0"
"\<lbrakk> a \<le> 0; b < 0 \<rbrakk> \<Longrightarrow> b \<le> (a :: int) smod b"
- apply (insert smod_int_range [where a=a and b=b])
- apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
- done
+ using smod_int_range [where a=a and b=b]
+ by (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
lemma smod_mod_positive:
"\<lbrakk> 0 \<le> (a :: int); 0 \<le> b \<rbrakk> \<Longrightarrow> a smod b = a mod b"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Suc_Notation.thy Fri Jan 17 21:30:08 2025 +0100
@@ -0,0 +1,134 @@
+(* Title: HOL/Library/Suc_Notation.thy
+ Author: Manuel Eberl and Tobias Nipkow
+
+Compact notation for nested \<open>Suc\<close> terms. Just notation. Use standard numerals for large numbers.
+*)
+
+theory Suc_Notation
+imports Main
+begin
+
+text \<open>Nested \<open>Suc\<close> terms of depth \<open>2 \<le> n \<le> 9\<close> are abbreviated with new notations \<open>Suc\<^sup>n\<close>:\<close>
+
+abbreviation (input) Suc2 where "Suc2 n \<equiv> Suc (Suc n)"
+abbreviation (input) Suc3 where "Suc3 n \<equiv> Suc (Suc2 n)"
+abbreviation (input) Suc4 where "Suc4 n \<equiv> Suc (Suc3 n)"
+abbreviation (input) Suc5 where "Suc5 n \<equiv> Suc (Suc4 n)"
+abbreviation (input) Suc6 where "Suc6 n \<equiv> Suc (Suc5 n)"
+abbreviation (input) Suc7 where "Suc7 n \<equiv> Suc (Suc6 n)"
+abbreviation (input) Suc8 where "Suc8 n \<equiv> Suc (Suc7 n)"
+abbreviation (input) Suc9 where "Suc9 n \<equiv> Suc (Suc8 n)"
+
+notation Suc2 ("Suc\<^sup>2")
+notation Suc3 ("Suc\<^sup>3")
+notation Suc4 ("Suc\<^sup>4")
+notation Suc5 ("Suc\<^sup>5")
+notation Suc6 ("Suc\<^sup>6")
+notation Suc7 ("Suc\<^sup>7")
+notation Suc8 ("Suc\<^sup>8")
+notation Suc9 ("Suc\<^sup>9")
+
+text \<open>Beyond 9, the syntax \<open>Suc\<^bsup>n\<^esup>\<close> kicks in:\<close>
+
+syntax
+ "_Suc_tower" :: "num_token \<Rightarrow> nat \<Rightarrow> nat" ("Suc\<^bsup>_\<^esup>")
+
+parse_translation \<open>
+ let
+ fun mk_sucs_aux 0 t = t
+ | mk_sucs_aux n t = mk_sucs_aux (n - 1) (\<^const>\<open>Suc\<close> $ t)
+ fun mk_sucs n = Abs("n", \<^typ>\<open>nat\<close>, mk_sucs_aux n (Bound 0))
+
+ fun Suc_tr [Free (str, _)] = mk_sucs (the (Int.fromString str))
+
+ in [(\<^syntax_const>\<open>_Suc_tower\<close>, K Suc_tr)] end
+\<close>
+
+print_translation \<open>
+ let
+ val digit_consts =
+ [\<^const_syntax>\<open>Suc2\<close>, \<^const_syntax>\<open>Suc3\<close>, \<^const_syntax>\<open>Suc4\<close>, \<^const_syntax>\<open>Suc5\<close>,
+ \<^const_syntax>\<open>Suc6\<close>, \<^const_syntax>\<open>Suc7\<close>, \<^const_syntax>\<open>Suc8\<close>, \<^const_syntax>\<open>Suc9\<close>]
+ val num_token_T = Simple_Syntax.read_typ "num_token"
+ val T = num_token_T --> HOLogic.natT --> HOLogic.natT
+ fun mk_num_token n = Free (Int.toString n, num_token_T)
+ fun dest_Suc_tower (Const (\<^const_syntax>\<open>Suc\<close>, _) $ t) acc =
+ dest_Suc_tower t (acc + 1)
+ | dest_Suc_tower t acc = (t, acc)
+
+ fun Suc_tr' [t] =
+ let
+ val (t', n) = dest_Suc_tower t 1
+ in
+ if n > 9 then
+ Const (\<^syntax_const>\<open>_Suc_tower\<close>, T) $ mk_num_token n $ t'
+ else if n > 1 then
+ Const (List.nth (digit_consts, n - 2), T) $ t'
+ else
+ raise Match
+ end
+
+ in [(\<^const_syntax>\<open>Suc\<close>, K Suc_tr')]
+ end
+\<close>
+
+(* Tests
+
+ML \<open>
+local
+ fun mk 0 = \<^term>\<open>x :: nat\<close>
+ | mk n = \<^const>\<open>Suc\<close> $ mk (n - 1)
+ val ctxt' = Variable.add_fixes_implicit @{term "x :: nat"} @{context}
+in
+ val _ =
+ map_range (fn n => (n + 1, mk (n + 1))) 20
+ |> map (fn (n, t) =>
+ Pretty.block [Pretty.str (Int.toString n ^ ": "),
+ Syntax.pretty_term ctxt' t] |> Pretty.writeln)
+end
+\<close>
+
+(* test parsing *)
+term "Suc x"
+term "Suc\<^sup>2 x"
+term "Suc\<^sup>3 x"
+term "Suc\<^sup>4 x"
+term "Suc\<^sup>5 x"
+term "Suc\<^sup>6 x"
+term "Suc\<^sup>7 x"
+term "Suc\<^sup>8 x"
+term "Suc\<^sup>9 x"
+
+term "Suc\<^bsup>2\<^esup> x"
+term "Suc\<^bsup>3\<^esup> x"
+term "Suc\<^bsup>4\<^esup> x"
+term "Suc\<^bsup>5\<^esup> x"
+term "Suc\<^bsup>6\<^esup> x"
+term "Suc\<^bsup>7\<^esup> x"
+term "Suc\<^bsup>8\<^esup> x"
+term "Suc\<^bsup>9\<^esup> x"
+term "Suc\<^bsup>10\<^esup> x"
+term "Suc\<^bsup>11\<^esup> x"
+term "Suc\<^bsup>12\<^esup> x"
+term "Suc\<^bsup>13\<^esup> x"
+term "Suc\<^bsup>14\<^esup> x"
+term "Suc\<^bsup>15\<^esup> x"
+term "Suc\<^bsup>16\<^esup> x"
+term "Suc\<^bsup>17\<^esup> x"
+term "Suc\<^bsup>18\<^esup> x"
+term "Suc\<^bsup>19\<^esup> x"
+term "Suc\<^bsup>20\<^esup> x"
+
+(* check that the notation really means the right thing *)
+lemma "Suc\<^sup>2 n = n+2 \<and> Suc\<^sup>3 n = n+3 \<and> Suc\<^sup>4 n = n+4 \<and> Suc\<^sup>5 n = n+5
+ \<and> Suc\<^sup>6 n = n+6 \<and> Suc\<^sup>7 n = n+7 \<and> Suc\<^sup>8 n = n+8 \<and> Suc\<^sup>9 n = n+9"
+by simp
+
+lemma "Suc\<^bsup>10\<^esup> n = n+10 \<and> Suc\<^bsup>11\<^esup> n = n+11 \<and> Suc\<^bsup>12\<^esup> n = n+12 \<and> Suc\<^bsup>13\<^esup> n = n+13
+ \<and> Suc\<^bsup>14\<^esup> n = n+14 \<and> Suc\<^bsup>15\<^esup> n = n+15 \<and> Suc\<^bsup>16\<^esup> n = n+16 \<and> Suc\<^bsup>17\<^esup> n = n+17
+ \<and> Suc\<^bsup>18\<^esup> n = n+18 \<and> Suc\<^bsup>19\<^esup> n = n+19 \<and> Suc\<^bsup>20\<^esup> n = n+20"
+by simp
+
+*)
+
+end
\ No newline at end of file
--- a/src/HOL/ROOT Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/ROOT Fri Jan 17 21:30:08 2025 +0100
@@ -88,6 +88,7 @@
RBT_Set
(*printing modifications*)
OptionalSugar
+ Suc_Notation
(*prototypic tools*)
Predicate_Compile_Quickcheck
(*legacy tools*)
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jan 17 21:30:08 2025 +0100
@@ -59,6 +59,7 @@
val bd_card_order_of_bnf: bnf -> thm
val bd_cinfinite_of_bnf: bnf -> thm
val bd_regularCard_of_bnf: bnf -> thm
+ val bd_def_of_bnf: bnf -> thm
val collect_set_map_of_bnf: bnf -> thm
val in_bd_of_bnf: bnf -> thm
val in_cong_of_bnf: bnf -> thm
@@ -251,14 +252,15 @@
type defs = {
map_def: thm,
set_defs: thm list,
+ bd_def: thm,
rel_def: thm,
pred_def: thm
}
-fun mk_defs map sets rel pred = {map_def = map, set_defs = sets, rel_def = rel, pred_def = pred};
+fun mk_defs map sets bd rel pred = {map_def = map, bd_def = bd, set_defs = sets, rel_def = rel, pred_def = pred};
-fun map_defs f {map_def, set_defs, rel_def, pred_def} =
- {map_def = f map_def, set_defs = map f set_defs, rel_def = f rel_def, pred_def = f pred_def};
+fun map_defs f {map_def, set_defs, bd_def, rel_def, pred_def} =
+ {map_def = f map_def, set_defs = map f set_defs, bd_def = f bd_def, rel_def = f rel_def, pred_def = f pred_def};
val morph_defs = map_defs o Morphism.thm;
@@ -582,6 +584,7 @@
val bd_card_order_of_bnf = #bd_card_order o #axioms o rep_bnf;
val bd_cinfinite_of_bnf = #bd_cinfinite o #axioms o rep_bnf;
val bd_regularCard_of_bnf = #bd_regularCard o #axioms o rep_bnf;
+val bd_def_of_bnf = #bd_def o #defs o rep_bnf;
val collect_set_map_of_bnf = Lazy.force o #collect_set_map o #facts o rep_bnf;
val in_bd_of_bnf = Lazy.force o #in_bd o #facts o rep_bnf;
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
@@ -1005,8 +1008,10 @@
val notes =
[(mk_def_binding map_of_bnf, map_def_of_bnf bnf),
(mk_def_binding rel_of_bnf, rel_def_of_bnf bnf),
+ (mk_def_binding bd_of_bnf, bd_def_of_bnf bnf),
(mk_def_binding pred_of_bnf, pred_def_of_bnf bnf)] @
@{map 2} (pair o mk_def_binding o K) (sets_of_bnf bnf) (set_defs_of_bnf bnf)
+ |> filter_out (fn (b, thm) => Thm.is_reflexive thm)
|> map (fn (b, thm) => ((b, []), [([thm], [])]));
in
lthy
@@ -2042,7 +2047,7 @@
val inj_map_strong = Lazy.lazy mk_inj_map_strong;
- val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_pred_def;
+ val defs = mk_defs bnf_map_def bnf_set_defs bnf_bd_def bnf_rel_def bnf_pred_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id
--- a/src/HOL/Tools/BNF/bnf_lift.ML Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Fri Jan 17 21:30:08 2025 +0100
@@ -436,7 +436,7 @@
(* get the bnf for RepT *)
val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
- bnf_of_typ true Dont_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
+ bnf_of_typ true Hardly_Inline (Binding.qualify true AbsT_name) flatten_tyargs []
Ds0 RepT ((empty_comp_cache, empty_unfolds), lthy);
val set_bs =
@@ -670,7 +670,7 @@
[card_order_bd_tac, cinfinite_bd_tac, regularCard_bd_tac] @ set_bds_tac @
[le_rel_OO_tac, rel_OO_Grp_tac, pred_set_tac];
- val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+ val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
tactics wit_tac NONE map_b rel_b pred_b set_bs
(((((((Binding.empty, AbsT), map_G), sets_G), bd_G), wits_G), SOME rel_G), SOME pred_G)
lthy;
@@ -852,7 +852,7 @@
map dest_TFree alpha0s |> filter (fn T => exists (fn Ts => member op= Ts T) Ass);
val ((bnf_F, (deads, alphas)), ((_, unfolds), lthy)) =
- bnf_of_typ true Dont_Inline (Binding.qualify true absT_name) flatten_tyargs
+ bnf_of_typ true Hardly_Inline (Binding.qualify true absT_name) flatten_tyargs
[] Ds0 repT ((empty_comp_cache, empty_unfolds), lthy);
val live = length alphas;
val _ = (if live = 0 then error "No live variables" else ());
@@ -1889,7 +1889,7 @@
| mk_wit_tacs [] ws ctxt = mk_wit_tacs set_F'_thmss ws ctxt
| mk_wit_tacs _ _ _ = all_tac;
- val (bnf_G, lthy) = bnf_def Dont_Inline (user_policy Note_Some) true I
+ val (bnf_G, lthy) = bnf_def Hardly_Inline (user_policy Note_Some) true I
tactics (mk_wit_tacs [] wit_thms) NONE map_b rel_b pred_b set_bs
(((((((Binding.empty, absT), map_G), sets_G), bd_G), wits_G), SOME rel_G), NONE) lthy;
--- a/src/HOL/Tools/inductive.ML Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Jan 17 21:30:08 2025 +0100
@@ -21,7 +21,7 @@
signature INDUCTIVE =
sig
type result =
- {preds: term list, elims: thm list, raw_induct: thm,
+ {preds: term list, elims: thm list, raw_induct: thm, def: thm, mono: thm,
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
val transform_result: morphism -> result -> result
type info = {names: string list, coind: bool} * result
@@ -180,17 +180,18 @@
(** context data **)
type result =
- {preds: term list, elims: thm list, raw_induct: thm,
+ {preds: term list, elims: thm list, raw_induct: thm, def: thm, mono: thm,
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
-fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
+fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs, def, mono} =
let
val term = Morphism.term phi;
val thm = Morphism.thm phi;
val fact = Morphism.fact phi;
in
- {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
- induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs}
+ {preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, def = thm def,
+ induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs,
+ mono = thm mono}
end;
type info = {names: string list, coind: bool} * result;
@@ -1152,6 +1153,8 @@
raw_induct = rulify lthy3 raw_induct,
induct = induct,
inducts = inducts,
+ def = fp_def,
+ mono = mono,
eqs = eqs'};
val lthy4 = lthy3
--- a/src/HOL/Tools/inductive_set.ML Fri Jan 17 20:30:01 2025 +0100
+++ b/src/HOL/Tools/inductive_set.ML Fri Jan 17 21:30:08 2025 +0100
@@ -463,7 +463,7 @@
eta_contract (member op = cs' orf is_pred pred_arities))) intros;
val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
val monos' = map (to_pred [] (Context.Proof lthy)) monos;
- val ({preds, intrs, elims, raw_induct, eqs, ...}, lthy1) =
+ val ({preds, intrs, elims, raw_induct, eqs, def, mono, ...}, lthy1) =
Inductive.add_ind_def
{quiet_mode = quiet_mode, verbose = verbose, alt_name = Binding.empty,
coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
@@ -513,7 +513,7 @@
(map (to_set [] (Context.Proof lthy3)) eqs) raw_induct' lthy3;
in
({intrs = intrs', elims = elims', induct = induct, inducts = inducts,
- raw_induct = raw_induct', preds = map fst defs, eqs = eqs'},
+ raw_induct = raw_induct', preds = map fst defs, eqs = eqs', def = def, mono = mono},
lthy4)
end;
--- a/src/Pure/Build/build_schedule.scala Fri Jan 17 20:30:01 2025 +0100
+++ b/src/Pure/Build/build_schedule.scala Fri Jan 17 21:30:08 2025 +0100
@@ -69,14 +69,16 @@
}
def load(
+ build_options: Options,
host_infos: Host_Infos,
log_database: SQL.Database,
sessions_structure: Sessions.Structure
): Timing_Data = {
+ val days = build_options.int("build_schedule_history")
val build_history =
for {
log_name <- log_database.execute_query_statement(
- Build_Log.private_data.meta_info_table.select(List(Build_Log.Column.log_name)),
+ Build_Log.private_data.select_recent_log_names(days),
List.from[String], res => res.string(Build_Log.Column.log_name))
meta_info <- Build_Log.private_data.read_meta_info(log_database, log_name)
build_info = Build_Log.private_data.read_build_info(log_database, log_name)
@@ -1065,9 +1067,8 @@
Host_Infos.load(build_options, build_hosts, _host_database)
}
- private val timing_data: Timing_Data = {
- Timing_Data.load(_host_infos, _log_database, build_context.sessions_structure)
- }
+ private val timing_data: Timing_Data =
+ Timing_Data.load(build_options, _host_infos, _log_database, build_context.sessions_structure)
private var _scheduler = init_scheduler(timing_data)
@@ -1108,6 +1109,7 @@
val props =
List(
Build_Log.Prop.build_id.name -> build_context.build_uuid,
+ Build_Log.Prop.isabelle_version.name -> Isabelle_System.isabelle_id(),
Build_Log.Prop.build_engine.name -> build_context.engine.name,
Build_Log.Prop.build_host.name -> hostname,
Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start))
@@ -1261,7 +1263,7 @@
def read_serial(db: SQL.Database, build_uuid: String = ""): Long =
db.execute_query_statementO[Long](
- Schedules.table.select(List(Schedules.serial.max), sql =
+ Schedules.table.select(List(Schedules.serial.max), sql =
SQL.where(if_proper(build_uuid, Schedules.build_uuid.equal(build_uuid)))),
_.long(Schedules.serial)).getOrElse(0L)
@@ -1373,7 +1375,7 @@
schedule.generator != old_schedule.generator ||
schedule.start != old_schedule.start ||
schedule.graph != old_schedule.graph
-
+
val schedule1 =
if (changed) schedule.copy(serial = old_schedule.next_serial) else schedule
if (schedule1.serial != schedule.serial) write_schedule(db, schedule1)
@@ -1525,7 +1527,7 @@
}
val host_infos = Host_Infos.load(build_options, cluster_hosts, host_database)
- val timing_data = Timing_Data.load(host_infos, log_database, full_sessions)
+ val timing_data = Timing_Data.load(build_options, host_infos, log_database, full_sessions)
val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
--- a/src/Pure/General/mercurial.scala Fri Jan 17 20:30:01 2025 +0100
+++ b/src/Pure/General/mercurial.scala Fri Jan 17 21:30:08 2025 +0100
@@ -117,6 +117,9 @@
/* hg_sync meta data */
+ def sync_id(root: Path, ssh: SSH.System = SSH.Local): Option[String] =
+ if (Hg_Sync.ok(root, ssh)) Some(Hg_Sync.directory(root, ssh).id) else None
+
object Hg_Sync {
val NAME = ".hg_sync"
val _NAME: String = " " + NAME
--- a/src/Pure/System/isabelle_system.scala Fri Jan 17 20:30:01 2025 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Jan 17 21:30:08 2025 +0100
@@ -100,7 +100,8 @@
def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
getetc("ISABELLE_ID", root = root) orElse
Mercurial.archive_id(root) orElse
- Mercurial.id_repository(root, rev = "") getOrElse
+ Mercurial.id_repository(root, rev = "") orElse
+ Mercurial.sync_id(root) getOrElse
error("Failed to identify Isabelle distribution " + root.expand)
object Isabelle_Id extends Scala.Fun_String("isabelle_id") {