author | nipkow |
Mon, 06 Aug 2001 13:43:24 +0200 | |
changeset 11464 | ddea204de5bc |
parent 11451 | 8abfb4f7bd02 |
permissions | -rw-r--r-- |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
1 |
(* Title: HOL/Product_Type_lemmas.ML |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
2 |
ID: $Id$ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
4 |
Copyright 1991 University of Cambridge |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
5 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
6 |
Ordered Pairs, the Cartesian product type, the unit type |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
7 |
*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
8 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
9 |
(* ML bindings *) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
10 |
val Pair_def = thm "Pair_def"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
11 |
val fst_def = thm "fst_def"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
12 |
val snd_def = thm "snd_def"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
13 |
val split_def = thm "split_def"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
14 |
val prod_fun_def = thm "prod_fun_def"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
15 |
val Sigma_def = thm "Sigma_def"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
16 |
val Unity_def = thm "Unity_def"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
17 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
18 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
19 |
(** unit **) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
20 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
21 |
Goalw [Unity_def] "u = ()"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
22 |
by (stac (rewrite_rule [thm"unit_def"] (thm"Rep_unit") RS singletonD RS sym) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
23 |
by (rtac (thm "Rep_unit_inverse" RS sym) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
24 |
qed "unit_eq"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
25 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
26 |
(*simplification procedure for unit_eq. |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
27 |
Cannot use this rule directly -- it loops!*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
28 |
local |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
29 |
val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
30 |
val unit_meta_eq = standard (mk_meta_eq unit_eq); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
31 |
fun proc _ _ t = |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
32 |
if HOLogic.is_unit t then None |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
33 |
else Some unit_meta_eq; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
34 |
in |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
35 |
val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
36 |
end; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
37 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
38 |
Addsimprocs [unit_eq_proc]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
39 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
40 |
Goal "(!!x::unit. PROP P x) == PROP P ()"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
41 |
by (Simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
42 |
qed "unit_all_eq1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
43 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
44 |
Goal "(!!x::unit. PROP P) == PROP P"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
45 |
by (rtac triv_forall_equality 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
46 |
qed "unit_all_eq2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
47 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
48 |
Goal "P () ==> P x"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
49 |
by (Simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
50 |
qed "unit_induct"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
51 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
52 |
(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
53 |
replacing it by f rather than by %u.f(). *) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
54 |
Goal "(%u::unit. f()) = f"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
55 |
by (rtac ext 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
56 |
by (Simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
57 |
qed "unit_abs_eta_conv"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
58 |
Addsimps [unit_abs_eta_conv]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
59 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
60 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
61 |
(** prod **) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
62 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
63 |
Goalw [thm "Prod_def"] "Pair_Rep a b : Prod"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
64 |
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
65 |
qed "ProdI"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
66 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
67 |
Goalw [thm "Pair_Rep_def"] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
68 |
by (dtac (fun_cong RS fun_cong) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
69 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
70 |
qed "Pair_Rep_inject"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
71 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
72 |
Goal "inj_on Abs_Prod Prod"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
73 |
by (rtac inj_on_inverseI 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
74 |
by (etac (thm "Abs_Prod_inverse") 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
75 |
qed "inj_on_Abs_Prod"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
76 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
77 |
val prems = Goalw [Pair_def] |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
78 |
"[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
79 |
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
80 |
by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
81 |
qed "Pair_inject"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
82 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
83 |
Goal "((a,b) = (a',b')) = (a=a' & b=b')"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
84 |
by (blast_tac (claset() addSEs [Pair_inject]) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
85 |
qed "Pair_eq"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
86 |
AddIffs [Pair_eq]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
87 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
88 |
Goalw [fst_def] "fst (a,b) = a"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
89 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
90 |
qed "fst_conv"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
91 |
Goalw [snd_def] "snd (a,b) = b"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
92 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
93 |
qed "snd_conv"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
94 |
Addsimps [fst_conv, snd_conv]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
95 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
96 |
Goal "fst (x, y) = a ==> x = a"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
97 |
by (Asm_full_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
98 |
qed "fst_eqD"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
99 |
Goal "snd (x, y) = a ==> y = a"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
100 |
by (Asm_full_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
101 |
qed "snd_eqD"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
102 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
103 |
Goalw [Pair_def] "? x y. p = (x,y)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
104 |
by (rtac (rewrite_rule [thm "Prod_def"] (thm "Rep_Prod") RS CollectE) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
105 |
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
106 |
rtac (thm "Rep_Prod_inverse" RS sym RS trans), etac arg_cong]); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
107 |
qed "PairE_lemma"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
108 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
109 |
val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
110 |
by (rtac (PairE_lemma RS exE) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
111 |
by (REPEAT (eresolve_tac [prem,exE] 1)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
112 |
qed "PairE"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
113 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
114 |
fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac, |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
115 |
K prune_params_tac]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
116 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
117 |
(* Do not add as rewrite rule: invalidates some proofs in IMP *) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
118 |
Goal "p = (fst(p),snd(p))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
119 |
by (pair_tac "p" 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
120 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
121 |
qed "surjective_pairing"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
122 |
Addsimps [surjective_pairing RS sym]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
123 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
124 |
Goal "? x y. z = (x, y)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
125 |
by (rtac exI 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
126 |
by (rtac exI 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
127 |
by (rtac surjective_pairing 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
128 |
qed "surj_pair"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
129 |
Addsimps [surj_pair]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
130 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
131 |
bind_thm ("split_paired_all", |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
132 |
SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection))); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
133 |
bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
134 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
135 |
(* |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
136 |
Addsimps [split_paired_all] does not work with simplifier |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
137 |
because it also affects premises in congrence rules, |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
138 |
where is can lead to premises of the form !!a b. ... = ?P(a,b) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
139 |
which cannot be solved by reflexivity. |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
140 |
*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
141 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
142 |
(* replace parameters of product type by individual component parameters *) |
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
143 |
val safe_full_simp_tac = generic_simp_tac true (true, false, false); |
11180
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
144 |
local (* filtering with exists_paired_all is an essential optimization *) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
145 |
fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
146 |
can HOLogic.dest_prodT T orelse exists_paired_all t |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
147 |
| exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
148 |
| exists_paired_all (Abs (_, _, t)) = exists_paired_all t |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
149 |
| exists_paired_all _ = false; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
150 |
val ss = HOL_basic_ss |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
151 |
addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv] |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
152 |
addsimprocs [unit_eq_proc]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
153 |
in |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
154 |
val split_all_tac = SUBGOAL (fn (t, i) => |
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
155 |
if exists_paired_all t then safe_full_simp_tac ss i else no_tac); |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
156 |
val unsafe_split_all_tac = SUBGOAL (fn (t, i) => |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
157 |
if exists_paired_all t then full_simp_tac ss i else no_tac); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
158 |
fun split_all th = |
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
159 |
if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
160 |
end; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
161 |
|
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
162 |
claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac); |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
163 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
164 |
Goal "(!x. P x) = (!a b. P(a,b))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
165 |
by (Fast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
166 |
qed "split_paired_All"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
167 |
Addsimps [split_paired_All]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
168 |
(* AddIffs is not a good idea because it makes Blast_tac loop *) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
169 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
170 |
bind_thm ("prod_induct", |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
171 |
allI RS (allI RS (split_paired_All RS iffD2)) RS spec); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
172 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
173 |
Goal "(? x. P x) = (? a b. P(a,b))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
174 |
by (Fast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
175 |
qed "split_paired_Ex"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
176 |
Addsimps [split_paired_Ex]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
177 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
178 |
Goalw [split_def] "split c (a,b) = c a b"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
179 |
by (Simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
180 |
qed "split_conv"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
181 |
Addsimps [split_conv]; |
11033 | 182 |
bind_thm ("split", split_conv); (*for compatibility*) |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
183 |
|
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
184 |
bind_thm ("splitI", split_conv RS iffD2); |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
185 |
bind_thm ("splitD", split_conv RS iffD1); |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
186 |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
187 |
(*Subsumes the old split_Pair when f is the identity function*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
188 |
Goal "split (%x y. f(x,y)) = f"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
189 |
by (rtac ext 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
190 |
by (pair_tac "x" 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
191 |
by (Simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
192 |
qed "split_Pair_apply"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
193 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
194 |
(*Can't be added to simpset: loops!*) |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
195 |
Goal "(THE x. P x) = (THE (a,b). P(a,b))"; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
196 |
by (simp_tac (simpset() addsimps [split_Pair_apply]) 1); |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
197 |
qed "split_paired_The"; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
198 |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
199 |
Goalw [split_def] "The (split P) = (THE xy. P (fst xy) (snd xy))"; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
200 |
by (rtac refl 1); |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
201 |
qed "The_split"; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
202 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
203 |
Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
204 |
by (split_all_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
205 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
206 |
qed "Pair_fst_snd_eq"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
207 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
208 |
Goal "fst p = fst q ==> snd p = snd q ==> p = q"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
209 |
by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
210 |
qed "prod_eqI"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
211 |
AddXIs [prod_eqI]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
212 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
213 |
(*Prevents simplification of c: much faster*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
214 |
Goal "p=q ==> split c p = split c q"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
215 |
by (etac arg_cong 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
216 |
qed "split_weak_cong"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
217 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
218 |
Goal "(%(x,y). f(x,y)) = f"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
219 |
by (rtac ext 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
220 |
by (split_all_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
221 |
by (rtac split_conv 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
222 |
qed "split_eta"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
223 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
224 |
val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
225 |
by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
226 |
qed "cond_split_eta"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
227 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
228 |
(*simplification procedure for cond_split_eta. |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
229 |
using split_eta a rewrite rule is not general enough, and using |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
230 |
cond_split_eta directly would render some existing proofs very inefficient. |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
231 |
similarly for split_beta. *) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
232 |
local |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
233 |
fun Pair_pat k 0 (Bound m) = (m = k) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
234 |
| Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
235 |
m = k+i andalso Pair_pat k (i-1) t |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
236 |
| Pair_pat _ _ _ = false; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
237 |
fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
238 |
| no_args k i (t $ u) = no_args k i t andalso no_args k i u |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
239 |
| no_args k i (Bound m) = m < k orelse m > k+i |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
240 |
| no_args _ _ _ = true; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
241 |
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
242 |
| split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
243 |
| split_pat tp i _ = None; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
244 |
fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
245 |
(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
246 |
(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1])); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
247 |
val sign = sign_of (the_context ()); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
248 |
fun simproc name patstr = Simplifier.mk_simproc name |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
249 |
[Thm.read_cterm sign (patstr, HOLogic.termT)]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
250 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
251 |
val beta_patstr = "split f z"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
252 |
val eta_patstr = "split f"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
253 |
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
254 |
| beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
255 |
(beta_term_pat k i t andalso beta_term_pat k i u) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
256 |
| beta_term_pat k i t = no_args k i t; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
257 |
fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
258 |
| eta_term_pat _ _ _ = false; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
259 |
fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
260 |
| subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
261 |
else (subst arg k i t $ subst arg k i u) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
262 |
| subst arg k i t = t; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
263 |
fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
264 |
(case split_pat beta_term_pat 1 t of |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
265 |
Some (i,f) => Some (metaeq sg s (subst arg 0 i f)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
266 |
| None => None) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
267 |
| beta_proc _ _ _ = None; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
268 |
fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
269 |
(case split_pat eta_term_pat 1 t of |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
270 |
Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end)) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
271 |
| None => None) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
272 |
| eta_proc _ _ _ = None; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
273 |
in |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
274 |
val split_beta_proc = simproc "split_beta" beta_patstr beta_proc; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
275 |
val split_eta_proc = simproc "split_eta" eta_patstr eta_proc; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
276 |
end; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
277 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
278 |
Addsimprocs [split_beta_proc,split_eta_proc]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
279 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
280 |
Goal "(%(x,y). P x y) z = P (fst z) (snd z)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
281 |
by (stac surjective_pairing 1 THEN rtac split_conv 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
282 |
qed "split_beta"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
283 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
284 |
(*For use with split_tac and the simplifier*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
285 |
Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
286 |
by (stac surjective_pairing 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
287 |
by (stac split_conv 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
288 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
289 |
qed "split_split"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
290 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
291 |
(* could be done after split_tac has been speeded up significantly: |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
292 |
simpset_ref() := simpset() addsplits [split_split]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
293 |
precompute the constants involved and don't do anything unless |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
294 |
the current goal contains one of those constants |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
295 |
*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
296 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
297 |
Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
298 |
by (stac split_split 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
299 |
by (Simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
300 |
qed "split_split_asm"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
301 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
302 |
(** split used as a logical connective or set former **) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
303 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
304 |
(*These rules are for use with blast_tac. |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
305 |
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
306 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
307 |
Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
308 |
by (split_all_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
309 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
310 |
qed "splitI2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
311 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
312 |
Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
313 |
by (split_all_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
314 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
315 |
qed "splitI2'"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
316 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
317 |
val prems = Goalw [split_def] |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
318 |
"[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
319 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
320 |
qed "splitE"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
321 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
322 |
val prems = Goalw [split_def] |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
323 |
"[| split c p z; !!x y. [| p = (x,y); c x y z |] ==> Q |] ==> Q"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
324 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
325 |
qed "splitE'"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
326 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
327 |
val major::prems = Goal |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
328 |
"[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R \ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
329 |
\ |] ==> R"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
330 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
331 |
by (rtac (split_beta RS subst) 1 THEN rtac major 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
332 |
qed "splitE2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
333 |
|
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
334 |
Goal "split R (a,b) c ==> R a b c"; |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
335 |
by (Asm_full_simp_tac 1); |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
336 |
qed "splitD'"; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
337 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
338 |
Goal "z: c a b ==> z: split c (a,b)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
339 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
340 |
qed "mem_splitI"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
341 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
342 |
Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
343 |
by (split_all_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
344 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
345 |
qed "mem_splitI2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
346 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
347 |
val prems = Goalw [split_def] |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
348 |
"[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
349 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
350 |
qed "mem_splitE"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
351 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
352 |
AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
353 |
AddSEs [splitE, splitE', mem_splitE]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
354 |
|
11180
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
355 |
local (* filtering with exists_p_split is an essential optimization *) |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
356 |
fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
357 |
| exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
358 |
| exists_p_split (Abs (_, _, t)) = exists_p_split t |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
359 |
| exists_p_split _ = false; |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
360 |
val ss = HOL_basic_ss addsimps [split_conv] |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
361 |
in |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
362 |
val split_conv_tac = SUBGOAL (fn (t, i) => |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
363 |
if exists_p_split t then safe_full_simp_tac ss i else no_tac); |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
364 |
end; |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
365 |
(* This prevents applications of splitE for already splitted arguments leading |
39d3b8e8ad5c
removed performance leak for split_conv_tac (and corresponding safe wrapper)
oheimb
parents:
11170
diff
changeset
|
366 |
to quite time-consuming computations (in particular for nested tuples) *) |
11170
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
367 |
claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac); |
015af2fc7026
simplified proofs for splitI and splitD, added splitD'
oheimb
parents:
11033
diff
changeset
|
368 |
|
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
369 |
Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
370 |
by (rtac ext 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
371 |
by (Fast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
372 |
qed "split_eta_SetCompr"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
373 |
Addsimps [split_eta_SetCompr]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
374 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
375 |
Goal "(%u. ? x y. u = (x, y) & P x y) = split P"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
376 |
br ext 1; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
377 |
by (Fast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
378 |
qed "split_eta_SetCompr2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
379 |
Addsimps [split_eta_SetCompr2]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
380 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
381 |
(* allows simplifications of nested splits in case of independent predicates *) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
382 |
Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
383 |
by (rtac ext 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
384 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
385 |
qed "split_part"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
386 |
Addsimps [split_part]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
387 |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
388 |
Goal "(THE (x',y'). x = x' & y = y') = (x,y)"; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
389 |
by (Blast_tac 1); |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
390 |
qed "The_split_eq"; |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
391 |
Addsimps [The_split_eq]; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
392 |
(* |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
393 |
the following would be slightly more general, |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
394 |
but cannot be used as rewrite rule: |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
395 |
### Cannot add premise as rewrite rule because it contains (type) unknowns: |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
396 |
### ?y = .x |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
397 |
Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
398 |
by (rtac some_equality 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
399 |
by ( Simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
400 |
by (split_all_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
401 |
by (Asm_full_simp_tac 1); |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11339
diff
changeset
|
402 |
qed "The_split_eq"; |
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
403 |
*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
404 |
|
11339 | 405 |
Goal "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y"; |
406 |
by Auto_tac; |
|
407 |
qed "injective_fst_snd"; |
|
408 |
||
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
409 |
(*** prod_fun -- action of the product functor upon functions ***) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
410 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
411 |
Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
412 |
by (rtac split_conv 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
413 |
qed "prod_fun"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
414 |
Addsimps [prod_fun]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
415 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
416 |
Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
417 |
by (rtac ext 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
418 |
by (pair_tac "x" 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
419 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
420 |
qed "prod_fun_compose"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
421 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
422 |
Goal "prod_fun (%x. x) (%y. y) = (%z. z)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
423 |
by (rtac ext 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
424 |
by (pair_tac "z" 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
425 |
by (Asm_simp_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
426 |
qed "prod_fun_ident"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
427 |
Addsimps [prod_fun_ident]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
428 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
429 |
Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
430 |
by (rtac image_eqI 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
431 |
by (rtac (prod_fun RS sym) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
432 |
by (assume_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
433 |
qed "prod_fun_imageI"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
434 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
435 |
val major::prems = Goal |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
436 |
"[| c: (prod_fun f g)`r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
437 |
\ |] ==> P"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
438 |
by (rtac (major RS imageE) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
439 |
by (res_inst_tac [("p","x")] PairE 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
440 |
by (resolve_tac prems 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
441 |
by (Blast_tac 2); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
442 |
by (blast_tac (claset() addIs [prod_fun]) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
443 |
qed "prod_fun_imageE"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
444 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
445 |
AddIs [prod_fun_imageI]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
446 |
AddSEs [prod_fun_imageE]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
447 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
448 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
449 |
(*** Disjoint union of a family of sets - Sigma ***) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
450 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
451 |
Goalw [Sigma_def] "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
452 |
by (REPEAT (ares_tac [singletonI,UN_I] 1)); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
453 |
qed "SigmaI"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
454 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
455 |
AddSIs [SigmaI]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
456 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
457 |
(*The general elimination rule*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
458 |
val major::prems = Goalw [Sigma_def] |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
459 |
"[| c: Sigma A B; \ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
460 |
\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
461 |
\ |] ==> P"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
462 |
by (cut_facts_tac [major] 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
463 |
by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
464 |
qed "SigmaE"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
465 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
466 |
(** Elimination of (a,b):A*B -- introduces no eigenvariables **) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
467 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
468 |
Goal "(a,b) : Sigma A B ==> a : A"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
469 |
by (etac SigmaE 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
470 |
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
471 |
qed "SigmaD1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
472 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
473 |
Goal "(a,b) : Sigma A B ==> b : B(a)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
474 |
by (etac SigmaE 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
475 |
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
476 |
qed "SigmaD2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
477 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
478 |
val [major,minor]= Goal |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
479 |
"[| (a,b) : Sigma A B; \ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
480 |
\ [| a:A; b:B(a) |] ==> P \ |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
481 |
\ |] ==> P"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
482 |
by (rtac minor 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
483 |
by (rtac (major RS SigmaD1) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
484 |
by (rtac (major RS SigmaD2) 1) ; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
485 |
qed "SigmaE2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
486 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
487 |
AddSEs [SigmaE2, SigmaE]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
488 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
489 |
val prems = Goal |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
490 |
"[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
491 |
by (cut_facts_tac prems 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
492 |
by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
493 |
qed "Sigma_mono"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
494 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
495 |
Goal "Sigma {} B = {}"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
496 |
by (Blast_tac 1) ; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
497 |
qed "Sigma_empty1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
498 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
499 |
Goal "A <*> {} = {}"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
500 |
by (Blast_tac 1) ; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
501 |
qed "Sigma_empty2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
502 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
503 |
Addsimps [Sigma_empty1,Sigma_empty2]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
504 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
505 |
Goal "UNIV <*> UNIV = UNIV"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
506 |
by Auto_tac; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
507 |
qed "UNIV_Times_UNIV"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
508 |
Addsimps [UNIV_Times_UNIV]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
509 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
510 |
Goal "- (UNIV <*> A) = UNIV <*> (-A)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
511 |
by Auto_tac; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
512 |
qed "Compl_Times_UNIV1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
513 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
514 |
Goal "- (A <*> UNIV) = (-A) <*> UNIV"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
515 |
by Auto_tac; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
516 |
qed "Compl_Times_UNIV2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
517 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
518 |
Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
519 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
520 |
Goal "((a,b): Sigma A B) = (a:A & b:B(a))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
521 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
522 |
qed "mem_Sigma_iff"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
523 |
AddIffs [mem_Sigma_iff]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
524 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
525 |
Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
526 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
527 |
qed "Times_subset_cancel2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
528 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
529 |
Goal "x:C ==> (A <*> C = B <*> C) = (A = B)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
530 |
by (blast_tac (claset() addEs [equalityE]) 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
531 |
qed "Times_eq_cancel2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
532 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
533 |
Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
534 |
by (Fast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
535 |
qed "SetCompr_Sigma_eq"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
536 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
537 |
(*** Complex rules for Sigma ***) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
538 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
539 |
Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
540 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
541 |
qed "Collect_split"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
542 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
543 |
Addsimps [Collect_split]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
544 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
545 |
(*Suggested by Pierre Chartier*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
546 |
Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
547 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
548 |
qed "UN_Times_distrib"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
549 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
550 |
Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
551 |
by (Fast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
552 |
qed "split_paired_Ball_Sigma"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
553 |
Addsimps [split_paired_Ball_Sigma]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
554 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
555 |
Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
556 |
by (Fast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
557 |
qed "split_paired_Bex_Sigma"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
558 |
Addsimps [split_paired_Bex_Sigma]; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
559 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
560 |
Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
561 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
562 |
qed "Sigma_Un_distrib1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
563 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
564 |
Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
565 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
566 |
qed "Sigma_Un_distrib2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
567 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
568 |
Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
569 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
570 |
qed "Sigma_Int_distrib1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
571 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
572 |
Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
573 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
574 |
qed "Sigma_Int_distrib2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
575 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
576 |
Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
577 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
578 |
qed "Sigma_Diff_distrib1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
579 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
580 |
Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
581 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
582 |
qed "Sigma_Diff_distrib2"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
583 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
584 |
Goal "Sigma (Union X) B = (UN A:X. Sigma A B)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
585 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
586 |
qed "Sigma_Union"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
587 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
588 |
(*Non-dependent versions are needed to avoid the need for higher-order |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
589 |
matching, especially when the rules are re-oriented*) |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
590 |
Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
591 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
592 |
qed "Times_Un_distrib1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
593 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
594 |
Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
595 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
596 |
qed "Times_Int_distrib1"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
597 |
|
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
598 |
Goal "(A - B) <*> C = (A <*> C) - (B <*> C)"; |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
599 |
by (Blast_tac 1); |
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
diff
changeset
|
600 |
qed "Times_Diff_distrib1"; |