got rid of ML proof scripts for Product_Type;
authorwenzelm
Fri Oct 19 22:01:25 2001 +0200 (2001-10-19)
changeset 1183802d75712061d
parent 11837 b2a9853ec6dd
child 11839 3ef83c265aca
got rid of ML proof scripts for Product_Type;
src/HOL/Product_Type.ML
src/HOL/Product_Type.thy
src/HOL/Tools/split_rule.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Product_Type.ML	Fri Oct 19 22:01:25 2001 +0200
     1.3 @@ -0,0 +1,97 @@
     1.4 +
     1.5 +(* legacy ML bindings *)
     1.6 +
     1.7 +val Collect_split = thm "Collect_split";
     1.8 +val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1";
     1.9 +val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";
    1.10 +val PairE = thm "PairE";
    1.11 +val PairE_lemma = thm "PairE_lemma";
    1.12 +val Pair_Rep_inject = thm "Pair_Rep_inject";
    1.13 +val Pair_def = thm "Pair_def";
    1.14 +val Pair_eq = thm "Pair_eq";
    1.15 +val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    1.16 +val Pair_inject = thm "Pair_inject";
    1.17 +val ProdI = thm "ProdI";
    1.18 +val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    1.19 +val SigmaD1 = thm "SigmaD1";
    1.20 +val SigmaD2 = thm "SigmaD2";
    1.21 +val SigmaE = thm "SigmaE";
    1.22 +val SigmaE2 = thm "SigmaE2";
    1.23 +val SigmaI = thm "SigmaI";
    1.24 +val Sigma_Diff_distrib1 = thm "Sigma_Diff_distrib1";
    1.25 +val Sigma_Diff_distrib2 = thm "Sigma_Diff_distrib2";
    1.26 +val Sigma_Int_distrib1 = thm "Sigma_Int_distrib1";
    1.27 +val Sigma_Int_distrib2 = thm "Sigma_Int_distrib2";
    1.28 +val Sigma_Un_distrib1 = thm "Sigma_Un_distrib1";
    1.29 +val Sigma_Un_distrib2 = thm "Sigma_Un_distrib2";
    1.30 +val Sigma_Union = thm "Sigma_Union";
    1.31 +val Sigma_def = thm "Sigma_def";
    1.32 +val Sigma_empty1 = thm "Sigma_empty1";
    1.33 +val Sigma_empty2 = thm "Sigma_empty2";
    1.34 +val Sigma_mono = thm "Sigma_mono";
    1.35 +val The_split = thm "The_split";
    1.36 +val The_split_eq = thm "The_split_eq";
    1.37 +val The_split_eq = thm "The_split_eq";
    1.38 +val Times_Diff_distrib1 = thm "Times_Diff_distrib1";
    1.39 +val Times_Int_distrib1 = thm "Times_Int_distrib1";
    1.40 +val Times_Un_distrib1 = thm "Times_Un_distrib1";
    1.41 +val Times_eq_cancel2 = thm "Times_eq_cancel2";
    1.42 +val Times_subset_cancel2 = thm "Times_subset_cancel2";
    1.43 +val UNIV_Times_UNIV = thm "UNIV_Times_UNIV";
    1.44 +val UN_Times_distrib = thm "UN_Times_distrib";
    1.45 +val Unity_def = thm "Unity_def";
    1.46 +val cond_split_eta = thm "cond_split_eta";
    1.47 +val fst_conv = thm "fst_conv";
    1.48 +val fst_def = thm "fst_def";
    1.49 +val fst_eqD = thm "fst_eqD";
    1.50 +val inj_on_Abs_Prod = thm "inj_on_Abs_Prod";
    1.51 +val injective_fst_snd = thm "injective_fst_snd";
    1.52 +val mem_Sigma_iff = thm "mem_Sigma_iff";
    1.53 +val mem_splitE = thm "mem_splitE";
    1.54 +val mem_splitI = thm "mem_splitI";
    1.55 +val mem_splitI2 = thm "mem_splitI2";
    1.56 +val prod_eqI = thm "prod_eqI";
    1.57 +val prod_fun = thm "prod_fun";
    1.58 +val prod_fun_compose = thm "prod_fun_compose";
    1.59 +val prod_fun_def = thm "prod_fun_def";
    1.60 +val prod_fun_ident = thm "prod_fun_ident";
    1.61 +val prod_fun_imageE = thm "prod_fun_imageE";
    1.62 +val prod_fun_imageI = thm "prod_fun_imageI";
    1.63 +val prod_induct = thm "prod_induct";
    1.64 +val snd_conv = thm "snd_conv";
    1.65 +val snd_def = thm "snd_def";
    1.66 +val snd_eqD = thm "snd_eqD";
    1.67 +val split = thm "split";
    1.68 +val splitD = thm "splitD";
    1.69 +val splitD' = thm "splitD'";
    1.70 +val splitE = thm "splitE";
    1.71 +val splitE' = thm "splitE'";
    1.72 +val splitE2 = thm "splitE2";
    1.73 +val splitI = thm "splitI";
    1.74 +val splitI2 = thm "splitI2";
    1.75 +val splitI2' = thm "splitI2'";
    1.76 +val split_Pair_apply = thm "split_Pair_apply";
    1.77 +val split_beta = thm "split_beta";
    1.78 +val split_conv = thm "split_conv";
    1.79 +val split_def = thm "split_def";
    1.80 +val split_eta = thm "split_eta";
    1.81 +val split_eta_SetCompr = thm "split_eta_SetCompr";
    1.82 +val split_eta_SetCompr2 = thm "split_eta_SetCompr2";
    1.83 +val split_paired_All = thm "split_paired_All";
    1.84 +val split_paired_Ball_Sigma = thm "split_paired_Ball_Sigma";
    1.85 +val split_paired_Bex_Sigma = thm "split_paired_Bex_Sigma";
    1.86 +val split_paired_Ex = thm "split_paired_Ex";
    1.87 +val split_paired_The = thm "split_paired_The";
    1.88 +val split_paired_all = thm "split_paired_all";
    1.89 +val split_part = thm "split_part";
    1.90 +val split_split = thm "split_split";
    1.91 +val split_split_asm = thm "split_split_asm";
    1.92 +val split_tupled_all = thms "split_tupled_all";
    1.93 +val split_weak_cong = thm "split_weak_cong";
    1.94 +val surj_pair = thm "surj_pair";
    1.95 +val surjective_pairing = thm "surjective_pairing";
    1.96 +val unit_abs_eta_conv = thm "unit_abs_eta_conv";
    1.97 +val unit_all_eq1 = thm "unit_all_eq1";
    1.98 +val unit_all_eq2 = thm "unit_all_eq2";
    1.99 +val unit_eq = thm "unit_eq";
   1.100 +val unit_induct = thm "unit_induct";
     2.1 --- a/src/HOL/Product_Type.thy	Fri Oct 19 22:00:08 2001 +0200
     2.2 +++ b/src/HOL/Product_Type.thy	Fri Oct 19 22:01:25 2001 +0200
     2.3 @@ -4,13 +4,62 @@
     2.4      Copyright   1992  University of Cambridge
     2.5  *)
     2.6  
     2.7 -header {* Finite products (including unit) *}
     2.8 +header {* Cartesian products *}
     2.9  
    2.10  theory Product_Type = Fun
    2.11 -files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"):
    2.12 +files ("Tools/split_rule.ML"):
    2.13 +
    2.14 +subsection {* Unit *}
    2.15 +
    2.16 +typedef unit = "{True}"
    2.17 +proof
    2.18 +  show "True : ?unit" by blast
    2.19 +qed
    2.20 +
    2.21 +constdefs
    2.22 +  Unity :: unit    ("'(')")
    2.23 +  "() == Abs_unit True"
    2.24 +
    2.25 +lemma unit_eq: "u = ()"
    2.26 +  by (induct u) (simp add: unit_def Unity_def)
    2.27 +
    2.28 +text {*
    2.29 +  Simplification procedure for @{thm [source] unit_eq}.  Cannot use
    2.30 +  this rule directly --- it loops!
    2.31 +*}
    2.32 +
    2.33 +ML_setup {*
    2.34 +  local
    2.35 +    val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
    2.36 +    val unit_meta_eq = standard (mk_meta_eq (thm "unit_eq"));
    2.37 +    fun proc _ _ t =
    2.38 +      if HOLogic.is_unit t then None
    2.39 +      else Some unit_meta_eq
    2.40 +  in val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc end;
    2.41 +
    2.42 +  Addsimprocs [unit_eq_proc];
    2.43 +*}
    2.44 +
    2.45 +lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
    2.46 +  by simp
    2.47 +
    2.48 +lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
    2.49 +  by (rule triv_forall_equality)
    2.50 +
    2.51 +lemma unit_induct [induct type: unit]: "P () ==> P x"
    2.52 +  by simp
    2.53 +
    2.54 +text {*
    2.55 +  This rewrite counters the effect of @{text unit_eq_proc} on @{term
    2.56 +  [source] "%u::unit. f u"}, replacing it by @{term [source]
    2.57 +  f} rather than by @{term [source] "%u. f ()"}.
    2.58 +*}
    2.59 +
    2.60 +lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
    2.61 +  by (rule ext) simp
    2.62  
    2.63  
    2.64 -subsection {* Products *}
    2.65 +subsection {* Pairs *}
    2.66  
    2.67  subsubsection {* Type definition *}
    2.68  
    2.69 @@ -21,7 +70,7 @@
    2.70  global
    2.71  
    2.72  typedef (Prod)
    2.73 -  ('a, 'b) "*"          (infixr 20)
    2.74 +  ('a, 'b) "*"    (infixr 20)
    2.75      = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}"
    2.76  proof
    2.77    fix a b show "Pair_Rep a b : ?Prod"
    2.78 @@ -98,24 +147,78 @@
    2.79    Sigma_def:    "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    2.80  
    2.81  
    2.82 -subsection {* Unit *}
    2.83 +subsubsection {* Lemmas and tool setup *}
    2.84 +
    2.85 +lemma ProdI: "Pair_Rep a b : Prod"
    2.86 +  by (unfold Prod_def) blast
    2.87 +
    2.88 +lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'"
    2.89 +  apply (unfold Pair_Rep_def)
    2.90 +  apply (drule fun_cong [THEN fun_cong])
    2.91 +  apply blast
    2.92 +  done
    2.93  
    2.94 -typedef unit = "{True}"
    2.95 -proof
    2.96 -  show "True : ?unit"
    2.97 -    by blast
    2.98 +lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod"
    2.99 +  apply (rule inj_on_inverseI)
   2.100 +  apply (erule Abs_Prod_inverse)
   2.101 +  done
   2.102 +
   2.103 +lemma Pair_inject:
   2.104 +  "(a, b) = (a', b') ==> (a = a' ==> b = b' ==> R) ==> R"
   2.105 +proof -
   2.106 +  case rule_context [unfolded Pair_def]
   2.107 +  show ?thesis
   2.108 +    apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE])
   2.109 +    apply (rule rule_context ProdI)+
   2.110 +    .
   2.111  qed
   2.112  
   2.113 -constdefs
   2.114 -  Unity :: unit    ("'(')")
   2.115 -  "() == Abs_unit True"
   2.116 +lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')"
   2.117 +  by (blast elim!: Pair_inject)
   2.118 +
   2.119 +lemma fst_conv [simp]: "fst (a, b) = a"
   2.120 +  by (unfold fst_def) blast
   2.121 +
   2.122 +lemma snd_conv [simp]: "snd (a, b) = b"
   2.123 +  by (unfold snd_def) blast
   2.124  
   2.125 +lemma fst_eqD: "fst (x, y) = a ==> x = a"
   2.126 +  by simp
   2.127 +
   2.128 +lemma snd_eqD: "snd (x, y) = a ==> y = a"
   2.129 +  by simp
   2.130 +
   2.131 +lemma PairE_lemma: "EX x y. p = (x, y)"
   2.132 +  apply (unfold Pair_def)
   2.133 +  apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE])
   2.134 +  apply (erule exE, erule exE, rule exI, rule exI)
   2.135 +  apply (rule Rep_Prod_inverse [symmetric, THEN trans])
   2.136 +  apply (erule arg_cong)
   2.137 +  done
   2.138  
   2.139 -subsection {* Lemmas and tool setup *}
   2.140 +lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q"
   2.141 +  by (insert PairE_lemma [of p]) blast
   2.142 +
   2.143 +ML_setup {*
   2.144 +  local val PairE = thm "PairE" in
   2.145 +    fun pair_tac s =
   2.146 +      EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac];
   2.147 +  end;
   2.148 +*}
   2.149  
   2.150 -use "Product_Type_lemmas.ML"
   2.151 +lemma surjective_pairing: "p = (fst p, snd p)"
   2.152 +  -- {* Do not add as rewrite rule: invalidates some proofs in IMP *}
   2.153 +  by (cases p) simp
   2.154 +
   2.155 +declare surjective_pairing [symmetric, simp]
   2.156  
   2.157 -lemma (*split_paired_all:*) "(!!x. PROP P x) == (!!a b. PROP P (a, b))"   (* FIXME unused *)
   2.158 +lemma surj_pair [simp]: "EX x y. z = (x, y)"
   2.159 +  apply (rule exI)
   2.160 +  apply (rule exI)
   2.161 +  apply (rule surjective_pairing)
   2.162 +  done
   2.163 +
   2.164 +lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
   2.165  proof
   2.166    fix a b
   2.167    assume "!!x. PROP P x"
   2.168 @@ -127,12 +230,457 @@
   2.169    thus "PROP P x" by simp
   2.170  qed
   2.171  
   2.172 +lemmas split_tupled_all = split_paired_all unit_all_eq2
   2.173 +
   2.174 +text {*
   2.175 +  The rule @{thm [source] split_paired_all} does not work with the
   2.176 +  Simplifier because it also affects premises in congrence rules,
   2.177 +  where this can lead to premises of the form @{text "!!a b. ... =
   2.178 +  ?P(a, b)"} which cannot be solved by reflexivity.
   2.179 +*}
   2.180 +
   2.181 +ML_setup "
   2.182 +  (* replace parameters of product type by individual component parameters *)
   2.183 +  val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   2.184 +  local (* filtering with exists_paired_all is an essential optimization *)
   2.185 +    fun exists_paired_all (Const (\"all\", _) $ Abs (_, T, t)) =
   2.186 +          can HOLogic.dest_prodT T orelse exists_paired_all t
   2.187 +      | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
   2.188 +      | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
   2.189 +      | exists_paired_all _ = false;
   2.190 +    val ss = HOL_basic_ss
   2.191 +      addsimps [thm \"split_paired_all\", thm \"unit_all_eq2\", thm \"unit_abs_eta_conv\"]
   2.192 +      addsimprocs [unit_eq_proc];
   2.193 +  in
   2.194 +    val split_all_tac = SUBGOAL (fn (t, i) =>
   2.195 +      if exists_paired_all t then safe_full_simp_tac ss i else no_tac);
   2.196 +    val unsafe_split_all_tac = SUBGOAL (fn (t, i) =>
   2.197 +      if exists_paired_all t then full_simp_tac ss i else no_tac);
   2.198 +    fun split_all th =
   2.199 +   if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
   2.200 +  end;
   2.201 +
   2.202 +claset_ref() := claset() addSbefore (\"split_all_tac\", split_all_tac);
   2.203 +"
   2.204 +
   2.205 +lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))"
   2.206 +  -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
   2.207 +  by fast
   2.208 +
   2.209 +lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x"
   2.210 +  by fast
   2.211 +
   2.212 +lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
   2.213 +  by fast
   2.214 +
   2.215 +lemma split_conv [simp]: "split c (a, b) = c a b"
   2.216 +  by (simp add: split_def)
   2.217 +
   2.218 +lemmas split = split_conv  -- {* for backwards compatibility *}
   2.219 +
   2.220 +lemmas splitI = split_conv [THEN iffD2, standard]
   2.221 +lemmas splitD = split_conv [THEN iffD1, standard]
   2.222 +
   2.223 +lemma split_Pair_apply: "split (%x y. f (x, y)) = f"
   2.224 +  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   2.225 +  apply (rule ext)
   2.226 +  apply (tactic {* pair_tac "x" 1 *})
   2.227 +  apply simp
   2.228 +  done
   2.229 +
   2.230 +lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))"
   2.231 +  -- {* Can't be added to simpset: loops! *}
   2.232 +  by (simp add: split_Pair_apply)
   2.233 +
   2.234 +lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
   2.235 +  by (simp add: split_def)
   2.236 +
   2.237 +lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)"
   2.238 +  apply (simp only: split_tupled_all)
   2.239 +  apply simp
   2.240 +  done
   2.241 +
   2.242 +lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q"
   2.243 +  by (simp add: Pair_fst_snd_eq)
   2.244 +
   2.245 +lemma split_weak_cong: "p = q ==> split c p = split c q"
   2.246 +  -- {* Prevents simplification of @{term c}: much faster *}
   2.247 +  by (erule arg_cong)
   2.248 +
   2.249 +lemma split_eta: "(%(x, y). f (x, y)) = f"
   2.250 +  apply (rule ext)
   2.251 +  apply (simp only: split_tupled_all)
   2.252 +  apply (rule split_conv)
   2.253 +  done
   2.254 +
   2.255 +lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   2.256 +  by (simp add: split_eta)
   2.257 +
   2.258 +text {*
   2.259 +  Simplification procedure for @{thm [source] cond_split_eta}.  Using
   2.260 +  @{thm [source] split_eta} as a rewrite rule is not general enough,
   2.261 +  and using @{thm [source] cond_split_eta} directly would render some
   2.262 +  existing proofs very inefficient; similarly for @{text
   2.263 +  split_beta}. *}
   2.264 +
   2.265 +ML_setup {*
   2.266 +
   2.267 +local
   2.268 +  val cond_split_eta = thm "cond_split_eta";
   2.269 +  fun  Pair_pat k 0 (Bound m) = (m = k)
   2.270 +  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
   2.271 +                        m = k+i andalso Pair_pat k (i-1) t
   2.272 +  |    Pair_pat _ _ _ = false;
   2.273 +  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
   2.274 +  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
   2.275 +  |   no_args k i (Bound m) = m < k orelse m > k+i
   2.276 +  |   no_args _ _ _ = true;
   2.277 +  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
   2.278 +  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
   2.279 +  |   split_pat tp i _ = None;
   2.280 +  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
   2.281 +        (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
   2.282 +        (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
   2.283 +  val sign = sign_of (the_context ());
   2.284 +  fun simproc name patstr = Simplifier.mk_simproc name
   2.285 +                [Thm.read_cterm sign (patstr, HOLogic.termT)];
   2.286 +
   2.287 +  val beta_patstr = "split f z";
   2.288 +  val  eta_patstr = "split f";
   2.289 +  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
   2.290 +  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
   2.291 +                        (beta_term_pat k i t andalso beta_term_pat k i u)
   2.292 +  |   beta_term_pat k i t = no_args k i t;
   2.293 +  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
   2.294 +  |    eta_term_pat _ _ _ = false;
   2.295 +  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
   2.296 +  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
   2.297 +                              else (subst arg k i t $ subst arg k i u)
   2.298 +  |   subst arg k i t = t;
   2.299 +  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
   2.300 +        (case split_pat beta_term_pat 1 t of
   2.301 +        Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
   2.302 +        | None => None)
   2.303 +  |   beta_proc _ _ _ = None;
   2.304 +  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
   2.305 +        (case split_pat eta_term_pat 1 t of
   2.306 +          Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
   2.307 +        | None => None)
   2.308 +  |   eta_proc _ _ _ = None;
   2.309 +in
   2.310 +  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
   2.311 +  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
   2.312 +end;
   2.313 +
   2.314 +Addsimprocs [split_beta_proc, split_eta_proc];
   2.315 +*}
   2.316 +
   2.317 +lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
   2.318 +  by (subst surjective_pairing, rule split_conv)
   2.319 +
   2.320 +lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
   2.321 +  -- {* For use with @{text split} and the Simplifier. *}
   2.322 +  apply (subst surjective_pairing)
   2.323 +  apply (subst split_conv)
   2.324 +  apply blast
   2.325 +  done
   2.326 +
   2.327 +text {*
   2.328 +  @{thm [source] split_split} could be declared as @{text "[split]"}
   2.329 +  done after the Splitter has been speeded up significantly;
   2.330 +  precompute the constants involved and don't do anything unless the
   2.331 +  current goal contains one of those constants.
   2.332 +*}
   2.333 +
   2.334 +lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
   2.335 +  apply (subst split_split)
   2.336 +  apply simp
   2.337 +  done
   2.338 +
   2.339 +
   2.340 +text {*
   2.341 +  \medskip @{term split} used as a logical connective or set former.
   2.342 +
   2.343 +  \medskip These rules are for use with @{text blast}; could instead
   2.344 +  call @{text simp} using @{thm [source] split} as rewrite. *}
   2.345 +
   2.346 +lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
   2.347 +  apply (simp only: split_tupled_all)
   2.348 +  apply (simp (no_asm_simp))
   2.349 +  done
   2.350 +
   2.351 +lemma splitI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> split c p x"
   2.352 +  apply (simp only: split_tupled_all)
   2.353 +  apply (simp (no_asm_simp))
   2.354 +  done
   2.355 +
   2.356 +lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
   2.357 +  by (induct p) (auto simp add: split_def)
   2.358 +
   2.359 +lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
   2.360 +  by (induct p) (auto simp add: split_def)
   2.361 +
   2.362 +lemma splitE2:
   2.363 +  "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
   2.364 +proof -
   2.365 +  assume q: "Q (split P z)"
   2.366 +  assume r: "!!x y. [|z = (x, y); Q (P x y)|] ==> R"
   2.367 +  show R
   2.368 +    apply (rule r surjective_pairing)+
   2.369 +    apply (rule split_beta [THEN subst], rule q)
   2.370 +    done
   2.371 +qed
   2.372 +
   2.373 +lemma splitD': "split R (a,b) c ==> R a b c"
   2.374 +  by simp
   2.375 +
   2.376 +lemma mem_splitI: "z: c a b ==> z: split c (a, b)"
   2.377 +  by simp
   2.378 +
   2.379 +lemma mem_splitI2: "!!p. [| !!a b. p = (a, b) ==> z: c a b |] ==> z: split c p"
   2.380 +  apply (simp only: split_tupled_all)
   2.381 +  apply simp
   2.382 +  done
   2.383 +
   2.384 +lemma mem_splitE: "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"
   2.385 +proof -
   2.386 +  case rule_context [unfolded split_def]
   2.387 +  show ?thesis by (rule rule_context surjective_pairing)+
   2.388 +qed
   2.389 +
   2.390 +declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
   2.391 +declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
   2.392 +
   2.393 +ML_setup "
   2.394 +local (* filtering with exists_p_split is an essential optimization *)
   2.395 +  fun exists_p_split (Const (\"split\",_) $ _ $ (Const (\"Pair\",_)$_$_)) = true
   2.396 +    | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
   2.397 +    | exists_p_split (Abs (_, _, t)) = exists_p_split t
   2.398 +    | exists_p_split _ = false;
   2.399 +  val ss = HOL_basic_ss addsimps [thm \"split_conv\"];
   2.400 +in
   2.401 +val split_conv_tac = SUBGOAL (fn (t, i) =>
   2.402 +    if exists_p_split t then safe_full_simp_tac ss i else no_tac);
   2.403 +end;
   2.404 +(* This prevents applications of splitE for already splitted arguments leading
   2.405 +   to quite time-consuming computations (in particular for nested tuples) *)
   2.406 +claset_ref() := claset() addSbefore (\"split_conv_tac\", split_conv_tac);
   2.407 +"
   2.408 +
   2.409 +lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   2.410 +  apply (rule ext)
   2.411 +  apply fast
   2.412 +  done
   2.413 +
   2.414 +lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   2.415 +  apply (rule ext)
   2.416 +  apply fast
   2.417 +  done
   2.418 +
   2.419 +lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   2.420 +  -- {* Allows simplifications of nested splits in case of independent predicates. *}
   2.421 +  apply (rule ext)
   2.422 +  apply blast
   2.423 +  done
   2.424 +
   2.425 +lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   2.426 +  by blast
   2.427 +
   2.428 +(*
   2.429 +the following  would be slightly more general,
   2.430 +but cannot be used as rewrite rule:
   2.431 +### Cannot add premise as rewrite rule because it contains (type) unknowns:
   2.432 +### ?y = .x
   2.433 +Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"
   2.434 +by (rtac some_equality 1);
   2.435 +by ( Simp_tac 1);
   2.436 +by (split_all_tac 1);
   2.437 +by (Asm_full_simp_tac 1);
   2.438 +qed "The_split_eq";
   2.439 +*)
   2.440 +
   2.441 +lemma injective_fst_snd: "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y"
   2.442 +  by auto
   2.443 +
   2.444 +
   2.445 +text {*
   2.446 +  \bigskip @{term prod_fun} --- action of the product functor upon
   2.447 +  functions.
   2.448 +*}
   2.449 +
   2.450 +lemma prod_fun [simp]: "prod_fun f g (a, b) = (f a, g b)"
   2.451 +  by (simp add: prod_fun_def)
   2.452 +
   2.453 +lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
   2.454 +  apply (rule ext)
   2.455 +  apply (tactic {* pair_tac "x" 1 *})
   2.456 +  apply simp
   2.457 +  done
   2.458 +
   2.459 +lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
   2.460 +  apply (rule ext)
   2.461 +  apply (tactic {* pair_tac "z" 1 *})
   2.462 +  apply simp
   2.463 +  done
   2.464 +
   2.465 +lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
   2.466 +  apply (rule image_eqI)
   2.467 +  apply (rule prod_fun [symmetric])
   2.468 +  apply assumption
   2.469 +  done
   2.470 +
   2.471 +lemma prod_fun_imageE [elim!]:
   2.472 +  "[| c: (prod_fun f g)`r;  !!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P
   2.473 +    |] ==> P"
   2.474 +proof -
   2.475 +  case rule_context
   2.476 +  assume major: "c: (prod_fun f g)`r"
   2.477 +  show ?thesis
   2.478 +    apply (rule major [THEN imageE])
   2.479 +    apply (rule_tac p = x in PairE)
   2.480 +    apply (rule rule_context)
   2.481 +     prefer 2
   2.482 +     apply blast
   2.483 +    apply (blast intro: prod_fun)
   2.484 +    done
   2.485 +qed
   2.486 +
   2.487 +
   2.488 +text {*
   2.489 +  \bigskip Disjoint union of a family of sets -- Sigma.
   2.490 +*}
   2.491 +
   2.492 +lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   2.493 +  by (unfold Sigma_def) blast
   2.494 +
   2.495 +
   2.496 +lemma SigmaE:
   2.497 +    "[| c: Sigma A B;
   2.498 +        !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P
   2.499 +     |] ==> P"
   2.500 +  -- {* The general elimination rule. *}
   2.501 +  by (unfold Sigma_def) blast
   2.502 +
   2.503 +text {*
   2.504 +  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
   2.505 +  eigenvariables.
   2.506 +*}
   2.507 +
   2.508 +lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
   2.509 +  apply (erule SigmaE)
   2.510 +  apply blast
   2.511 +  done
   2.512 +
   2.513 +lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
   2.514 +  apply (erule SigmaE)
   2.515 +  apply blast
   2.516 +  done
   2.517 +
   2.518 +lemma SigmaE2:
   2.519 +    "[| (a, b) : Sigma A B;
   2.520 +        [| a:A;  b:B(a) |] ==> P
   2.521 +     |] ==> P"
   2.522 +  by (blast dest: SigmaD1 SigmaD2)
   2.523 +
   2.524 +declare SigmaE [elim!] SigmaE2 [elim!]
   2.525 +
   2.526 +lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   2.527 +  by blast
   2.528 +
   2.529 +lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
   2.530 +  by blast
   2.531 +
   2.532 +lemma Sigma_empty2 [simp]: "A <*> {} = {}"
   2.533 +  by blast
   2.534 +
   2.535 +lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV"
   2.536 +  by auto
   2.537 +
   2.538 +lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)"
   2.539 +  by auto
   2.540 +
   2.541 +lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV"
   2.542 +  by auto
   2.543 +
   2.544 +lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
   2.545 +  by blast
   2.546 +
   2.547 +lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)"
   2.548 +  by blast
   2.549 +
   2.550 +lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)"
   2.551 +  by (blast elim: equalityE)
   2.552 +
   2.553 +lemma SetCompr_Sigma_eq:
   2.554 +    "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"
   2.555 +  by blast
   2.556 +
   2.557 +text {*
   2.558 +  \bigskip Complex rules for Sigma.
   2.559 +*}
   2.560 +
   2.561 +lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q"
   2.562 +  by blast
   2.563 +
   2.564 +lemma UN_Times_distrib:
   2.565 +  "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"
   2.566 +  -- {* Suggested by Pierre Chartier *}
   2.567 +  by blast
   2.568 +
   2.569 +lemma split_paired_Ball_Sigma [simp]:
   2.570 +    "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   2.571 +  by blast
   2.572 +
   2.573 +lemma split_paired_Bex_Sigma [simp]:
   2.574 +    "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   2.575 +  by blast
   2.576 +
   2.577 +lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"
   2.578 +  by blast
   2.579 +
   2.580 +lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"
   2.581 +  by blast
   2.582 +
   2.583 +lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"
   2.584 +  by blast
   2.585 +
   2.586 +lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"
   2.587 +  by blast
   2.588 +
   2.589 +lemma Sigma_Diff_distrib1: "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))"
   2.590 +  by blast
   2.591 +
   2.592 +lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))"
   2.593 +  by blast
   2.594 +
   2.595 +lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)"
   2.596 +  by blast
   2.597 +
   2.598 +text {*
   2.599 +  Non-dependent versions are needed to avoid the need for higher-order
   2.600 +  matching, especially when the rules are re-oriented.
   2.601 +*}
   2.602 +
   2.603 +lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)"
   2.604 +  by blast
   2.605 +
   2.606 +lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)"
   2.607 +  by blast
   2.608 +
   2.609 +lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)"
   2.610 +  by blast
   2.611 +
   2.612 +
   2.613  lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   2.614    apply (rule_tac x = "(a, b)" in image_eqI)
   2.615     apply auto
   2.616    done
   2.617  
   2.618  
   2.619 +text {*
   2.620 +  Setup of internal @{text split_rule}.
   2.621 +*}
   2.622 +
   2.623  constdefs
   2.624    internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c"
   2.625    "internal_split == split"
     3.1 --- a/src/HOL/Tools/split_rule.ML	Fri Oct 19 22:00:08 2001 +0200
     3.2 +++ b/src/HOL/Tools/split_rule.ML	Fri Oct 19 22:01:25 2001 +0200
     3.3 @@ -26,6 +26,10 @@
     3.4  
     3.5  (** theory context references **)
     3.6  
     3.7 +val split_conv = thm "split_conv";
     3.8 +val fst_conv = thm "fst_conv";
     3.9 +val snd_conv = thm "snd_conv";
    3.10 +
    3.11  fun internal_split_const (Ta, Tb, Tc) =
    3.12    Const ("Product_Type.internal_split", [[Ta, Tb] ---> Tc, HOLogic.mk_prodT (Ta, Tb)] ---> Tc);
    3.13