Quelle  Misc.thy

section ‹Miscellaneous facts›

text ‹This theory proves various facts that are not directly related to this developments
  do not occur in the imported theories.›

theory Misc
  imports
    Complex_Bounded_Operators.Cblinfun_Code
    "HOL-Library.Z2"
    Jordan_Normal_Form.Matrix
    Hilbert_Space_Tensor_Product.Weak_Star_Topology
begin

― ‹Remove notation that collides with the notation we use›
no_notation Order.top ("⊤🍋")
unbundle no m_inv_syntax
unbundle no vec_syntax
unbundle no inner_syntax

― ‹Import notation from Bounded Operator and Jordan Normal Form libraries›
unbundle cblinfun_syntax
unbundle jnf_syntax

(* abbreviation "butterfly (ket i) (ket j) \<equiv> butterfly (ket i) (ket j)" *)
(* abbreviation "butterfly (ket i) (ket i) \<equiv> butterfly (ket i) (ket i)" *)

text ‹The following declares the ML antiquotation 🍋‹fact›. In ML code,
 🍋‹@{fact f}› for a theorem/fact name f is replaced by an ML string
 containing a printable(!) representation of fact. (I.e.,
 if you print that string using writeln, the user can ctrl-click on it.)

 This is useful when constructing diagnostic messages in ML code, e.g.,
 🍋‹"Use the theorem " ^ @{fact thmname} ^ "here."››

setup ‹ML_Antiquotation.inline_embedded 🍋‹fact›
 (Args.context -- Scan.lift Args.name_position) >> (fn (ctxt,namepos) => let
 val facts = Proof_Context.facts_of ctxt
 val fullname = Facts.check (Context.Proof ctxt) facts namepos
 val (markup, shortname) = Proof_Context.markup_extern_fact ctxt fullname
 val string = Markup.markups markup shortname
 in ML_Syntax.print_string string end
 )
 ›


instantiation bit :: enum begin
definition "enum_bit = [0::bit,1]"
definition "enum_all_bit P ⟷ P (0::bit) ∧ P 1"
definition "enum_ex_bit P ⟷ P (0::bit) ∨ P 1"
instance
proof intro_classes
  show ‹(UNIV :: bit set) = set enum_class.enum›
    by (auto simp: enum_bit_def)
  show ‹distinct (enum_class.enum :: bit list)›
    by (auto simp: enum_bit_def)
  show ‹enum_class.enum_all P = Ball UNIV P› for P :: ‹bit ==> bool›
    apply (simp add: enum_bit_def enum_all_bit_def enum_ex_bit_def)
    by (metis bit.exhaust)
  show ‹enum_class.enum_ex P = Bex UNIV P› for P :: ‹bit ==> bool›
    apply (simp add: enum_bit_def enum_all_bit_def enum_ex_bit_def)
    by (metis bit.exhaust)
qed
end

lemma card_bit[simp]: "CARD(bit) = 2"
  using card_2_iff' by force

instantiation bit :: card_UNIV begin
definition "finite_UNIV = Phantom(bit) True"
definition "card_UNIV = Phantom(bit) 2"
instance
  apply intro_classes
  by (simp_all add: finite_UNIV_bit_def card_UNIV_bit_def)
end

lemma mat_of_rows_list_carrier[simp]:
  "mat_of_rows_list n vs ∈ carrier_mat (length vs) n"
  "dim_row (mat_of_rows_list n vs) = length vs"
  "dim_col (mat_of_rows_list n vs) = n"
  unfolding mat_of_rows_list_def by auto

lemma mat_of_rows_list_carrier2xn[iff]:
  "mat_of_rows_list n [a,b] ∈ carrier_mat 2 n"
  by auto

lemma mat_of_rows_list_carrier4xn[iff]:
  "mat_of_rows_list n [a,b,c,d] ∈ carrier_mat 4 n"
  by auto


(* text \<open>Overriding \<^theory>\<open>Complex_Bounded_Operators.Complex_Bounded_Linear_Function\<close>.\<^term>\<open>sandwich\<close>.
      The latter is the same function but defined as a \<^typ>\<open>(_,_) cblinfun\<close> which is less convenient for us.\<close>
definition sandwich where \<open>sandwich a b = a o\<^sub>C\<^sub>L b o\<^sub>C\<^sub>L a*\<close> *)

(* lemma clinear_sandwich[simp]: \<open>clinear (sandwich a)\<close>
  apply (rule clinearI)
   apply (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right sandwich_def)
  by (simp add: sandwich_apply)

lemma bounded_clinear_sandwich[simp]: \<open>bounded_clinear (sandwich a)\<close>
  apply (rule bounded_clinearI[where K=\<open>norm a * norm a\<close>])
   apply (auto simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right sandwich_def)
  by (smt (verit, ccfv_SIG) mult.commute mult_right_mono norm_adj norm_cblinfun_compose norm_ge_zero ordered_field_class.sign_simps(32)) *)

(* lemma sandwich_id[simp]: \<open>sandwich id_cblinfun = id_cblinfun\<close>
  by (auto simp: sandwich_apply) *)

(* lemma mat_of_cblinfun_sandwich:
  fixes a :: "(_::onb_enum, _::onb_enum) cblinfun"
  shows \<open>mat_of_cblinfun (sandwich a b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')\<close>
  by (simp add: mat_of_cblinfun_compose sandwich_def Let_def mat_of_cblinfun_adj)
 *)

lemma prod_cases3' [cases type]:
  obtains (fields) a b c where "y = ((a, b), c)"
  by (cases y, case_tac a) blast

text ‹We define the following abbreviations:
 ▪ ‹mutually f (x₁,x₂,…,x_n)› expands to the conjuction of all term‹f x_i x_j› with term‹i≠j›.
 ▪ ‹each f (x₁,x₂,…,x_n)› expands to the conjuction of all term‹f x_i›.›

syntax "_mutually" :: "'a ==> args ==> 'b" ("mutually _ '(_')")
syntax "_mutually2" :: "'a ==> 'b ==> args ==> args ==> 'c"

translations "mutually f (x)" => "CONST True"
translations "mutually f (_args x y)" => "f x y ∧ f y x"
translations "mutually f (_args x (_args x' xs))" => "_mutually2 f x (_args x' xs) (_args x' xs)"
translations "_mutually2 f x y zs" => "f x y ∧ f y x ∧ _mutually f zs"
translations "_mutually2 f x (_args y ys) zs" => "f x y ∧ f y x ∧ _mutually2 f x ys zs"

syntax "_each" :: "'a ==> args ==> 'b" ("each _ '(_')")
translations "each f (x)" => "f x"
translations "_each f (_args x xs)" => "f x ∧ _each f xs"



lemma dim_col_mat_adjoint[simp]: "dim_col (mat_adjoint m) = dim_row m"
  unfolding mat_adjoint_def by simp
lemma dim_row_mat_adjoint[simp]: "dim_row (mat_adjoint m) = dim_col m"
  unfolding mat_adjoint_def by simp

lemma invI: 
  assumes ‹inj f›
  assumes ‹x = f y›
  shows ‹inv f x = y›
  by (simp add: assms(1) assms(2))

instantiation prod :: (default,default) default begin
definition ‹default_prod = (default, default)›
instance..
end

instance bit :: default..

lemma surj_from_comp:
  assumes ‹surj (g o f)›
  assumes ‹inj g›
  shows ‹surj f›
  by (metis assms(1) assms(2) f_inv_into_f fun.set_map inj_image_mem_iff iso_tuple_UNIV_I surj_iff_all)

lemma double_exists: ‹(∃x y. Q x y) ⟷ (∃z. Q (fst z) (snd z))›
  by simp

lemma Ex_iffI:
  assumes ‹∧x. P x ==> Q (f x)›
  assumes ‹∧x. Q x ==> P (g x)›
  shows ‹Ex P ⟷ Ex Q›
  using assms(1) assms(2) by auto

(* TODO move to Bounded_Operators *)
lemma cspan_space_as_set[simp]: ‹cspan (space_as_set X) = space_as_set X›
  by auto

(* TODO integrate into lift_cblinfun_comp *)
(* TODO In doc of lift_cblinfun_comp, mention that it works specifically after cblinfun_assoc_left *)
thm lift_cblinfun_comp
lemma lift_cblinfun_comp2: 
  assumes ‹a o_CL b = c›
  shows ‹(d o_CL a) o_CL b = d o_CL c›
  by (simp add: assms cblinfun_assoc_right)
lemmas lift_cblinfun_comp = lift_cblinfun_comp lift_cblinfun_comp2

unbundle no cblinfun_syntax
unbundle no jnf_syntax

end