src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 67732 39d80006fc29
parent 67731 184c293f0a33
child 67968 a5ad4c015d1c
equal deleted inserted replaced
67731:184c293f0a33 67732:39d80006fc29
    37 text \<open>
    37 text \<open>
    38   Concrete syntax for \<open>('a, 'b) vec\<close>:
    38   Concrete syntax for \<open>('a, 'b) vec\<close>:
    39     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
    39     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
    40     \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
    40     \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
    41 \<close>
    41 \<close>
    42 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
    42 syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15)
    43 parse_translation \<open>
    43 parse_translation \<open>
    44   let
    44   let
    45     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
    45     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
    46     fun finite_vec_tr [t, u] =
    46     fun finite_vec_tr [t, u] =
    47       (case Term_Position.strip_positions u of
    47       (case Term_Position.strip_positions u of
    50             vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
    50             vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
    51               Syntax.const @{class_syntax finite})
    51               Syntax.const @{class_syntax finite})
    52           else vec t u
    52           else vec t u
    53       | _ => vec t u)
    53       | _ => vec t u)
    54   in
    54   in
    55     [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
    55     [(@{syntax_const "_vec_type"}, K finite_vec_tr)]
    56   end
    56   end
    57 \<close>
    57 \<close>
    58 
    58 
    59 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    59 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    60   by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
    60   by (simp add: vec_nth_inject [symmetric] fun_eq_iff)