--- a/src/HOL/Code_Numeral.thy Wed Jan 01 19:24:00 2025 +0100
+++ b/src/HOL/Code_Numeral.thy Wed Jan 01 19:42:53 2025 +0100
@@ -872,26 +872,6 @@
and (Haskell) "Prelude.abs"
and (Scala) "_.abs"
and (Eval) "abs"
-| constant "Bit_Operations.and :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
- (SML) "IntInf.andb ((_),/ (_))"
- and (OCaml) "Z.logand"
- and (Haskell) infixl 7 ".&."
- and (Scala) infixl 3 "&"
-| constant "Bit_Operations.or :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
- (SML) "IntInf.orb ((_),/ (_))"
- and (OCaml) "Z.logor"
- and (Haskell) infixl 5 ".|."
- and (Scala) infixl 1 "|"
-| constant "Bit_Operations.xor :: integer \<Rightarrow> integer \<Rightarrow> integer" \<rightharpoonup>
- (SML) "IntInf.xorb ((_),/ (_))"
- and (OCaml) "Z.logxor"
- and (Haskell) infixl 6 ".^."
- and (Scala) infixl 2 "^"
-| constant "Bit_Operations.not :: integer \<Rightarrow> integer" \<rightharpoonup>
- (SML) "IntInf.notb"
- and (OCaml) "Z.lognot"
- and (Haskell) "Data.Bits.complement"
- and (Scala) "_.unary'_~"
code_identifier
code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
--- a/src/HOL/Data_Structures/Heaps.thy Wed Jan 01 19:24:00 2025 +0100
+++ b/src/HOL/Data_Structures/Heaps.thy Wed Jan 01 19:42:53 2025 +0100
@@ -25,8 +25,11 @@
fun is_empty :: "'a tree \<Rightarrow> bool" where
"is_empty t = (t = Leaf)"
+fun get_min :: "'a tree \<Rightarrow> 'a" where
+"get_min (Node l a r) = a"
+
sublocale Priority_Queue where empty = empty and is_empty = is_empty and insert = insert
-and get_min = "value" and del_min = del_min and invar = heap and mset = mset_tree
+and get_min = get_min and del_min = del_min and invar = heap and mset = mset_tree
proof (standard, goal_cases)
case 1 thus ?case by (simp add: empty_def)
next
@@ -34,7 +37,7 @@
next
case 3 thus ?case by(simp add: mset_insert)
next
- case 4 thus ?case by(simp add: mset_del_min)
+ case 4 thus ?case by(auto simp add: mset_del_min neq_Leaf_iff)
next
case 5 thus ?case by(auto simp: neq_Leaf_iff Min_insert2 simp del: Un_iff)
next
@@ -74,8 +77,11 @@
case (4 q) thus ?case by (cases q)(auto simp: invar_merge)
qed
+lemmas local_empty_def = local.empty_def
+lemmas local_get_min_def = local.get_min.simps
+
sublocale PQM: Priority_Queue_Merge where empty = empty and is_empty = is_empty and insert = insert
-and get_min = "value" and del_min = del_min and invar = heap and mset = mset_tree and merge = merge
+and get_min = get_min and del_min = del_min and invar = heap and mset = mset_tree and merge = merge
proof(standard, goal_cases)
case 1 thus ?case by (simp add: mset_merge)
next
--- a/src/HOL/IMP/Live_True.thy Wed Jan 01 19:24:00 2025 +0100
+++ b/src/HOL/IMP/Live_True.thy Wed Jan 01 19:42:53 2025 +0100
@@ -33,7 +33,7 @@
lemma mono_union_L:
"mono (\<lambda>Y. X \<union> L c Y)"
-by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono)
+using L_mono unfolding mono_def by (metis (no_types) order_eq_iff set_eq_subset sup_mono)
lemma L_While_unfold:
"L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)"
--- a/src/Tools/Code/code_haskell.ML Wed Jan 01 19:24:00 2025 +0100
+++ b/src/Tools/Code/code_haskell.ML Wed Jan 01 19:42:53 2025 +0100
@@ -330,10 +330,6 @@
("Maybe", ["Nothing", "Just"])
];
-val data_bits_import_operators = [
- ".&.", ".|.", ".^."
-];
-
fun serialize_haskell module_prefix string_classes ctxt { module_name,
reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
let
@@ -383,10 +379,7 @@
enclose "import Prelude (" ");" (commas (map str
(map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
@ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
- :: enclose "import Data.Bits (" ");" (commas
- (map (str o Library.enclose "(" ")") data_bits_import_operators))
:: print_qualified_import "Prelude"
- :: print_qualified_import "Data.Bits"
:: map (print_qualified_import o fst) includes;
fun print_module module_name (gr, imports) =
let