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 bindingfact
((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 \theoryComplex_Bounded_Operators.Complex_Bounded_Linear_Function.termsandwich.
      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 oCL b oCL 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 oCL b = c
  shows a oCL b = c
    and a oCL (b oCL d) = c oCL 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 (x1,x2,…,xn)› expands to the conjuction of all termf xi xj with termij.
 each f (x1,x2,…,xn)› expands to the conjuction of all termf xi.

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