diff --git a/metadata/entries/IEEE_Floating_Point.toml b/metadata/entries/IEEE_Floating_Point.toml
--- a/metadata/entries/IEEE_Floating_Point.toml
+++ b/metadata/entries/IEEE_Floating_Point.toml
@@ -1,39 +1,53 @@
title = "A Formal Model of IEEE Floating Point Arithmetic"
date = 2013-07-27
topics = [
"Computer science/Data structures",
]
abstract = "This development provides a formal model of IEEE-754 floating-point arithmetic. This formalization, including formal specification of the standard and proofs of important properties of floating-point arithmetic, forms the foundation for verifying programs with floating-point computation. There is also a code generation setup for floats so that we can execute programs using this formalization in functional programming languages."
license = "bsd"
note = ""
[authors]
[authors.yu]
email = "yu_email"
[contributors]
[contributors.hellauer]
email = "hellauer_email"
[contributors.immler]
homepage = "immler_homepage"
+[contributors.weber]
+email = "weber_email"
+
[notify]
paulson = "paulson_email"
immler = "immler_email"
+weber = "weber_email"
[history]
2017-09-25 = """
Added conversions from and to software floating point numbers
(by Fabian Hellauer and Fabian Immler).
"""
2018-02-05 = """
'Modernized' representation following the formalization in HOL4:
former \"float_format\" and predicate \"is_valid\" is now encoded in a type \"('e, 'f) float\" where
-'e and 'f encode the size of exponent and fraction."""
+'e and 'f encode the size of exponent and fraction.
+"""
+2023-05-10 = """
+Added the IEEE rounding mode \"roundNearestTiesToAway\".
+"""
+2023-05-22 = """
+Added a model of floating-point arithmetic with a single NaN value.
+"""
+2023-05-22 = """
+Added a translation of floating-point arithmetic into SMT-LIB.
+"""
[extra]
[related]
diff --git a/thys/Registers/Finite_Tensor_Product_Matrices.thy b/thys/Registers/Finite_Tensor_Product_Matrices.thy
--- a/thys/Registers/Finite_Tensor_Product_Matrices.thy
+++ b/thys/Registers/Finite_Tensor_Product_Matrices.thy
@@ -1,250 +1,251 @@
section \Tensor products as matrices\
theory Finite_Tensor_Product_Matrices
imports Finite_Tensor_Product
begin
definition tensor_pack :: "nat \ nat \ (nat \ nat) \ nat"
where "tensor_pack X Y = (\(x, y). x * Y + y)"
definition tensor_unpack :: "nat \ nat \ nat \ (nat \ nat)"
where "tensor_unpack X Y xy = (xy div Y, xy mod Y)"
lemma tensor_unpack_inj:
assumes "i < A * B" and "j < A * B"
shows "tensor_unpack A B i = tensor_unpack A B j \ i = j"
by (metis div_mult_mod_eq prod.sel(1) prod.sel(2) tensor_unpack_def)
lemma tensor_unpack_bound1[simp]: "i < A * B \ fst (tensor_unpack A B i) < A"
unfolding tensor_unpack_def
apply auto
using less_mult_imp_div_less by blast
lemma tensor_unpack_bound2[simp]: "i < A * B \ snd (tensor_unpack A B i) < B"
unfolding tensor_unpack_def
apply auto
by (metis mod_less_divisor mult.commute mult_zero_left nat_neq_iff not_less0)
lemma tensor_unpack_fstfst: \fst (tensor_unpack A B (fst (tensor_unpack (A * B) C i)))
= fst (tensor_unpack A (B * C) i)\
unfolding tensor_unpack_def apply auto
by (metis div_mult2_eq mult.commute)
lemma tensor_unpack_sndsnd: \snd (tensor_unpack B C (snd (tensor_unpack A (B * C) i)))
= snd (tensor_unpack (A * B) C i)\
unfolding tensor_unpack_def apply auto
by (meson dvd_triv_right mod_mod_cancel)
lemma tensor_unpack_fstsnd: \fst (tensor_unpack B C (snd (tensor_unpack A (B * C) i)))
= snd (tensor_unpack A B (fst (tensor_unpack (A * B) C i)))\
unfolding tensor_unpack_def apply auto
by (cases \C = 0\) (simp_all add: mult.commute [of B C] mod_mult2_eq [of i C B])
definition "tensor_state_jnf \ \ = (let d1 = dim_vec \ in let d2 = dim_vec \ in
vec (d1*d2) (\i. let (i1,i2) = tensor_unpack d1 d2 i in (vec_index \ i1) * (vec_index \ i2)))"
lemma tensor_state_jnf_dim[simp]: \dim_vec (tensor_state_jnf \ \) = dim_vec \ * dim_vec \\
unfolding tensor_state_jnf_def Let_def by simp
lemma enum_prod_nth_tensor_unpack:
assumes \i < CARD('a) * CARD('b)\
shows "(Enum.enum ! i :: 'a::enum\'b::enum) =
(let (i1,i2) = tensor_unpack CARD('a) CARD('b) i in
(Enum.enum ! i1, Enum.enum ! i2))"
using assms
by (simp add: enum_prod_def card_UNIV_length_enum product_nth tensor_unpack_def)
lemma vec_of_basis_enum_tensor_state_index:
fixes \ :: \'a::enum ell2\ and \ :: \'b::enum ell2\
assumes [simp]: \i < CARD('a) * CARD('b)\
shows \vec_of_basis_enum (\ \\<^sub>s \) $ i = (let (i1,i2) = tensor_unpack CARD('a) CARD('b) i in
vec_of_basis_enum \ $ i1 * vec_of_basis_enum \ $ i2)\
proof -
define i1 i2 where "i1 = fst (tensor_unpack CARD('a) CARD('b) i)"
and "i2 = snd (tensor_unpack CARD('a) CARD('b) i)"
have [simp]: "i1 < CARD('a)" "i2 < CARD('b)"
using assms i1_def tensor_unpack_bound1 apply presburger
using assms i2_def tensor_unpack_bound2 by presburger
have \vec_of_basis_enum (\ \\<^sub>s \) $ i = Rep_ell2 (\ \\<^sub>s \) (enum_class.enum ! i)\
by (simp add: vec_of_basis_enum_ell2_component)
also have \\ = Rep_ell2 \ (Enum.enum!i1) * Rep_ell2 \ (Enum.enum!i2)\
apply (transfer fixing: i i1 i2)
by (simp add: enum_prod_nth_tensor_unpack case_prod_beta i1_def i2_def)
also have \\ = vec_of_basis_enum \ $ i1 * vec_of_basis_enum \ $ i2\
by (simp add: vec_of_basis_enum_ell2_component)
finally show ?thesis
by (simp add: case_prod_beta i1_def i2_def)
qed
lemma vec_of_basis_enum_tensor_state:
fixes \ :: \'a::enum ell2\ and \ :: \'b::enum ell2\
shows \vec_of_basis_enum (\ \\<^sub>s \) = tensor_state_jnf (vec_of_basis_enum \) (vec_of_basis_enum \)\
apply (rule eq_vecI, simp_all)
apply (subst vec_of_basis_enum_tensor_state_index, simp_all)
by (simp add: tensor_state_jnf_def case_prod_beta Let_def)
lemma mat_of_cblinfun_tensor_op_index:
fixes a :: \'a::enum ell2 \\<^sub>C\<^sub>L 'b::enum ell2\ and b :: \'c::enum ell2 \\<^sub>C\<^sub>L 'd::enum ell2\
assumes [simp]: \i < CARD('b) * CARD('d)\
assumes [simp]: \j < CARD('a) * CARD('c)\
shows \mat_of_cblinfun (tensor_op a b) $$ (i,j) =
(let (i1,i2) = tensor_unpack CARD('b) CARD('d) i in
let (j1,j2) = tensor_unpack CARD('a) CARD('c) j in
mat_of_cblinfun a $$ (i1,j1) * mat_of_cblinfun b $$ (i2,j2))\
proof -
define i1 i2 j1 j2
where "i1 = fst (tensor_unpack CARD('b) CARD('d) i)"
and "i2 = snd (tensor_unpack CARD('b) CARD('d) i)"
and "j1 = fst (tensor_unpack CARD('a) CARD('c) j)"
and "j2 = snd (tensor_unpack CARD('a) CARD('c) j)"
have [simp]: "i1 < CARD('b)" "i2 < CARD('d)" "j1 < CARD('a)" "j2 < CARD('c)"
using assms i1_def tensor_unpack_bound1 apply presburger
using assms i2_def tensor_unpack_bound2 apply blast
using assms(2) j1_def tensor_unpack_bound1 apply blast
using assms(2) j2_def tensor_unpack_bound2 by presburger
have \mat_of_cblinfun (tensor_op a b) $$ (i,j)
= Rep_ell2 (tensor_op a b *\<^sub>V ket (Enum.enum!j)) (Enum.enum ! i)\
by (simp add: mat_of_cblinfun_ell2_component)
also have \\ = Rep_ell2 ((a *\<^sub>V ket (Enum.enum!j1)) \\<^sub>s (b *\<^sub>V ket (Enum.enum!j2))) (Enum.enum!i)\
by (simp add: tensor_op_ell2 enum_prod_nth_tensor_unpack[where i=j] Let_def case_prod_beta j1_def[symmetric] j2_def[symmetric] flip: tensor_ell2_ket)
also have \\ = vec_of_basis_enum ((a *\<^sub>V ket (Enum.enum!j1)) \\<^sub>s b *\<^sub>V ket (Enum.enum!j2)) $ i\
by (simp add: vec_of_basis_enum_ell2_component)
also have \\ = vec_of_basis_enum (a *\<^sub>V ket (enum_class.enum ! j1)) $ i1 *
vec_of_basis_enum (b *\<^sub>V ket (enum_class.enum ! j2)) $ i2\
by (simp add: case_prod_beta vec_of_basis_enum_tensor_state_index i1_def[symmetric] i2_def[symmetric])
also have \\ = Rep_ell2 (a *\<^sub>V ket (enum_class.enum ! j1)) (enum_class.enum ! i1) *
Rep_ell2 (b *\<^sub>V ket (enum_class.enum ! j2)) (enum_class.enum ! i2)\
by (simp add: vec_of_basis_enum_ell2_component)
also have \\ = mat_of_cblinfun a $$ (i1, j1) * mat_of_cblinfun b $$ (i2, j2)\
by (simp add: mat_of_cblinfun_ell2_component)
finally show ?thesis
by (simp add: i1_def[symmetric] i2_def[symmetric] j1_def[symmetric] j2_def[symmetric] case_prod_beta)
qed
definition "tensor_op_jnf A B =
(let r1 = dim_row A in
let c1 = dim_col A in
let r2 = dim_row B in
let c2 = dim_col B in
mat (r1 * r2) (c1 * c2)
(\(i,j). let (i1,i2) = tensor_unpack r1 r2 i in
let (j1,j2) = tensor_unpack c1 c2 j in
(A $$ (i1,j1)) * (B $$ (i2,j2))))"
lemma tensor_op_jnf_dim[simp]:
\dim_row (tensor_op_jnf a b) = dim_row a * dim_row b\
\dim_col (tensor_op_jnf a b) = dim_col a * dim_col b\
unfolding tensor_op_jnf_def Let_def by simp_all
lemma mat_of_cblinfun_tensor_op:
fixes a :: \'a::enum ell2 \\<^sub>C\<^sub>L 'b::enum ell2\ and b :: \'c::enum ell2 \\<^sub>C\<^sub>L 'd::enum ell2\
shows \mat_of_cblinfun (tensor_op a b) = tensor_op_jnf (mat_of_cblinfun a) (mat_of_cblinfun b)\
apply (rule eq_matI, simp_all add: )
- apply (subst mat_of_cblinfun_tensor_op_index, simp_all)
- by (simp add: tensor_op_jnf_def case_prod_beta Let_def)
+ apply (subst mat_of_cblinfun_tensor_op_index)
+ apply (simp_all add: canonical_basis_length)
+ by (simp add: tensor_op_jnf_def case_prod_beta Let_def canonical_basis_length)
lemma mat_of_cblinfun_assoc_ell2'[simp]:
\mat_of_cblinfun (assoc_ell2' :: (('a::enum\('b::enum\'c::enum)) ell2 \\<^sub>C\<^sub>L _)) = one_mat (CARD('a)*CARD('b)*CARD('c))\
(is "mat_of_cblinfun ?assoc = _")
proof (rule mat_eq_iff[THEN iffD2], intro conjI allI impI)
show \dim_row (mat_of_cblinfun ?assoc) =
dim_row (1\<^sub>m (CARD('a) * CARD('b) * CARD('c)))\
- by (simp)
+ by (simp add: canonical_basis_length)
show \dim_col (mat_of_cblinfun ?assoc) =
dim_col (1\<^sub>m (CARD('a) * CARD('b) * CARD('c)))\
- by (simp)
+ by (simp add: canonical_basis_length)
fix i j
let ?i = "Enum.enum ! i :: (('a\'b)\'c)" and ?j = "Enum.enum ! j :: ('a\('b\'c))"
assume \i < dim_row (1\<^sub>m (CARD('a) * CARD('b) * CARD('c)))\
then have iB[simp]: \i < CARD('a) * CARD('b) * CARD('c)\ by simp
then have iB'[simp]: \i < CARD('a) * (CARD('b) * CARD('c))\ by linarith
assume \j < dim_col (1\<^sub>m (CARD('a) * CARD('b) * CARD('c)))\
then have jB[simp]: \j < CARD('a) * CARD('b) * CARD('c)\ by simp
then have jB'[simp]: \j < CARD('a) * (CARD('b) * CARD('c))\ by linarith
define i1 i23 i2 i3
where "i1 = fst (tensor_unpack CARD('a) (CARD('b)*CARD('c)) i)"
and "i23 = snd (tensor_unpack CARD('a) (CARD('b)*CARD('c)) i)"
and "i2 = fst (tensor_unpack CARD('b) CARD('c) i23)"
and "i3 = snd (tensor_unpack CARD('b) CARD('c) i23)"
define j12 j1 j2 j3
where "j12 = fst (tensor_unpack (CARD('a)*CARD('b)) CARD('c) j)"
and "j1 = fst (tensor_unpack CARD('a) CARD('b) j12)"
and "j2 = snd (tensor_unpack CARD('a) CARD('b) j12)"
and "j3 = snd (tensor_unpack (CARD('a)*CARD('b)) CARD('c) j)"
have [simp]: "j12 < CARD('a)*CARD('b)" "i23 < CARD('b)*CARD('c)"
using j12_def jB tensor_unpack_bound1 apply presburger
using i23_def iB' tensor_unpack_bound2 by blast
have j1': \fst (tensor_unpack CARD('a) (CARD('b) * CARD('c)) j) = j1\
by (simp add: j1_def j12_def tensor_unpack_fstfst)
let ?i1 = "Enum.enum ! i1 :: 'a" and ?i2 = "Enum.enum ! i2 :: 'b" and ?i3 = "Enum.enum ! i3 :: 'c"
let ?j1 = "Enum.enum ! j1 :: 'a" and ?j2 = "Enum.enum ! j2 :: 'b" and ?j3 = "Enum.enum ! j3 :: 'c"
have i: \?i = ((?i1,?i2),?i3)\
by (auto simp add: enum_prod_nth_tensor_unpack case_prod_beta
tensor_unpack_fstfst tensor_unpack_fstsnd tensor_unpack_sndsnd i1_def i2_def i23_def i3_def)
have j: \?j = (?j1,(?j2,?j3))\
by (auto simp add: enum_prod_nth_tensor_unpack case_prod_beta
tensor_unpack_fstfst tensor_unpack_fstsnd tensor_unpack_sndsnd j1_def j2_def j12_def j3_def)
have ijeq: \(?i1,?i2,?i3) = (?j1,?j2,?j3) \ i = j\
unfolding i1_def i2_def i3_def j1_def j2_def j3_def apply simp
apply (subst enum_inj, simp, simp)
apply (subst enum_inj, simp, simp)
apply (subst enum_inj, simp, simp)
apply (subst tensor_unpack_inj[symmetric, where i=i and j=j and A="CARD('a)" and B="CARD('b)*CARD('c)"], simp, simp)
unfolding prod_eq_iff
apply (subst tensor_unpack_inj[symmetric, where i=\snd (tensor_unpack CARD('a) (CARD('b) * CARD('c)) i)\ and A="CARD('b)" and B="CARD('c)"], simp, simp)
by (simp add: i1_def[symmetric] j1_def[symmetric] i2_def[symmetric] j2_def[symmetric] i3_def[symmetric] j3_def[symmetric]
i23_def[symmetric] j12_def[symmetric] j1'
prod_eq_iff tensor_unpack_fstsnd tensor_unpack_sndsnd)
have \mat_of_cblinfun ?assoc $$ (i, j) = Rep_ell2 (assoc_ell2' *\<^sub>V ket ?j) ?i\
by (subst mat_of_cblinfun_ell2_component, auto)
also have \\ = Rep_ell2 ((ket ?j1 \\<^sub>s ket ?j2) \\<^sub>s ket ?j3) ?i\
by (simp add: j assoc_ell2'_tensor flip: tensor_ell2_ket)
also have \\ = (if (?i1,?i2,?i3) = (?j1,?j2,?j3) then 1 else 0)\
by (auto simp add: ket.rep_eq i)
also have \\ = (if i=j then 1 else 0)\
using ijeq by simp
finally
show \mat_of_cblinfun ?assoc $$ (i, j) =
1\<^sub>m (CARD('a) * CARD('b) * CARD('c)) $$ (i, j)\
by auto
qed
lemma assoc_ell2'_inv: "assoc_ell2 o\<^sub>C\<^sub>L assoc_ell2' = id_cblinfun"
apply (rule equal_ket, case_tac x, hypsubst)
by (simp flip: tensor_ell2_ket add: cblinfun_apply_cblinfun_compose assoc_ell2'_tensor assoc_ell2_tensor)
lemma assoc_ell2_inv: "assoc_ell2' o\<^sub>C\<^sub>L assoc_ell2 = id_cblinfun"
apply (rule equal_ket, case_tac x, hypsubst)
by (simp flip: tensor_ell2_ket add: cblinfun_apply_cblinfun_compose assoc_ell2'_tensor assoc_ell2_tensor)
lemma mat_of_cblinfun_assoc_ell2[simp]:
\mat_of_cblinfun (assoc_ell2 :: ((('a::enum\'b::enum)\'c::enum) ell2 \\<^sub>C\<^sub>L _)) = one_mat (CARD('a)*CARD('b)*CARD('c))\
(is "mat_of_cblinfun ?assoc = _")
proof -
let ?assoc' = "assoc_ell2' :: (('a::enum\('b::enum\'c::enum)) ell2 \\<^sub>C\<^sub>L _)"
have "one_mat (CARD('a)*CARD('b)*CARD('c)) = mat_of_cblinfun (?assoc o\<^sub>C\<^sub>L ?assoc')"
by (simp add: mult.assoc mat_of_cblinfun_id)
also have \\ = mat_of_cblinfun ?assoc * mat_of_cblinfun ?assoc'\
using mat_of_cblinfun_compose by blast
also have \\ = mat_of_cblinfun ?assoc * one_mat (CARD('a)*CARD('b)*CARD('c))\
by simp
also have \\ = mat_of_cblinfun ?assoc\
apply (rule right_mult_one_mat')
- by (simp)
+ by (simp add: canonical_basis_length)
finally show ?thesis
by simp
qed
end