removal of NatArith.ML and Product_Type.ML
authorpaulson
Mon Dec 13 15:06:59 2004 +0100 (2004-12-13)
changeset 15404a9a762f586b5
parent 15403 9e58e666074d
child 15405 010ea63b7a67
removal of NatArith.ML and Product_Type.ML
src/HOL/IsaMakefile
src/HOL/NatArith.ML
src/HOL/NatArith.thy
src/HOL/Product_Type.ML
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Dec 13 14:31:02 2004 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Dec 13 15:06:59 2004 +0100
     1.3 @@ -90,9 +90,8 @@
     1.4    Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
     1.5    Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
     1.6    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
     1.7 -  Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
     1.8 -  Nat.thy NatArith.ML NatArith.thy \
     1.9 -  Power.thy PreList.thy Product_Type.ML Product_Type.thy \
    1.10 +  Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy\
    1.11 +  Nat.ML Nat.thy NatArith.thy Power.thy PreList.thy Product_Type.thy \
    1.12    Refute.thy ROOT.ML \
    1.13    Recdef.thy Reconstruction.thy\
    1.14    Record.thy Relation.ML Relation.thy Relation_Power.ML \
     2.1 --- a/src/HOL/NatArith.ML	Mon Dec 13 14:31:02 2004 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,139 +0,0 @@
     2.4 -(*  Title:      HOL/NatArith.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1998  University of Cambridge
     2.8 -
     2.9 -Further proofs about elementary arithmetic, using the arithmetic proof
    2.10 -procedures.
    2.11 -*)
    2.12 -
    2.13 -(*legacy ...*)
    2.14 -structure NatArith = struct val thy = the_context () end;
    2.15 -
    2.16 -
    2.17 -Goal "m <= m*(m::nat)";
    2.18 -by (induct_tac "m" 1);
    2.19 -by Auto_tac;
    2.20 -qed "le_square";
    2.21 -
    2.22 -Goal "(m::nat) <= m*(m*m)";
    2.23 -by (induct_tac "m" 1);
    2.24 -by Auto_tac;
    2.25 -qed "le_cube";
    2.26 -
    2.27 -
    2.28 -(*** Subtraction laws -- mostly from Clemens Ballarin ***)
    2.29 -
    2.30 -Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
    2.31 -by (arith_tac 1);
    2.32 -qed "diff_less_mono";
    2.33 -
    2.34 -Goal "(i < j-k) = (i+k < (j::nat))";
    2.35 -by (arith_tac 1);
    2.36 -qed "less_diff_conv";
    2.37 -
    2.38 -Goal "(j-k <= (i::nat)) = (j <= i+k)";
    2.39 -by (arith_tac 1);
    2.40 -qed "le_diff_conv";
    2.41 -
    2.42 -Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
    2.43 -by (arith_tac 1);
    2.44 -qed "le_diff_conv2";
    2.45 -
    2.46 -Goal "i <= (n::nat) ==> n - (n - i) = i";
    2.47 -by (arith_tac 1);
    2.48 -qed "diff_diff_cancel";
    2.49 -Addsimps [diff_diff_cancel];
    2.50 -
    2.51 -Goal "k <= (n::nat) ==> m <= n + m - k";
    2.52 -by (arith_tac 1);
    2.53 -qed "le_add_diff";
    2.54 -
    2.55 -(*Replaces the previous diff_less and le_diff_less, which had the stronger
    2.56 -  second premise n<=m*)
    2.57 -Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
    2.58 -by (arith_tac 1);
    2.59 -qed "diff_less";
    2.60 -
    2.61 -
    2.62 -(** Simplification of relational expressions involving subtraction **)
    2.63 -
    2.64 -Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
    2.65 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    2.66 -qed "diff_diff_eq";
    2.67 -
    2.68 -Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
    2.69 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
    2.70 -qed "eq_diff_iff";
    2.71 -
    2.72 -Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
    2.73 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
    2.74 -qed "less_diff_iff";
    2.75 -
    2.76 -Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
    2.77 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
    2.78 -qed "le_diff_iff";
    2.79 -
    2.80 -
    2.81 -(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
    2.82 -
    2.83 -(* Monotonicity of subtraction in first argument *)
    2.84 -Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
    2.85 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    2.86 -qed "diff_le_mono";
    2.87 -
    2.88 -Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
    2.89 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    2.90 -qed "diff_le_mono2";
    2.91 -
    2.92 -Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
    2.93 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    2.94 -qed "diff_less_mono2";
    2.95 -
    2.96 -Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
    2.97 -by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    2.98 -qed "diffs0_imp_equal";
    2.99 -
   2.100 -(** Lemmas for ex/Factorization **)
   2.101 -
   2.102 -Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n";
   2.103 -by (case_tac "m" 1);
   2.104 -by Auto_tac;
   2.105 -qed "one_less_mult"; 
   2.106 -
   2.107 -Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<m*n";
   2.108 -by (case_tac "m" 1);
   2.109 -by Auto_tac;
   2.110 -qed "n_less_m_mult_n"; 
   2.111 -
   2.112 -Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<n*m";
   2.113 -by (case_tac "m" 1);
   2.114 -by Auto_tac;
   2.115 -qed "n_less_n_mult_m"; 
   2.116 -
   2.117 -
   2.118 -(** Rewriting to pull differences out **)
   2.119 -
   2.120 -Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
   2.121 -by (arith_tac 1);
   2.122 -qed "diff_diff_right";
   2.123 -
   2.124 -Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
   2.125 -by (arith_tac 1);
   2.126 -qed "diff_Suc_diff_eq1"; 
   2.127 -
   2.128 -Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
   2.129 -by (arith_tac 1);
   2.130 -qed "diff_Suc_diff_eq2"; 
   2.131 -
   2.132 -(*The others are
   2.133 -      i - j - k = i - (j + k),
   2.134 -      k <= j ==> j - k + i = j + i - k,
   2.135 -      k <= j ==> i + (j - k) = i + j - k *)
   2.136 -Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
   2.137 -	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
   2.138 -
   2.139 -
   2.140 -
   2.141 -(*No analogue of not_less_Least or Least_Suc yet, since it isn't used much*)
   2.142 -
     3.1 --- a/src/HOL/NatArith.thy	Mon Dec 13 14:31:02 2004 +0100
     3.2 +++ b/src/HOL/NatArith.thy	Mon Dec 13 15:06:59 2004 +0100
     3.3 @@ -3,7 +3,7 @@
     3.4      Author:     Tobias Nipkow and Markus Wenzel
     3.5  *)
     3.6  
     3.7 -header {* More arithmetic on natural numbers *}
     3.8 +header {*Further Arithmetic Facts Concerning the Natural Numbers*}
     3.9  
    3.10  theory NatArith
    3.11  imports Nat
    3.12 @@ -12,8 +12,9 @@
    3.13  
    3.14  setup arith_setup
    3.15  
    3.16 +text{*The following proofs may rely on the arithmetic proof procedures.*}
    3.17  
    3.18 -lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
    3.19 +lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
    3.20  by (simp add: less_eq reflcl_trancl [symmetric]
    3.21              del: reflcl_trancl, arith)
    3.22  
    3.23 @@ -21,21 +22,145 @@
    3.24      "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
    3.25      -- {* elimination of @{text -} on @{text nat} *}
    3.26    by (cases "a<b" rule: case_split)
    3.27 -    (auto simp add: diff_is_0_eq [THEN iffD2])
    3.28 +     (auto simp add: diff_is_0_eq [THEN iffD2])
    3.29  
    3.30  lemma nat_diff_split_asm:
    3.31      "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
    3.32      -- {* elimination of @{text -} on @{text nat} in assumptions *}
    3.33    by (simp split: nat_diff_split)
    3.34  
    3.35 -ML {*
    3.36 - val nat_diff_split = thm "nat_diff_split";
    3.37 - val nat_diff_split_asm = thm "nat_diff_split_asm";
    3.38 -*}
    3.39 -(* Careful: arith_tac produces counter examples!
    3.40 -fun add_arith cs = cs addafter ("arith_tac", arith_tac);
    3.41 -TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
    3.42 -
    3.43  lemmas [arith_split] = nat_diff_split split_min split_max
    3.44  
    3.45 +
    3.46 +
    3.47 +lemma le_square: "m \<le> m*(m::nat)"
    3.48 +by (induct_tac "m", auto)
    3.49 +
    3.50 +lemma le_cube: "(m::nat) \<le> m*(m*m)"
    3.51 +by (induct_tac "m", auto)
    3.52 +
    3.53 +
    3.54 +text{*Subtraction laws, mostly by Clemens Ballarin*}
    3.55 +
    3.56 +lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
    3.57 +by arith
    3.58 +
    3.59 +lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
    3.60 +by arith
    3.61 +
    3.62 +lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
    3.63 +by arith
    3.64 +
    3.65 +lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
    3.66 +by arith
    3.67 +
    3.68 +lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
    3.69 +by arith
    3.70 +
    3.71 +lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
    3.72 +by arith
    3.73 +
    3.74 +(*Replaces the previous diff_less and le_diff_less, which had the stronger
    3.75 +  second premise n\<le>m*)
    3.76 +lemma diff_less: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
    3.77 +by arith
    3.78 +
    3.79 +
    3.80 +(** Simplification of relational expressions involving subtraction **)
    3.81 +
    3.82 +lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
    3.83 +by (simp split add: nat_diff_split)
    3.84 +
    3.85 +lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
    3.86 +by (auto split add: nat_diff_split)
    3.87 +
    3.88 +lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
    3.89 +by (auto split add: nat_diff_split)
    3.90 +
    3.91 +lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
    3.92 +by (auto split add: nat_diff_split)
    3.93 +
    3.94 +
    3.95 +text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
    3.96 +
    3.97 +(* Monotonicity of subtraction in first argument *)
    3.98 +lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
    3.99 +by (simp split add: nat_diff_split)
   3.100 +
   3.101 +lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
   3.102 +by (simp split add: nat_diff_split)
   3.103 +
   3.104 +lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
   3.105 +by (simp split add: nat_diff_split)
   3.106 +
   3.107 +lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
   3.108 +by (simp split add: nat_diff_split)
   3.109 +
   3.110 +text{*Lemmas for ex/Factorization*}
   3.111 +
   3.112 +lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
   3.113 +by (case_tac "m", auto)
   3.114 +
   3.115 +lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
   3.116 +by (case_tac "m", auto)
   3.117 +
   3.118 +lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
   3.119 +by (case_tac "m", auto)
   3.120 +
   3.121 +
   3.122 +text{*Rewriting to pull differences out*}
   3.123 +
   3.124 +lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
   3.125 +by arith
   3.126 +
   3.127 +lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
   3.128 +by arith
   3.129 +
   3.130 +lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
   3.131 +by arith
   3.132 +
   3.133 +(*The others are
   3.134 +      i - j - k = i - (j + k),
   3.135 +      k \<le> j ==> j - k + i = j + i - k,
   3.136 +      k \<le> j ==> i + (j - k) = i + j - k *)
   3.137 +declare diff_diff_left [simp] 
   3.138 +        diff_add_assoc [symmetric, simp]
   3.139 +        diff_add_assoc2[symmetric, simp]
   3.140 +
   3.141 +text{*At present we prove no analogue of @{text not_less_Least} or @{text
   3.142 +Least_Suc}, since there appears to be no need.*}
   3.143 +
   3.144 +ML
   3.145 +{*
   3.146 +val nat_diff_split = thm "nat_diff_split";
   3.147 +val nat_diff_split_asm = thm "nat_diff_split_asm";
   3.148 +val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
   3.149 +val nat_diff_split = thm "nat_diff_split";
   3.150 +val nat_diff_split_asm = thm "nat_diff_split_asm";
   3.151 +val le_square = thm "le_square";
   3.152 +val le_cube = thm "le_cube";
   3.153 +val diff_less_mono = thm "diff_less_mono";
   3.154 +val less_diff_conv = thm "less_diff_conv";
   3.155 +val le_diff_conv = thm "le_diff_conv";
   3.156 +val le_diff_conv2 = thm "le_diff_conv2";
   3.157 +val diff_diff_cancel = thm "diff_diff_cancel";
   3.158 +val le_add_diff = thm "le_add_diff";
   3.159 +val diff_less = thm "diff_less";
   3.160 +val diff_diff_eq = thm "diff_diff_eq";
   3.161 +val eq_diff_iff = thm "eq_diff_iff";
   3.162 +val less_diff_iff = thm "less_diff_iff";
   3.163 +val le_diff_iff = thm "le_diff_iff";
   3.164 +val diff_le_mono = thm "diff_le_mono";
   3.165 +val diff_le_mono2 = thm "diff_le_mono2";
   3.166 +val diff_less_mono2 = thm "diff_less_mono2";
   3.167 +val diffs0_imp_equal = thm "diffs0_imp_equal";
   3.168 +val one_less_mult = thm "one_less_mult";
   3.169 +val n_less_m_mult_n = thm "n_less_m_mult_n";
   3.170 +val n_less_n_mult_m = thm "n_less_n_mult_m";
   3.171 +val diff_diff_right = thm "diff_diff_right";
   3.172 +val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
   3.173 +val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
   3.174 +*}
   3.175 +
   3.176 +
   3.177  end
     4.1 --- a/src/HOL/Product_Type.ML	Mon Dec 13 14:31:02 2004 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,97 +0,0 @@
     4.4 -
     4.5 -(* legacy ML bindings *)
     4.6 -
     4.7 -val Collect_split = thm "Collect_split";
     4.8 -val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
     4.9 -val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
    4.10 -val PairE = thm "PairE";
    4.11 -val PairE_lemma = thm "PairE_lemma";
    4.12 -val Pair_Rep_inject = thm "Pair_Rep_inject";
    4.13 -val Pair_def = thm "Pair_def";
    4.14 -val Pair_eq = thm "Pair_eq";
    4.15 -val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    4.16 -val Pair_inject = thm "Pair_inject";
    4.17 -val ProdI = thm "ProdI";
    4.18 -val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    4.19 -val SigmaD1 = thm "SigmaD1";
    4.20 -val SigmaD2 = thm "SigmaD2";
    4.21 -val SigmaE = thm "SigmaE";
    4.22 -val SigmaE2 = thm "SigmaE2";
    4.23 -val SigmaI = thm "SigmaI";
    4.24 -val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
    4.25 -val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
    4.26 -val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
    4.27 -val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
    4.28 -val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
    4.29 -val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
    4.30 -val Sigma_Union = thm "Sigma_Union";
    4.31 -val Sigma_def = thm "Sigma_def";
    4.32 -val Sigma_empty1 = thm "Sigma_empty1";
    4.33 -val Sigma_empty2 = thm "Sigma_empty2";
    4.34 -val Sigma_mono = thm "Sigma_mono";
    4.35 -val The_split = thm "The_split";
    4.36 -val The_split_eq = thm "The_split_eq";
    4.37 -val The_split_eq = thm "The_split_eq";
    4.38 -val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
    4.39 -val Times_Int_distrib1 = thm "Times_Int_distrib1";
    4.40 -val Times_Un_distrib1 = thm "Times_Un_distrib1";
    4.41 -val Times_eq_cancel2 = thm "Times_eq_cancel2";
    4.42 -val Times_subset_cancel2 = thm "Times_subset_cancel2";
    4.43 -val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
    4.44 -val UN_Times_distrib = thm "UN_Times_distrib";
    4.45 -val Unity_def = thm "Unity_def";
    4.46 -val cond_split_eta = thm "cond_split_eta";
    4.47 -val fst_conv = thm "fst_conv";
    4.48 -val fst_def = thm "fst_def";
    4.49 -val fst_eqD = thm "fst_eqD";
    4.50 -val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
    4.51 -val injective_fst_snd = thm "injective_fst_snd";
    4.52 -val mem_Sigma_iff = thm "mem_Sigma_iff";
    4.53 -val mem_splitE = thm "mem_splitE";
    4.54 -val mem_splitI = thm "mem_splitI";
    4.55 -val mem_splitI2 = thm "mem_splitI2";
    4.56 -val prod_eqI = thm "prod_eqI";
    4.57 -val prod_fun = thm "prod_fun";
    4.58 -val prod_fun_compose = thm "prod_fun_compose";
    4.59 -val prod_fun_def = thm "prod_fun_def";
    4.60 -val prod_fun_ident = thm "prod_fun_ident";
    4.61 -val prod_fun_imageE = thm "prod_fun_imageE";
    4.62 -val prod_fun_imageI = thm "prod_fun_imageI";
    4.63 -val prod_induct = thm "prod_induct";
    4.64 -val snd_conv = thm "snd_conv";
    4.65 -val snd_def = thm "snd_def";
    4.66 -val snd_eqD = thm "snd_eqD";
    4.67 -val split = thm "split";
    4.68 -val splitD = thm "splitD";
    4.69 -val splitD' = thm "splitD'";
    4.70 -val splitE = thm "splitE";
    4.71 -val splitE' = thm "splitE'";
    4.72 -val splitE2 = thm "splitE2";
    4.73 -val splitI = thm "splitI";
    4.74 -val splitI2 = thm "splitI2";
    4.75 -val splitI2' = thm "splitI2'";
    4.76 -val split_Pair_apply = thm "split_Pair_apply";
    4.77 -val split_beta = thm "split_beta";
    4.78 -val split_conv = thm "split_conv";
    4.79 -val split_def = thm "split_def";
    4.80 -val split_eta = thm "split_eta";
    4.81 -val split_eta_SetCompr = thm "split_eta_SetCompr";
    4.82 -val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
    4.83 -val split_paired_All = thm "split_paired_All";
    4.84 -val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
    4.85 -val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
    4.86 -val split_paired_Ex = thm "split_paired_Ex";
    4.87 -val split_paired_The = thm "split_paired_The";
    4.88 -val split_paired_all = thm "split_paired_all";
    4.89 -val split_part = thm "split_part";
    4.90 -val split_split = thm "split_split";
    4.91 -val split_split_asm = thm "split_split_asm";
    4.92 -val split_tupled_all = thms "split_tupled_all";
    4.93 -val split_weak_cong = thm "split_weak_cong";
    4.94 -val surj_pair = thm "surj_pair";
    4.95 -val surjective_pairing = thm "surjective_pairing";
    4.96 -val unit_abs_eta_conv = thm "unit_abs_eta_conv";
    4.97 -val unit_all_eq1 = thm "unit_all_eq1";
    4.98 -val unit_all_eq2 = thm "unit_all_eq2";
    4.99 -val unit_eq = thm "unit_eq";
   4.100 -val unit_induct = thm "unit_induct";
     5.1 --- a/src/HOL/Product_Type.thy	Mon Dec 13 14:31:02 2004 +0100
     5.2 +++ b/src/HOL/Product_Type.thy	Mon Dec 13 15:06:59 2004 +0100
     5.3 @@ -78,9 +78,9 @@
     5.4  qed
     5.5  
     5.6  syntax (xsymbols)
     5.7 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
     5.8 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
     5.9  syntax (HTML output)
    5.10 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    5.11 +  "*"      :: "[type, type] => type"         ("(_ \\<times>/ _)" [21, 20] 20)
    5.12  
    5.13  local
    5.14  
    5.15 @@ -157,12 +157,12 @@
    5.16  end
    5.17  *}
    5.18  
    5.19 -text{*Deleted x-symbol and html support using @{text"\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
    5.20 +text{*Deleted x-symbol and html support using @{text"\\<Sigma>"} (Sigma) because of the danger of confusion with Sum.*}
    5.21  syntax (xsymbols)
    5.22 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    5.23 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
    5.24  
    5.25  syntax (HTML output)
    5.26 -  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \<times> _" [81, 80] 80)
    5.27 +  "@Times" :: "['a set,  'a => 'b set] => ('a * 'b) set"  ("_ \\<times> _" [81, 80] 80)
    5.28  
    5.29  print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *}
    5.30  
    5.31 @@ -612,7 +612,7 @@
    5.32    by (unfold Sigma_def) blast
    5.33  
    5.34  text {*
    5.35 -  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
    5.36 +  Elimination of @{term "(a, b) : A \\<times> B"} -- introduces no
    5.37    eigenvariables.
    5.38  *}
    5.39  
    5.40 @@ -629,8 +629,8 @@
    5.41    by blast
    5.42  
    5.43  lemma Sigma_cong:
    5.44 -     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
    5.45 -      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
    5.46 +     "\\<lbrakk>A = B; !!x. x \\<in> B \\<Longrightarrow> C x = D x\\<rbrakk>
    5.47 +      \\<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
    5.48  by auto
    5.49  
    5.50  lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
    5.51 @@ -824,4 +824,102 @@
    5.52  
    5.53  setup prod_codegen_setup
    5.54  
    5.55 +ML
    5.56 +{*
    5.57 +val Collect_split = thm "Collect_split";
    5.58 +val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
    5.59 +val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
    5.60 +val PairE = thm "PairE";
    5.61 +val PairE_lemma = thm "PairE_lemma";
    5.62 +val Pair_Rep_inject = thm "Pair_Rep_inject";
    5.63 +val Pair_def = thm "Pair_def";
    5.64 +val Pair_eq = thm "Pair_eq";
    5.65 +val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    5.66 +val Pair_inject = thm "Pair_inject";
    5.67 +val ProdI = thm "ProdI";
    5.68 +val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    5.69 +val SigmaD1 = thm "SigmaD1";
    5.70 +val SigmaD2 = thm "SigmaD2";
    5.71 +val SigmaE = thm "SigmaE";
    5.72 +val SigmaE2 = thm "SigmaE2";
    5.73 +val SigmaI = thm "SigmaI";
    5.74 +val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
    5.75 +val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
    5.76 +val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
    5.77 +val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
    5.78 +val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
    5.79 +val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
    5.80 +val Sigma_Union = thm "Sigma_Union";
    5.81 +val Sigma_def = thm "Sigma_def";
    5.82 +val Sigma_empty1 = thm "Sigma_empty1";
    5.83 +val Sigma_empty2 = thm "Sigma_empty2";
    5.84 +val Sigma_mono = thm "Sigma_mono";
    5.85 +val The_split = thm "The_split";
    5.86 +val The_split_eq = thm "The_split_eq";
    5.87 +val The_split_eq = thm "The_split_eq";
    5.88 +val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
    5.89 +val Times_Int_distrib1 = thm "Times_Int_distrib1";
    5.90 +val Times_Un_distrib1 = thm "Times_Un_distrib1";
    5.91 +val Times_eq_cancel2 = thm "Times_eq_cancel2";
    5.92 +val Times_subset_cancel2 = thm "Times_subset_cancel2";
    5.93 +val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
    5.94 +val UN_Times_distrib = thm "UN_Times_distrib";
    5.95 +val Unity_def = thm "Unity_def";
    5.96 +val cond_split_eta = thm "cond_split_eta";
    5.97 +val fst_conv = thm "fst_conv";
    5.98 +val fst_def = thm "fst_def";
    5.99 +val fst_eqD = thm "fst_eqD";
   5.100 +val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
   5.101 +val injective_fst_snd = thm "injective_fst_snd";
   5.102 +val mem_Sigma_iff = thm "mem_Sigma_iff";
   5.103 +val mem_splitE = thm "mem_splitE";
   5.104 +val mem_splitI = thm "mem_splitI";
   5.105 +val mem_splitI2 = thm "mem_splitI2";
   5.106 +val prod_eqI = thm "prod_eqI";
   5.107 +val prod_fun = thm "prod_fun";
   5.108 +val prod_fun_compose = thm "prod_fun_compose";
   5.109 +val prod_fun_def = thm "prod_fun_def";
   5.110 +val prod_fun_ident = thm "prod_fun_ident";
   5.111 +val prod_fun_imageE = thm "prod_fun_imageE";
   5.112 +val prod_fun_imageI = thm "prod_fun_imageI";
   5.113 +val prod_induct = thm "prod_induct";
   5.114 +val snd_conv = thm "snd_conv";
   5.115 +val snd_def = thm "snd_def";
   5.116 +val snd_eqD = thm "snd_eqD";
   5.117 +val split = thm "split";
   5.118 +val splitD = thm "splitD";
   5.119 +val splitD' = thm "splitD'";
   5.120 +val splitE = thm "splitE";
   5.121 +val splitE' = thm "splitE'";
   5.122 +val splitE2 = thm "splitE2";
   5.123 +val splitI = thm "splitI";
   5.124 +val splitI2 = thm "splitI2";
   5.125 +val splitI2' = thm "splitI2'";
   5.126 +val split_Pair_apply = thm "split_Pair_apply";
   5.127 +val split_beta = thm "split_beta";
   5.128 +val split_conv = thm "split_conv";
   5.129 +val split_def = thm "split_def";
   5.130 +val split_eta = thm "split_eta";
   5.131 +val split_eta_SetCompr = thm "split_eta_SetCompr";
   5.132 +val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
   5.133 +val split_paired_All = thm "split_paired_All";
   5.134 +val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
   5.135 +val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
   5.136 +val split_paired_Ex = thm "split_paired_Ex";
   5.137 +val split_paired_The = thm "split_paired_The";
   5.138 +val split_paired_all = thm "split_paired_all";
   5.139 +val split_part = thm "split_part";
   5.140 +val split_split = thm "split_split";
   5.141 +val split_split_asm = thm "split_split_asm";
   5.142 +val split_tupled_all = thms "split_tupled_all";
   5.143 +val split_weak_cong = thm "split_weak_cong";
   5.144 +val surj_pair = thm "surj_pair";
   5.145 +val surjective_pairing = thm "surjective_pairing";
   5.146 +val unit_abs_eta_conv = thm "unit_abs_eta_conv";
   5.147 +val unit_all_eq1 = thm "unit_all_eq1";
   5.148 +val unit_all_eq2 = thm "unit_all_eq2";
   5.149 +val unit_eq = thm "unit_eq";
   5.150 +val unit_induct = thm "unit_induct";
   5.151 +*}
   5.152 +
   5.153  end