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

― ‹Remove notation that collides with the notation we use
no_notation ("ı")
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"
  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)

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"
  apply intro_classes
  by (simp_all add: finite_UNIV_bit_def card_UNIV_bit_def)

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 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