-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathCblinfun_Code_Examples.thy
119 lines (64 loc) · 2.97 KB
/
Cblinfun_Code_Examples.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
section \<open>\<open>Cblinfun_Code_Examples\<close> -- Examples and test cases for code generation\<close>
theory Cblinfun_Code_Examples
imports
"Complex_Bounded_Operators-Extra.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 "\<squnion>\<index>" 65)
no_notation Lattice.meet (infixl "\<sqinter>\<index>" 70)
unbundle cblinfun_notation
section \<open>Examples\<close>
subsection \<open>Operators\<close>
value "id_cblinfun :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
value "1 :: unit ell2 \<Rightarrow>\<^sub>C\<^sub>L unit ell2"
value "id_cblinfun + id_cblinfun :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
value "0 :: (bool ell2 \<Rightarrow>\<^sub>C\<^sub>L Enum.finite_3 ell2)"
value "- id_cblinfun :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
value "id_cblinfun - id_cblinfun :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
value "classical_operator (\<lambda>b. Some (\<not> b))"
value "id_cblinfun = (0 :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2)"
value "2 *\<^sub>R id_cblinfun :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
value "imaginary_unit *\<^sub>C id_cblinfun :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
value "id_cblinfun o\<^sub>C\<^sub>L 0 :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
value "id_cblinfun* :: bool ell2 \<Rightarrow>\<^sub>C\<^sub>L bool ell2"
subsection \<open>Vectors\<close>
value "0 :: bool ell2"
value "1 :: unit ell2"
value "ket False"
value "2 *\<^sub>C ket False"
value "2 *\<^sub>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 \<open>Vector/Matrix\<close>
value "id_cblinfun *\<^sub>V ket True"
value \<open>vector_to_cblinfun (ket True) :: unit ell2 \<Rightarrow>\<^sub>C\<^sub>L _\<close>
subsection \<open>Subspaces\<close>
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} \<squnion> ccspan {ket True}"
value "ccspan {ket False} + ccspan {ket True}"
value "ccspan {ket False} \<sqinter> ccspan {ket True}"
value "id_cblinfun *\<^sub>S ccspan {ket False}"
value "id_cblinfun *\<^sub>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} \<le> 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