src/HOL/Analysis/Finite_Cartesian_Product.thy
changeset 67731 184c293f0a33
parent 67686 2c58505bf151
child 67732 39d80006fc29
equal deleted inserted replaced
67730:f91c437f6f68 67731:184c293f0a33
    13   "HOL-Library.FuncSet"
    13   "HOL-Library.FuncSet"
    14 begin
    14 begin
    15 
    15 
    16 subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
    16 subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
    17 
    17 
    18 typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
    18 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
    19   morphisms vec_nth vec_lambda ..
    19   morphisms vec_nth vec_lambda ..
    20 
    20 
    21 declare vec_lambda_inject [simplified, simp]
    21 declare vec_lambda_inject [simplified, simp]
    22 
    22 
    23 bundle vec_syntax begin
    23 bundle vec_syntax begin
    32   vec_lambda (binder "\<chi>" 10)
    32   vec_lambda (binder "\<chi>" 10)
    33 end
    33 end
    34 
    34 
    35 unbundle vec_syntax
    35 unbundle vec_syntax
    36 
    36 
    37 (*
    37 text \<open>
    38   Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
    38   Concrete syntax for \<open>('a, 'b) vec\<close>:
    39   the finite type class write "vec 'b 'n"
    39     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
    40 *)
    40     \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
    41 
    41 \<close>
    42 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
    42 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
    43 
       
    44 parse_translation \<open>
    43 parse_translation \<open>
    45   let
    44   let
    46     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
    45     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
    47     fun finite_vec_tr [t, u] =
    46     fun finite_vec_tr [t, u] =
    48       (case Term_Position.strip_positions u of
    47       (case Term_Position.strip_positions u of
   105     by (auto elim!: countableE)
   104     by (auto elim!: countableE)
   106 qed
   105 qed
   107 
   106 
   108 lemma infinite_UNIV_vec:
   107 lemma infinite_UNIV_vec:
   109   assumes "infinite (UNIV :: 'a set)"
   108   assumes "infinite (UNIV :: 'a set)"
   110   shows   "infinite (UNIV :: ('a, 'b :: finite) vec set)"
   109   shows   "infinite (UNIV :: ('a^'b) set)"
   111 proof (subst bij_betw_finite)
   110 proof (subst bij_betw_finite)
   112   show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
   111   show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
   113     by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
   112     by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
   114   have "infinite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" (is "infinite ?A")
   113   have "infinite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" (is "infinite ?A")
   115   proof
   114   proof
   125     by auto
   124     by auto
   126   finally show "infinite (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" .
   125   finally show "infinite (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" .
   127 qed
   126 qed
   128 
   127 
   129 lemma CARD_vec [simp]:
   128 lemma CARD_vec [simp]:
   130   "CARD(('a,'b::finite) vec) = CARD('a) ^ CARD('b)"
   129   "CARD('a^'b) = CARD('a) ^ CARD('b)"
   131 proof (cases "finite (UNIV :: 'a set)")
   130 proof (cases "finite (UNIV :: 'a set)")
   132   case True
   131   case True
   133   show ?thesis
   132   show ?thesis
   134   proof (subst bij_betw_same_card)
   133   proof (subst bij_betw_same_card)
   135     show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
   134     show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
   383 
   382 
   384 instantiation vec :: (metric_space, finite) uniformity_dist
   383 instantiation vec :: (metric_space, finite) uniformity_dist
   385 begin
   384 begin
   386 
   385 
   387 definition [code del]:
   386 definition [code del]:
   388   "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) =
   387   "(uniformity :: (('a^'b::_) \<times> ('a^'b::_)) filter) =
   389     (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   388     (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   390 
   389 
   391 instance
   390 instance
   392   by standard (rule uniformity_vec_def)
   391   by standard (rule uniformity_vec_def)
   393 end
   392 end