src/HOL/Library/Cardinality.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60583 a645a0e6d790
     1.1 --- a/src/HOL/Library/Cardinality.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Brian Huffman, Andreas Lochbihler
     1.5  *)
     1.6  
     1.7 -section {* Cardinality of types *}
     1.8 +section \<open>Cardinality of types\<close>
     1.9  
    1.10  theory Cardinality
    1.11  imports Phantom_Type
    1.12  begin
    1.13  
    1.14 -subsection {* Preliminary lemmas *}
    1.15 +subsection \<open>Preliminary lemmas\<close>
    1.16  (* These should be moved elsewhere *)
    1.17  
    1.18  lemma (in type_definition) univ:
    1.19 @@ -37,18 +37,18 @@
    1.20      by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD)
    1.21  qed
    1.22  
    1.23 -subsection {* Cardinalities of types *}
    1.24 +subsection \<open>Cardinalities of types\<close>
    1.25  
    1.26  syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
    1.27  
    1.28  translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
    1.29  
    1.30 -print_translation {*
    1.31 +print_translation \<open>
    1.32    let
    1.33      fun card_univ_tr' ctxt [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    1.34        Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
    1.35    in [(@{const_syntax card}, card_univ_tr')] end
    1.36 -*}
    1.37 +\<close>
    1.38  
    1.39  lemma card_prod [simp]: "CARD('a \<times> 'b) = CARD('a) * CARD('b)"
    1.40    unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product)
    1.41 @@ -161,9 +161,9 @@
    1.42  lemma card_literal: "CARD(String.literal) = 0"
    1.43  by(simp add: card_eq_0_iff infinite_literal)
    1.44  
    1.45 -subsection {* Classes with at least 1 and 2  *}
    1.46 +subsection \<open>Classes with at least 1 and 2\<close>
    1.47  
    1.48 -text {* Class finite already captures "at least 1" *}
    1.49 +text \<open>Class finite already captures "at least 1"\<close>
    1.50  
    1.51  lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)"
    1.52    unfolding neq0_conv [symmetric] by simp
    1.53 @@ -171,7 +171,7 @@
    1.54  lemma one_le_card_finite [simp]: "Suc 0 \<le> CARD('a::finite)"
    1.55    by (simp add: less_Suc_eq_le [symmetric])
    1.56  
    1.57 -text {* Class for cardinality "at least 2" *}
    1.58 +text \<open>Class for cardinality "at least 2"\<close>
    1.59  
    1.60  class card2 = finite + 
    1.61    assumes two_le_card: "2 \<le> CARD('a)"
    1.62 @@ -183,7 +183,7 @@
    1.63    using one_less_card [where 'a='a] by simp
    1.64  
    1.65  
    1.66 -subsection {* A type class for deciding finiteness of types *}
    1.67 +subsection \<open>A type class for deciding finiteness of types\<close>
    1.68  
    1.69  type_synonym 'a finite_UNIV = "('a, bool) phantom"
    1.70  
    1.71 @@ -196,7 +196,7 @@
    1.72    \<longleftrightarrow> of_phantom (finite_UNIV :: 'a finite_UNIV)"
    1.73  by(simp add: finite_UNIV)
    1.74  
    1.75 -subsection {* A type class for computing the cardinality of types *}
    1.76 +subsection \<open>A type class for computing the cardinality of types\<close>
    1.77  
    1.78  definition is_list_UNIV :: "'a list \<Rightarrow> bool"
    1.79  where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
    1.80 @@ -211,7 +211,7 @@
    1.81    fixes card_UNIV :: "'a card_UNIV"
    1.82    assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)"
    1.83  
    1.84 -subsection {* Instantiations for @{text "card_UNIV"} *}
    1.85 +subsection \<open>Instantiations for @{text "card_UNIV"}\<close>
    1.86  
    1.87  instantiation nat :: card_UNIV begin
    1.88  definition "finite_UNIV = Phantom(nat) False"
    1.89 @@ -396,9 +396,9 @@
    1.90    by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def)
    1.91  end
    1.92  
    1.93 -subsection {* Code setup for sets *}
    1.94 +subsection \<open>Code setup for sets\<close>
    1.95  
    1.96 -text {*
    1.97 +text \<open>
    1.98    Implement @{term "CARD('a)"} via @{term card_UNIV} and provide
    1.99    implementations for @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, 
   1.100    and @{term "op ="}if the calling context already provides @{class finite_UNIV}
   1.101 @@ -406,7 +406,7 @@
   1.102    always via @{term card_UNIV}, we would require instances of essentially all 
   1.103    element types, i.e., a lot of instantiation proofs and -- at run time --
   1.104    possibly slow dictionary constructions.
   1.105 -*}
   1.106 +\<close>
   1.107  
   1.108  definition card_UNIV' :: "'a card_UNIV"
   1.109  where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
   1.110 @@ -491,13 +491,13 @@
   1.111  
   1.112  end
   1.113  
   1.114 -text {* 
   1.115 +text \<open>
   1.116    Provide more informative exceptions than Match for non-rewritten cases.
   1.117    If generated code raises one these exceptions, then a code equation calls
   1.118    the mentioned operator for an element type that is not an instance of
   1.119    @{class card_UNIV} and is therefore not implemented via @{term card_UNIV}.
   1.120    Constrain the element type with sort @{class card_UNIV} to change this.
   1.121 -*}
   1.122 +\<close>
   1.123  
   1.124  lemma card_coset_error [code]:
   1.125    "card (List.coset xs) =