Theory Cblinfun_Code_Examples

section ‹‹Cblinfun_Code_Examples› -- Examples and test cases for code generation›

theory Cblinfun_Code_Examples
  imports
    "Complex_Bounded_Operators.Extra_Pretty_Code_Examples"
    Jordan_Normal_Form.Matrix_Impl
    "HOL-Library.Code_Target_Numeral"
    Cblinfun_Code
begin

hide_const (open) Order.bottom Order.top
no_notation Lattice.join (infixl "⊔ı" 65)
no_notation Lattice.meet (infixl "⊓ı" 70)

unbundle lattice_syntax
unbundle cblinfun_notation

section ‹Examples›

subsection ‹Operators›

value "id_cblinfun :: bool ell2 ⇒⇩C⇩L bool ell2"

value "1 :: unit ell2 ⇒⇩C⇩L unit ell2"

value "id_cblinfun + id_cblinfun :: bool ell2 ⇒⇩C⇩L bool ell2"

value "0 :: (bool ell2 ⇒⇩C⇩L Enum.finite_3 ell2)"

value "- id_cblinfun :: bool ell2 ⇒⇩C⇩L bool ell2"

value "id_cblinfun - id_cblinfun :: bool ell2 ⇒⇩C⇩L bool ell2"

value "classical_operator (λb. Some (¬ b))"

value ‹explicit_cblinfun (λx y :: bool. of_bool (x ∧ y))›

value "id_cblinfun = (0 :: bool ell2 ⇒⇩C⇩L bool ell2)"

value "2 *⇩R id_cblinfun :: bool ell2 ⇒⇩C⇩L bool ell2"

value "imaginary_unit *⇩C id_cblinfun :: bool ell2 ⇒⇩C⇩L bool ell2"

value "id_cblinfun o⇩C⇩L 0 :: bool ell2 ⇒⇩C⇩L bool ell2"

value "id_cblinfun* :: bool ell2 ⇒⇩C⇩L bool ell2"

subsection ‹Vectors›

value "0 :: bool ell2"

value "1 :: unit ell2"

value "ket False"

value "2 *⇩C ket False"

value "2 *⇩R ket False"

value "ket True + ket False"

value "ket True - ket True"

value "ket True = ket True"

value "- ket True"

value "cinner (ket True) (ket True)"

value "norm (ket True)"

value "ket () * ket ()"

value "1 :: unit ell2"

value "(1::unit ell2) * (1::unit ell2)"

subsection ‹Vector/Matrix›

value "id_cblinfun *⇩V ket True"

value ‹vector_to_cblinfun (ket True) :: unit ell2 ⇒⇩C⇩L _›

subsection ‹Subspaces›

value "ccspan {ket False}"

value "Proj (ccspan {ket False})"

value "top :: bool ell2 ccsubspace"

value "bot :: bool ell2 ccsubspace"

value "0 :: bool ell2 ccsubspace"

value "ccspan {ket False} ⊔ ccspan {ket True}"

value "ccspan {ket False} + ccspan {ket True}"

value "ccspan {ket False} ⊓ ccspan {ket True}"

value "id_cblinfun *⇩S ccspan {ket False}"

value "id_cblinfun *⇩S (top :: bool ell2 ccsubspace)" (* Special case, using range_cblinfun_code for efficiency *)

value "- ccspan {ket False}"

value "ccspan {ket False, ket True} = top"

value "ccspan {ket False} ≤ ccspan {ket True}"

value "cblinfun_image id_cblinfun (ccspan {ket True})"

value "kernel id_cblinfun :: bool ell2 ccsubspace"

value "eigenspace 1 id_cblinfun :: bool ell2 ccsubspace"

value "Inf {ccspan {ket False}, top}"

value "Sup {ccspan {ket False}, top}"

end