<commit_before>(*  Title:      HOL/prod
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

For prod.thy.  Ordered Pairs, the Cartesian product type, the unit type
*)

open Prod;

(*This counts as a non-emptiness result for admitting 'a * 'b as a type*)
goalw Prod.thy [Prod_def] "Pair_Rep a b : Prod";
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
qed "ProdI";

val [major] = goalw Prod.thy [Pair_Rep_def]
    "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), 
            rtac conjI, rtac refl, rtac refl]);
qed "Pair_Rep_inject";

goal Prod.thy "inj_onto Abs_Prod Prod";
by (rtac inj_onto_inverseI 1);
by (etac Abs_Prod_inverse 1);
qed "inj_onto_Abs_Prod";

val prems = goalw Prod.thy [Pair_def]
    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
by (REPEAT (ares_tac (prems@[ProdI]) 1));
qed "Pair_inject";

goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
by (blast_tac (claset() addSEs [Pair_inject]) 1);
qed "Pair_eq";
AddIffs [Pair_eq];

goalw Prod.thy [fst_def] "fst((a,b)) = a";
by (Blast_tac 1);
qed "fst_conv";
goalw Prod.thy [snd_def] "snd((a,b)) = b";
by (Blast_tac 1);
qed "snd_conv";
Addsimps [fst_conv, snd_conv];

goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
qed "PairE_lemma";

val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
by (rtac (PairE_lemma RS exE) 1);
by (REPEAT (eresolve_tac [prem,exE] 1));
qed "PairE";

fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;

(* replace parameters of product type by individual component parameters *)
local
fun is_pair (_,Type("*",_)) = true
  | is_pair _ = false;

fun find_pair_param prem =
  let val params = Logic.strip_params prem
  in if exists is_pair params
     then let val params = rev(rename_wrt_term prem params)
                           (*as they are printed*)
          in apsome fst (find_first is_pair params) end
     else None
  end;

in

val split_all_tac = REPEAT1 o SUBGOAL (fn (prem,i) =>
  case find_pair_param prem of
    None => no_tac
  | Some x => EVERY[res_inst_tac[("p",x)] PairE i,
                    REPEAT(hyp_subst_tac i), prune_params_tac]);

end;

(* claset_ref() := claset() addbefore  ("split_all_tac", TRY o split_all_tac);*)
   claset_ref() := claset() addSaltern ("split_all_tac",       split_all_tac);

(*** lemmas for splitting paired `!!'
Does not work with simplifier because it also affects premises in
congrence rules, where is can lead to premises of the form
!!a b. ... = ?P(a,b)
which cannot be solved by reflexivity.
   
val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))";
by (rtac prem 1);
val lemma1 = result();

local
    val psig = sign_of Prod.thy;
    val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
    val PeqP = reflexive(read_cterm psig ("P", pT));
    val psplit = zero_var_indexes(read_instantiate [("p","x")]
                                  surjective_pairing RS eq_reflection)
in
val adhoc = combination PeqP psplit
end;


val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
by (rewtac adhoc);
by (rtac prem 1);
val lemma = result();

val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
by (rtac lemma 1);
by (rtac prem 1);
val lemma2 = result();

bind_thm("split_paired_all", equal_intr lemma1 lemma2);
Addsimps [split_paired_all];
***)

goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
by (Fast_tac 1);
qed "split_paired_All";
Addsimps [split_paired_All];
(* AddIffs is not a good idea because it makes Blast_tac loop *)

goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
by (Fast_tac 1);
qed "split_paired_Ex";
Addsimps [split_paired_Ex];

goalw Prod.thy [split_def] "split c (a,b) = c a b";
by (Simp_tac 1);
qed "split";
Addsimps [split];

goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
by (res_inst_tac[("p","s")] PairE 1);
by (res_inst_tac[("p","t")] PairE 1);
by (Asm_simp_tac 1);
qed "Pair_fst_snd_eq";

(*Prevents simplification of c: much faster*)
qed_goal "split_weak_cong" Prod.thy
  "p=q ==> split c p = split c q"
  (fn [prem] => [rtac (prem RS arg_cong) 1]);

(* Do not add as rewrite rule: invalidates some proofs in IMP *)
goal Prod.thy "p = (fst(p),snd(p))";
by (res_inst_tac [("p","p")] PairE 1);
by (Asm_simp_tac 1);
qed "surjective_pairing";

goal Prod.thy "p = split (%x y.(x,y)) p";
by (res_inst_tac [("p","p")] PairE 1);
by (Asm_simp_tac 1);
qed "surjective_pairing2";

val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
Addsimps [surj_pair];

qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
  (K [rtac ext 1, split_all_tac 1, rtac split 1]);

val split_beta = prove_goal Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);

(*For use with split_tac and the simplifier*)<commit_msg>improved pair_tac to call prune_params_tac afterwards improved the (bad) efficiency of split_all_tac by about 50% split_all_tac is now added to claset() _before_ other safe tactics<commit_after>(*  Title:      HOL/prod
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

For prod.thy.  Ordered Pairs, the Cartesian product type, the unit type
*)

open Prod;

(*This counts as a non-emptiness result for admitting 'a * 'b as a type*)
goalw Prod.thy [Prod_def] "Pair_Rep a b : Prod";
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
qed "ProdI";

val [major] = goalw Prod.thy [Pair_Rep_def]
    "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), 
            rtac conjI, rtac refl, rtac refl]);
qed "Pair_Rep_inject";

goal Prod.thy "inj_onto Abs_Prod Prod";
by (rtac inj_onto_inverseI 1);
by (etac Abs_Prod_inverse 1);
qed "inj_onto_Abs_Prod";

val prems = goalw Prod.thy [Pair_def]
    "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
by (REPEAT (ares_tac (prems@[ProdI]) 1));
qed "Pair_inject";

goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')";
by (blast_tac (claset() addSEs [Pair_inject]) 1);
qed "Pair_eq";
AddIffs [Pair_eq];

goalw Prod.thy [fst_def] "fst((a,b)) = a";
by (Blast_tac 1);
qed "fst_conv";
goalw Prod.thy [snd_def] "snd((a,b)) = b";
by (Blast_tac 1);
qed "snd_conv";
Addsimps [fst_conv, snd_conv];

goalw Prod.thy [Pair_def] "? x y. p = (x,y)";
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
           rtac (Rep_Prod_inverse RS sym RS trans),  etac arg_cong]);
qed "PairE_lemma";

val [prem] = goal Prod.thy "[| !!x y. p = (x,y) ==> Q |] ==> Q";
by (rtac (PairE_lemma RS exE) 1);
by (REPEAT (eresolve_tac [prem,exE] 1));
qed "PairE";

fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
			 K prune_params_tac];

(* replace parameters of product type by individual component parameters *)
local
  fun is_pair (_,Type("*",_)) = true
    | is_pair  _              = false;
  fun ptac x = res_inst_tac [("p",x)] PairE;
  fun find_pair_params prem =
    let val params = Logic.strip_params prem
    in if exists is_pair params
       then let val params = rev(rename_wrt_term prem params)
                             (*as they are printed*)
            in filter is_pair params end
       else []
   end;
in
val split_all_tac = REPEAT1 o SUBGOAL (fn (prem,i) => 
  let val params = find_pair_params prem in
  if params = [] then no_tac 
  	         else EVERY'[EVERY' (map (ptac o fst) params),
			     REPEAT o hyp_subst_tac,
			     K prune_params_tac] i end)
end;

(*claset_ref() := claset()  addbefore  ("split_all_tac", TRY o split_all_tac);*)
  claset_ref() := claset() addSWrapper ("split_all_tac", 
					fn tac2 => split_all_tac ORELSE' tac2);

(*** lemmas for splitting paired `!!'
Does not work with simplifier because it also affects premises in
congrence rules, where is can lead to premises of the form
!!a b. ... = ?P(a,b)
which cannot be solved by reflexivity.
   
val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))";
by (rtac prem 1);
val lemma1 = result();

local
    val psig = sign_of Prod.thy;
    val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
    val PeqP = reflexive(read_cterm psig ("P", pT));
    val psplit = zero_var_indexes(read_instantiate [("p","x")]
                                  surjective_pairing RS eq_reflection)
in
val adhoc = combination PeqP psplit
end;


val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
by (rewtac adhoc);
by (rtac prem 1);
val lemma = result();

val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
by (rtac lemma 1);
by (rtac prem 1);
val lemma2 = result();

bind_thm("split_paired_all", equal_intr lemma1 lemma2);
Addsimps [split_paired_all];
***)

goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
by (Fast_tac 1);
qed "split_paired_All";
Addsimps [split_paired_All];
(* AddIffs is not a good idea because it makes Blast_tac loop *)

goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
by (Fast_tac 1);
qed "split_paired_Ex";
Addsimps [split_paired_Ex];

goalw Prod.thy [split_def] "split c (a,b) = c a b";
by (Simp_tac 1);
qed "split";
Addsimps [split];

goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
by (res_inst_tac[("p","s")] PairE 1);
by (res_inst_tac[("p","t")] PairE 1);
by (Asm_simp_tac 1);
qed "Pair_fst_snd_eq";

(*Prevents simplification of c: much faster*)
qed_goal "split_weak_cong" Prod.thy
  "p=q ==> split c p = split c q"
  (fn [prem] => [rtac (prem RS arg_cong) 1]);

(* Do not add as rewrite rule: invalidates some proofs in IMP *)
goal Prod.thy "p = (fst(p),snd(p))";
by (res_inst_tac [("p","p")] PairE 1);
by (Asm_simp_tac 1);
qed "surjective_pairing";

goal Prod.thy "p = split (%x y.(x,y)) p";
by (res_inst_tac [("p","p")] PairE 1);
by (Asm_simp_tac 1);
qed "surjective_pairing2";

val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [
	rtac exI 1, rtac exI 1, rtac surjective_pairing 1]);
Addsimps [surj_pair];

qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
  (K [rtac ext 1, split_all_tac 1, rtac split 1]);

qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);

(*For use with split_tac and the simplifier*)
{'fraction_non_alphanumeric': 0.1603640799474524, 'fraction_numerical': 0.009195833724312659, 'mean_word_length': 3.824807605251245, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 32, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '298061', 'n_tokens_mistral': 4688, 'n_tokens_neox': 4419, 'n_words': 1379}