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
begin

― ‹Remove notation that collides with the notation we use›
no_notation Order.top ("⊤ı")
no_notation m_inv ("invı _" [81] 80)
unbundle no_vec_syntax
unbundle no_inner_syntax

― ‹Import notation from Bounded Operator and Jordan Normal Form libraries›
unbundle cblinfun_notation
unbundle jnf_notation


abbreviation "butterket i j ≡ butterfly (ket i) (ket j)"
abbreviation "selfbutterket 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
  apply intro_classes
     apply (auto simp: enum_bit_def enum_all_bit_def enum_ex_bit_def)
   apply (metis bit_not_one_iff)
  by (metis bit_not_zero_iff)
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 apply_id_cblinfun[simp]: ‹(*⇩_V) id_cblinfun = id›
  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_def)

lemma sandwich_id[simp]: ‹sandwich id_cblinfun = id›
  by (auto simp: sandwich_def)

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

lemma lift_cblinfun_comp:
  assumes ‹a o⇩_C⇩_L b = c›
  shows ‹a o⇩_C⇩_L b = c›
    and ‹a o⇩_C⇩_L (b o⇩_C⇩_L d) = c o⇩_C⇩_L d›
    and ‹a *⇩_S (b *⇩_S S) = c *⇩_S S›
    and ‹a *⇩_V (b *⇩_V x) = c *⇩_V x›
     apply (fact assms)
    apply (simp add: assms cblinfun_assoc_left(1))
  using assms cblinfun_assoc_left(2) apply force
  using assms by force

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 enum_inj:
  assumes "i < CARD('a)" and "j < CARD('a)"
  shows "(Enum.enum ! i :: 'a::enum) = Enum.enum ! j ⟷ i = j"
  using inj_on_nth[OF enum_distinct, where I=‹{..<CARD('a)}›]
  using assms by (auto dest: inj_onD simp flip: card_UNIV_length_enum)


lemma [simp]: "dim_col (mat_adjoint m) = dim_row m"
  unfolding mat_adjoint_def by simp
lemma [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

end