src/HOL/Product_Type.thy
changeset 15404 a9a762f586b5
parent 15394 a2c34e6ca4f8
child 15422 cbdddc0efadf
     1.1 --- a/src/HOL/Product_Type.thy	Mon Dec 13 14:31:02 2004 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Dec 13 15:06:59 2004 +0100
     1.3 @@ -78,9 +78,9 @@
     1.4  qed
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
     1.8 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
     1.9  syntax (HTML output)
    1.10 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    1.11 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
    1.12  
    1.13  local
    1.14  
    1.15 @@ -157,12 +157,12 @@
    1.16  end
    1.17  *}
    1.18  
    1.19 -text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
    1.20 +text{*Deleted x-symbol and html support using @{text"\\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
    1.21  syntax (xsymbols)
    1.22 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    1.23 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
    1.24  
    1.25  syntax (HTML output)
    1.26 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    1.27 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
    1.28  
    1.29  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    1.30  
    1.31 @@ -612,7 +612,7 @@
    1.32    by (unfold Sigma_def) blast
    1.33  
    1.34  text {*
    1.35 -  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
    1.36 +  Elimination of @{term "(a, b) : A \\<times> B"} -- introduces no
    1.37    eigenvariables.
    1.38  *}
    1.39  
    1.40 @@ -629,8 +629,8 @@
    1.41    by blast
    1.42  
    1.43  lemma Sigma_cong:
    1.44 -     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
    1.45 -      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
    1.46 +     "\\<lbrakk>A = B; !!x. x \\<in> B \\<Longrightarrow> C x = D x\\<rbrakk>
    1.47 +      \\<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
    1.48  by auto
    1.49  
    1.50  lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
    1.51 @@ -824,4 +824,102 @@
    1.52  
    1.53  setup prod_codegen_setup
    1.54  
    1.55 +ML
    1.56 +{*
    1.57 +val Collect_split = thm "Collect_split";
    1.58 +val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
    1.59 +val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
    1.60 +val PairE = thm "PairE";
    1.61 +val PairE_lemma = thm "PairE_lemma";
    1.62 +val Pair_Rep_inject = thm "Pair_Rep_inject";
    1.63 +val Pair_def = thm "Pair_def";
    1.64 +val Pair_eq = thm "Pair_eq";
    1.65 +val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    1.66 +val Pair_inject = thm "Pair_inject";
    1.67 +val ProdI = thm "ProdI";
    1.68 +val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    1.69 +val SigmaD1 = thm "SigmaD1";
    1.70 +val SigmaD2 = thm "SigmaD2";
    1.71 +val SigmaE = thm "SigmaE";
    1.72 +val SigmaE2 = thm "SigmaE2";
    1.73 +val SigmaI = thm "SigmaI";
    1.74 +val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
    1.75 +val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
    1.76 +val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
    1.77 +val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
    1.78 +val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
    1.79 +val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
    1.80 +val Sigma_Union = thm "Sigma_Union";
    1.81 +val Sigma_def = thm "Sigma_def";
    1.82 +val Sigma_empty1 = thm "Sigma_empty1";
    1.83 +val Sigma_empty2 = thm "Sigma_empty2";
    1.84 +val Sigma_mono = thm "Sigma_mono";
    1.85 +val The_split = thm "The_split";
    1.86 +val The_split_eq = thm "The_split_eq";
    1.87 +val The_split_eq = thm "The_split_eq";
    1.88 +val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
    1.89 +val Times_Int_distrib1 = thm "Times_Int_distrib1";
    1.90 +val Times_Un_distrib1 = thm "Times_Un_distrib1";
    1.91 +val Times_eq_cancel2 = thm "Times_eq_cancel2";
    1.92 +val Times_subset_cancel2 = thm "Times_subset_cancel2";
    1.93 +val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
    1.94 +val UN_Times_distrib = thm "UN_Times_distrib";
    1.95 +val Unity_def = thm "Unity_def";
    1.96 +val cond_split_eta = thm "cond_split_eta";
    1.97 +val fst_conv = thm "fst_conv";
    1.98 +val fst_def = thm "fst_def";
    1.99 +val fst_eqD = thm "fst_eqD";
   1.100 +val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
   1.101 +val injective_fst_snd = thm "injective_fst_snd";
   1.102 +val mem_Sigma_iff = thm "mem_Sigma_iff";
   1.103 +val mem_splitE = thm "mem_splitE";
   1.104 +val mem_splitI = thm "mem_splitI";
   1.105 +val mem_splitI2 = thm "mem_splitI2";
   1.106 +val prod_eqI = thm "prod_eqI";
   1.107 +val prod_fun = thm "prod_fun";
   1.108 +val prod_fun_compose = thm "prod_fun_compose";
   1.109 +val prod_fun_def = thm "prod_fun_def";
   1.110 +val prod_fun_ident = thm "prod_fun_ident";
   1.111 +val prod_fun_imageE = thm "prod_fun_imageE";
   1.112 +val prod_fun_imageI = thm "prod_fun_imageI";
   1.113 +val prod_induct = thm "prod_induct";
   1.114 +val snd_conv = thm "snd_conv";
   1.115 +val snd_def = thm "snd_def";
   1.116 +val snd_eqD = thm "snd_eqD";
   1.117 +val split = thm "split";
   1.118 +val splitD = thm "splitD";
   1.119 +val splitD' = thm "splitD'";
   1.120 +val splitE = thm "splitE";
   1.121 +val splitE' = thm "splitE'";
   1.122 +val splitE2 = thm "splitE2";
   1.123 +val splitI = thm "splitI";
   1.124 +val splitI2 = thm "splitI2";
   1.125 +val splitI2' = thm "splitI2'";
   1.126 +val split_Pair_apply = thm "split_Pair_apply";
   1.127 +val split_beta = thm "split_beta";
   1.128 +val split_conv = thm "split_conv";
   1.129 +val split_def = thm "split_def";
   1.130 +val split_eta = thm "split_eta";
   1.131 +val split_eta_SetCompr = thm "split_eta_SetCompr";
   1.132 +val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
   1.133 +val split_paired_All = thm "split_paired_All";
   1.134 +val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
   1.135 +val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
   1.136 +val split_paired_Ex = thm "split_paired_Ex";
   1.137 +val split_paired_The = thm "split_paired_The";
   1.138 +val split_paired_all = thm "split_paired_all";
   1.139 +val split_part = thm "split_part";
   1.140 +val split_split = thm "split_split";
   1.141 +val split_split_asm = thm "split_split_asm";
   1.142 +val split_tupled_all = thms "split_tupled_all";
   1.143 +val split_weak_cong = thm "split_weak_cong";
   1.144 +val surj_pair = thm "surj_pair";
   1.145 +val surjective_pairing = thm "surjective_pairing";
   1.146 +val unit_abs_eta_conv = thm "unit_abs_eta_conv";
   1.147 +val unit_all_eq1 = thm "unit_all_eq1";
   1.148 +val unit_all_eq2 = thm "unit_all_eq2";
   1.149 +val unit_eq = thm "unit_eq";
   1.150 +val unit_induct = thm "unit_induct";
   1.151 +*}
   1.152 +
   1.153  end