Theory Misc

section ‹Miscellaneous facts›

text ‹This theory proves various facts that are not directly related to this developments 
but 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) ≡ butterfly (ket i) (ket j)" *)
(* abbreviation "butterfly (ket i) (ket i) ≡ 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 \<^binding>‹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 ‹Overriding \<^theory>‹Complex_Bounded_Operators.Complex_Bounded_Linear_Function›.\<^term>‹sandwich›.
      The latter is the same function but defined as a \<^typ>‹(_,_) cblinfun› which is less convenient for us.›
definition sandwich where ‹sandwich a b = a o⇩_C⇩_L b o⇩_C⇩_L a*› *)

(* lemma clinear_sandwich[simp]: ‹clinear (sandwich a)›
  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]: ‹bounded_clinear (sandwich a)›
  apply (rule bounded_clinearI[where K=‹norm a * norm a›])
   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]: ‹sandwich id_cblinfun = id_cblinfun›
  by (auto simp: sandwich_apply) *)

(* lemma mat_of_cblinfun_sandwich:
  fixes a :: "(_::onb_enum, _::onb_enum) cblinfun"
  shows ‹mat_of_cblinfun (sandwich a b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')›
  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⇩_C⇩_L b = c›
  shows ‹(d o⇩_C⇩_L a) o⇩_C⇩_L b = d o⇩_C⇩_L 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