author | wenzelm |
Sat, 30 Oct 1999 20:20:48 +0200 | |
changeset 7982 | d534b897ce39 |
parent 7958 | f531589c9fc1 |
child 8100 | 6186ee807f2e |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/prod |
923 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
923 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
5810 | 6 |
Ordered Pairs, the Cartesian product type, the unit type |
923 | 7 |
*) |
8 |
||
9 |
(*This counts as a non-emptiness result for admitting 'a * 'b as a type*) |
|
5069 | 10 |
Goalw [Prod_def] "Pair_Rep a b : Prod"; |
923 | 11 |
by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); |
12 |
qed "ProdI"; |
|
13 |
||
14 |
val [major] = goalw Prod.thy [Pair_Rep_def] |
|
15 |
"Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; |
|
16 |
by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), |
|
1465 | 17 |
rtac conjI, rtac refl, rtac refl]); |
923 | 18 |
qed "Pair_Rep_inject"; |
19 |
||
5069 | 20 |
Goal "inj_on Abs_Prod Prod"; |
4830 | 21 |
by (rtac inj_on_inverseI 1); |
923 | 22 |
by (etac Abs_Prod_inverse 1); |
4830 | 23 |
qed "inj_on_Abs_Prod"; |
923 | 24 |
|
5316 | 25 |
val prems = Goalw [Pair_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
26 |
"[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; |
4830 | 27 |
by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1); |
923 | 28 |
by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
29 |
qed "Pair_inject"; |
|
30 |
||
5069 | 31 |
Goal "((a,b) = (a',b')) = (a=a' & b=b')"; |
4089 | 32 |
by (blast_tac (claset() addSEs [Pair_inject]) 1); |
923 | 33 |
qed "Pair_eq"; |
3429 | 34 |
AddIffs [Pair_eq]; |
923 | 35 |
|
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
36 |
Goalw [fst_def] "fst (a,b) = a"; |
4534 | 37 |
by (Blast_tac 1); |
923 | 38 |
qed "fst_conv"; |
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
39 |
Goalw [snd_def] "snd (a,b) = b"; |
4534 | 40 |
by (Blast_tac 1); |
923 | 41 |
qed "snd_conv"; |
4534 | 42 |
Addsimps [fst_conv, snd_conv]; |
923 | 43 |
|
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
44 |
Goal "fst (x, y) = a ==> x = a"; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
45 |
by (Asm_full_simp_tac 1); |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
46 |
qed "fst_eqD"; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
47 |
Goal "snd (x, y) = a ==> y = a"; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
48 |
by (Asm_full_simp_tac 1); |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
49 |
qed "snd_eqD"; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
50 |
|
5069 | 51 |
Goalw [Pair_def] "? x y. p = (x,y)"; |
923 | 52 |
by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); |
53 |
by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, |
|
1465 | 54 |
rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); |
923 | 55 |
qed "PairE_lemma"; |
56 |
||
5316 | 57 |
val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q"; |
923 | 58 |
by (rtac (PairE_lemma RS exE) 1); |
59 |
by (REPEAT (eresolve_tac [prem,exE] 1)); |
|
60 |
qed "PairE"; |
|
61 |
||
4819
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
62 |
fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac, |
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
63 |
K prune_params_tac]; |
4134 | 64 |
|
4828 | 65 |
(* Do not add as rewrite rule: invalidates some proofs in IMP *) |
5069 | 66 |
Goal "p = (fst(p),snd(p))"; |
4828 | 67 |
by (pair_tac "p" 1); |
68 |
by (Asm_simp_tac 1); |
|
69 |
qed "surjective_pairing"; |
|
70 |
||
7031 | 71 |
Goal "? x y. z = (x, y)"; |
72 |
by (rtac exI 1); |
|
73 |
by (rtac exI 1); |
|
74 |
by (rtac surjective_pairing 1); |
|
75 |
qed "surj_pair"; |
|
4828 | 76 |
Addsimps [surj_pair]; |
77 |
||
78 |
||
5699 | 79 |
bind_thm ("split_paired_all", |
80 |
SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection))); |
|
4828 | 81 |
(* |
82 |
Addsimps [split_paired_all] does not work with simplifier |
|
83 |
because it also affects premises in congrence rules, |
|
84 |
where is can lead to premises of the form !!a b. ... = ?P(a,b) |
|
85 |
which cannot be solved by reflexivity. |
|
86 |
*) |
|
87 |
||
1301 | 88 |
(* replace parameters of product type by individual component parameters *) |
89 |
local |
|
4819
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
90 |
fun is_pair (_,Type("*",_)) = true |
ef2e8e2a10e1
improved pair_tac to call prune_params_tac afterwards
oheimb
parents:
4799
diff
changeset
|
91 |
| is_pair _ = false; |
4828 | 92 |
fun exists_paired_all prem = exists is_pair (Logic.strip_params prem); |
93 |
val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]); |
|
1301 | 94 |
in |
4828 | 95 |
val split_all_tac = SUBGOAL (fn (prem,i) => |
96 |
if exists_paired_all prem then split_tac i else no_tac); |
|
1301 | 97 |
end; |
98 |
||
4828 | 99 |
claset_ref() := claset() addSWrapper ("split_all_tac", |
100 |
fn tac2 => split_all_tac ORELSE' tac2); |
|
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
101 |
|
5069 | 102 |
Goal "(!x. P x) = (!a b. P(a,b))"; |
4650 | 103 |
by (Fast_tac 1); |
1301 | 104 |
qed "split_paired_All"; |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
105 |
Addsimps [split_paired_All]; |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
106 |
(* AddIffs is not a good idea because it makes Blast_tac loop *) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
107 |
|
5715
5fc697ad232b
Added theorem prod_induct (needed for rep_datatype).
berghofe
parents:
5699
diff
changeset
|
108 |
bind_thm ("prod_induct", |
5fc697ad232b
Added theorem prod_induct (needed for rep_datatype).
berghofe
parents:
5699
diff
changeset
|
109 |
allI RS (allI RS (split_paired_All RS iffD2)) RS spec); |
5fc697ad232b
Added theorem prod_induct (needed for rep_datatype).
berghofe
parents:
5699
diff
changeset
|
110 |
|
5069 | 111 |
Goal "(? x. P x) = (? a b. P(a,b))"; |
4650 | 112 |
by (Fast_tac 1); |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
113 |
qed "split_paired_Ex"; |
4534 | 114 |
Addsimps [split_paired_Ex]; |
1301 | 115 |
|
5069 | 116 |
Goalw [split_def] "split c (a,b) = c a b"; |
4534 | 117 |
by (Simp_tac 1); |
923 | 118 |
qed "split"; |
4534 | 119 |
Addsimps [split]; |
923 | 120 |
|
7339 | 121 |
(*Subsumes the old split_Pair when f is the identity function*) |
122 |
Goal "split (%x y. f(x,y)) = f"; |
|
123 |
by (rtac ext 1); |
|
124 |
by (pair_tac "x" 1); |
|
4828 | 125 |
by (Simp_tac 1); |
7339 | 126 |
qed "split_Pair_apply"; |
127 |
||
128 |
(*Can't be added to simpset: loops!*) |
|
129 |
Goal "(SOME x. P x) = (SOME (a,b). P(a,b))"; |
|
130 |
by (simp_tac (simpset() addsimps [split_Pair_apply]) 1); |
|
131 |
qed "split_paired_Eps"; |
|
4828 | 132 |
|
5069 | 133 |
Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; |
4828 | 134 |
by (split_all_tac 1); |
1264 | 135 |
by (Asm_simp_tac 1); |
923 | 136 |
qed "Pair_fst_snd_eq"; |
137 |
||
138 |
(*Prevents simplification of c: much faster*) |
|
7031 | 139 |
val [prem] = goal Prod.thy |
140 |
"p=q ==> split c p = split c q"; |
|
141 |
by (rtac (prem RS arg_cong) 1); |
|
142 |
qed "split_weak_cong"; |
|
923 | 143 |
|
7031 | 144 |
Goal "(%(x,y). f(x,y)) = f"; |
145 |
by (rtac ext 1); |
|
146 |
by (split_all_tac 1); |
|
147 |
by (rtac split 1); |
|
148 |
qed "split_eta"; |
|
1655 | 149 |
|
7031 | 150 |
val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g"; |
151 |
by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1); |
|
152 |
qed "cond_split_eta"; |
|
5294 | 153 |
|
154 |
(*simplification procedure for cond_split_eta. |
|
155 |
using split_eta a rewrite rule is not general enough, and using |
|
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
156 |
cond_split_eta directly would render some existing proofs very inefficient. |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
157 |
similarly for split_beta. *) |
5294 | 158 |
local |
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
159 |
fun Pair_pat k 0 (Bound m) = (m = k) |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
160 |
| Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
161 |
m = k+i andalso Pair_pat k (i-1) t |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
162 |
| Pair_pat _ _ _ = false; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
163 |
fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
164 |
| no_args k i (t $ u) = no_args k i t andalso no_args k i u |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
165 |
| no_args k i (Bound m) = m < k orelse m > k+i |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
166 |
| no_args _ _ _ = true; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
167 |
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
168 |
| split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
169 |
| split_pat tp i _ = None; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
170 |
fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
171 |
(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))) |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
172 |
(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1])); |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
173 |
fun simproc name patstr = Simplifier.mk_simproc name |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
174 |
[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termTVar)]; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
175 |
|
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
176 |
val beta_patstr = "split f z"; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
177 |
val eta_patstr = "split f"; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
178 |
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
179 |
| beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
180 |
(beta_term_pat k i t andalso beta_term_pat k i u) |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
181 |
| beta_term_pat k i t = no_args k i t; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
182 |
fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
183 |
| eta_term_pat _ _ _ = false; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
184 |
fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
185 |
| subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
186 |
else (subst arg k i t $ subst arg k i u) |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
187 |
| subst arg k i t = t; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
188 |
fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
189 |
(case split_pat beta_term_pat 1 t of |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
190 |
Some (i,f) => Some (metaeq sg s (subst arg 0 i f)) |
5294 | 191 |
| None => None) |
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
192 |
| beta_proc _ _ _ = None; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
193 |
fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
194 |
(case split_pat eta_term_pat 1 t of |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
195 |
Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end)) |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
196 |
| None => None) |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
197 |
| eta_proc _ _ _ = None; |
5294 | 198 |
in |
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
199 |
val split_beta_proc = simproc "split_beta" beta_patstr beta_proc; |
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
200 |
val split_eta_proc = simproc "split_eta" eta_patstr eta_proc; |
5294 | 201 |
end; |
202 |
||
7495
affcfd2830b7
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
oheimb
parents:
7339
diff
changeset
|
203 |
Addsimprocs [split_beta_proc,split_eta_proc]; |
5294 | 204 |
|
7031 | 205 |
Goal "(%(x,y). P x y) z = P (fst z) (snd z)"; |
206 |
by (stac surjective_pairing 1 THEN rtac split 1); |
|
207 |
qed "split_beta"; |
|
4134 | 208 |
|
923 | 209 |
(*For use with split_tac and the simplifier*) |
5069 | 210 |
Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))"; |
923 | 211 |
by (stac surjective_pairing 1); |
212 |
by (stac split 1); |
|
2935 | 213 |
by (Blast_tac 1); |
4830 | 214 |
qed "split_split"; |
923 | 215 |
|
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
216 |
(* could be done after split_tac has been speeded up significantly: |
4830 | 217 |
simpset_ref() := simpset() addsplits [split_split]; |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
218 |
precompute the constants involved and don't do anything unless |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
219 |
the current goal contains one of those constants |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
220 |
*) |
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
221 |
|
5069 | 222 |
Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; |
4830 | 223 |
by (stac split_split 1); |
4435 | 224 |
by (Simp_tac 1); |
225 |
qed "expand_split_asm"; |
|
226 |
||
923 | 227 |
(** split used as a logical connective or set former **) |
228 |
||
2935 | 229 |
(*These rules are for use with blast_tac. |
923 | 230 |
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*) |
231 |
||
5069 | 232 |
Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p"; |
1552 | 233 |
by (split_all_tac 1); |
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
234 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
235 |
qed "splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
236 |
|
7958 | 237 |
Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x"; |
238 |
by (split_all_tac 1); |
|
239 |
by (Asm_simp_tac 1); |
|
240 |
qed "splitI2'"; |
|
241 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
242 |
Goal "c a b ==> split c (a,b)"; |
1264 | 243 |
by (Asm_simp_tac 1); |
923 | 244 |
qed "splitI"; |
245 |
||
5316 | 246 |
val prems = Goalw [split_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
247 |
"[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q"; |
923 | 248 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
249 |
qed "splitE"; |
|
250 |
||
7031 | 251 |
val major::prems = goal Prod.thy |
252 |
"[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R \ |
|
253 |
\ |] ==> R"; |
|
254 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
|
255 |
by (rtac (split_beta RS subst) 1 THEN rtac major 1); |
|
256 |
qed "splitE2"; |
|
4134 | 257 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
258 |
Goal "split R (a,b) ==> R a b"; |
923 | 259 |
by (etac (split RS iffD1) 1); |
260 |
qed "splitD"; |
|
261 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
262 |
Goal "z: c a b ==> z: split c (a,b)"; |
1264 | 263 |
by (Asm_simp_tac 1); |
923 | 264 |
qed "mem_splitI"; |
265 |
||
5069 | 266 |
Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p"; |
1552 | 267 |
by (split_all_tac 1); |
1454
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
268 |
by (Asm_simp_tac 1); |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
269 |
qed "mem_splitI2"; |
d0266c81a85e
Streamlined defs in Relation and added new intro/elim rules to do with
nipkow
parents:
1301
diff
changeset
|
270 |
|
5316 | 271 |
val prems = Goalw [split_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
272 |
"[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q"; |
923 | 273 |
by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
274 |
qed "mem_splitE"; |
|
275 |
||
7958 | 276 |
AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2]; |
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
277 |
AddSEs [splitE, mem_splitE]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
278 |
|
4534 | 279 |
(* allows simplifications of nested splits in case of independent predicates *) |
5069 | 280 |
Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"; |
4534 | 281 |
by (rtac ext 1); |
282 |
by (Blast_tac 1); |
|
283 |
qed "split_part"; |
|
284 |
Addsimps [split_part]; |
|
285 |
||
5069 | 286 |
Goal "(@(x',y'). x = x' & y = y') = (x,y)"; |
4534 | 287 |
by (Blast_tac 1); |
288 |
qed "Eps_split_eq"; |
|
289 |
Addsimps [Eps_split_eq]; |
|
290 |
(* |
|
291 |
the following would be slightly more general, |
|
292 |
but cannot be used as rewrite rule: |
|
293 |
### Cannot add premise as rewrite rule because it contains (type) unknowns: |
|
294 |
### ?y = .x |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
295 |
Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)"; |
4534 | 296 |
by (rtac select_equality 1); |
297 |
by ( Simp_tac 1); |
|
298 |
by (split_all_tac 1); |
|
299 |
by (Asm_full_simp_tac 1); |
|
300 |
qed "Eps_split_eq"; |
|
301 |
*) |
|
302 |
||
923 | 303 |
(*** prod_fun -- action of the product functor upon functions ***) |
304 |
||
5069 | 305 |
Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))"; |
923 | 306 |
by (rtac split 1); |
307 |
qed "prod_fun"; |
|
4521 | 308 |
Addsimps [prod_fun]; |
923 | 309 |
|
5278 | 310 |
Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; |
923 | 311 |
by (rtac ext 1); |
4828 | 312 |
by (pair_tac "x" 1); |
4521 | 313 |
by (Asm_simp_tac 1); |
923 | 314 |
qed "prod_fun_compose"; |
315 |
||
5069 | 316 |
Goal "prod_fun (%x. x) (%y. y) = (%z. z)"; |
923 | 317 |
by (rtac ext 1); |
4828 | 318 |
by (pair_tac "z" 1); |
4521 | 319 |
by (Asm_simp_tac 1); |
923 | 320 |
qed "prod_fun_ident"; |
4521 | 321 |
Addsimps [prod_fun_ident]; |
923 | 322 |
|
5316 | 323 |
Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r"; |
923 | 324 |
by (rtac image_eqI 1); |
325 |
by (rtac (prod_fun RS sym) 1); |
|
5316 | 326 |
by (assume_tac 1); |
923 | 327 |
qed "prod_fun_imageI"; |
328 |
||
5316 | 329 |
val major::prems = Goal |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
330 |
"[| c: (prod_fun f g)``r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \ |
923 | 331 |
\ |] ==> P"; |
332 |
by (rtac (major RS imageE) 1); |
|
333 |
by (res_inst_tac [("p","x")] PairE 1); |
|
334 |
by (resolve_tac prems 1); |
|
2935 | 335 |
by (Blast_tac 2); |
4089 | 336 |
by (blast_tac (claset() addIs [prod_fun]) 1); |
923 | 337 |
qed "prod_fun_imageE"; |
338 |
||
5788 | 339 |
AddIs [prod_fun_imageI]; |
340 |
AddSEs [prod_fun_imageE]; |
|
341 |
||
4521 | 342 |
|
923 | 343 |
(*** Disjoint union of a family of sets - Sigma ***) |
344 |
||
7031 | 345 |
Goalw [Sigma_def] "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B"; |
346 |
by (REPEAT (ares_tac [singletonI,UN_I] 1)); |
|
347 |
qed "SigmaI"; |
|
923 | 348 |
|
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
349 |
AddSIs [SigmaI]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
350 |
|
923 | 351 |
(*The general elimination rule*) |
7031 | 352 |
val major::prems = Goalw [Sigma_def] |
923 | 353 |
"[| c: Sigma A B; \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
354 |
\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \ |
7031 | 355 |
\ |] ==> P"; |
356 |
by (cut_facts_tac [major] 1); |
|
357 |
by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ; |
|
358 |
qed "SigmaE"; |
|
923 | 359 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
360 |
(** Elimination of (a,b):A*B -- introduces no eigenvariables **) |
7007 | 361 |
|
362 |
Goal "(a,b) : Sigma A B ==> a : A"; |
|
363 |
by (etac SigmaE 1); |
|
364 |
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; |
|
365 |
qed "SigmaD1"; |
|
923 | 366 |
|
7007 | 367 |
Goal "(a,b) : Sigma A B ==> b : B(a)"; |
368 |
by (etac SigmaE 1); |
|
369 |
by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ; |
|
370 |
qed "SigmaD2"; |
|
923 | 371 |
|
7007 | 372 |
val [major,minor]= goal Prod.thy |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
373 |
"[| (a,b) : Sigma A B; \ |
923 | 374 |
\ [| a:A; b:B(a) |] ==> P \ |
7007 | 375 |
\ |] ==> P"; |
376 |
by (rtac minor 1); |
|
377 |
by (rtac (major RS SigmaD1) 1); |
|
378 |
by (rtac (major RS SigmaD2) 1) ; |
|
379 |
qed "SigmaE2"; |
|
923 | 380 |
|
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
381 |
AddSEs [SigmaE2, SigmaE]; |
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
382 |
|
5316 | 383 |
val prems = Goal |
1642 | 384 |
"[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"; |
1515 | 385 |
by (cut_facts_tac prems 1); |
4089 | 386 |
by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
1515 | 387 |
qed "Sigma_mono"; |
388 |
||
7007 | 389 |
Goal "Sigma {} B = {}"; |
390 |
by (Blast_tac 1) ; |
|
391 |
qed "Sigma_empty1"; |
|
1618 | 392 |
|
7007 | 393 |
Goal "A Times {} = {}"; |
394 |
by (Blast_tac 1) ; |
|
395 |
qed "Sigma_empty2"; |
|
1618 | 396 |
|
397 |
Addsimps [Sigma_empty1,Sigma_empty2]; |
|
398 |
||
5069 | 399 |
Goal "((a,b): Sigma A B) = (a:A & b:B(a))"; |
2935 | 400 |
by (Blast_tac 1); |
1618 | 401 |
qed "mem_Sigma_iff"; |
3568
36ff1ab12021
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
nipkow
parents:
3429
diff
changeset
|
402 |
AddIffs [mem_Sigma_iff]; |
1618 | 403 |
|
6016 | 404 |
Goal "x:C ==> (A Times C <= B Times C) = (A <= B)"; |
405 |
by (Blast_tac 1); |
|
406 |
qed "Times_subset_cancel2"; |
|
407 |
||
408 |
Goal "x:C ==> (A Times C = B Times C) = (A = B)"; |
|
409 |
by (blast_tac (claset() addEs [equalityE]) 1); |
|
410 |
qed "Times_eq_cancel2"; |
|
411 |
||
5810 | 412 |
|
413 |
(*** Complex rules for Sigma ***) |
|
414 |
||
7031 | 415 |
Goal "{(a,b). P a & Q b} = Collect P Times Collect Q"; |
416 |
by (Blast_tac 1); |
|
417 |
qed "Collect_split"; |
|
418 |
||
4534 | 419 |
Addsimps [Collect_split]; |
1515 | 420 |
|
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
421 |
(*Suggested by Pierre Chartier*) |
5278 | 422 |
Goal "(UN (a,b):(A Times B). E a Times F b) = (UNION A E) Times (UNION B F)"; |
2935 | 423 |
by (Blast_tac 1); |
6830
f8aed3706af7
renamed UNION_... to UN_... (to fit the convention)
paulson
parents:
6394
diff
changeset
|
424 |
qed "UN_Times_distrib"; |
2856
cdb908486a96
Reorganization of how classical rules are installed
paulson
parents:
2637
diff
changeset
|
425 |
|
6016 | 426 |
Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"; |
5810 | 427 |
by (Fast_tac 1); |
6016 | 428 |
qed "split_paired_Ball_Sigma"; |
429 |
Addsimps [split_paired_Ball_Sigma]; |
|
5810 | 430 |
|
6016 | 431 |
Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"; |
5810 | 432 |
by (Fast_tac 1); |
6016 | 433 |
qed "split_paired_Bex_Sigma"; |
434 |
Addsimps [split_paired_Bex_Sigma]; |
|
5810 | 435 |
|
436 |
Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))"; |
|
437 |
by (Blast_tac 1); |
|
438 |
qed "Sigma_Un_distrib1"; |
|
439 |
||
440 |
Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))"; |
|
441 |
by (Blast_tac 1); |
|
442 |
qed "Sigma_Un_distrib2"; |
|
443 |
||
444 |
Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))"; |
|
445 |
by (Blast_tac 1); |
|
446 |
qed "Sigma_Int_distrib1"; |
|
447 |
||
448 |
Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))"; |
|
449 |
by (Blast_tac 1); |
|
450 |
qed "Sigma_Int_distrib2"; |
|
451 |
||
452 |
Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))"; |
|
453 |
by (Blast_tac 1); |
|
454 |
qed "Sigma_Diff_distrib1"; |
|
455 |
||
456 |
Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))"; |
|
457 |
by (Blast_tac 1); |
|
458 |
qed "Sigma_Diff_distrib2"; |
|
459 |
||
6016 | 460 |
Goal "Sigma (Union X) B = (UN A:X. Sigma A B)"; |
461 |
by (Blast_tac 1); |
|
462 |
qed "Sigma_Union"; |
|
463 |
||
5810 | 464 |
|
923 | 465 |
(** Exhaustion rule for unit -- a degenerate form of induction **) |
466 |
||
5069 | 467 |
Goalw [Unity_def] |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset
|
468 |
"u = ()"; |
2886 | 469 |
by (stac (rewrite_rule [unit_def] Rep_unit RS singletonD RS sym) 1); |
2880 | 470 |
by (rtac (Rep_unit_inverse RS sym) 1); |
923 | 471 |
qed "unit_eq"; |
1754
852093aeb0ab
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1746
diff
changeset
|
472 |
|
5088
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
473 |
(*simplification procedure for unit_eq. |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
474 |
Cannot use this rule directly -- it loops!*) |
5083 | 475 |
local |
6394 | 476 |
val unit_pat = Thm.cterm_of (Theory.sign_of thy) (Free ("x", HOLogic.unitT)); |
5553 | 477 |
val unit_meta_eq = standard (mk_meta_eq unit_eq); |
5083 | 478 |
fun proc _ _ t = |
479 |
if HOLogic.is_unit t then None |
|
480 |
else Some unit_meta_eq; |
|
481 |
in |
|
482 |
val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc; |
|
483 |
end; |
|
484 |
||
485 |
Addsimprocs [unit_eq_proc]; |
|
486 |
||
487 |
||
5761 | 488 |
Goal "P () ==> P x"; |
489 |
by (Simp_tac 1); |
|
490 |
qed "unit_induct"; |
|
491 |
||
492 |
||
5088
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
493 |
(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
494 |
replacing it by f rather than by %u.f(). *) |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
495 |
Goal "(%u::unit. f()) = f"; |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
496 |
by (rtac ext 1); |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
497 |
by (Simp_tac 1); |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
498 |
qed "unit_abs_eta_conv"; |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
499 |
Addsimps [unit_abs_eta_conv]; |
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
500 |
|
e4aa78d1312f
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
paulson
parents:
5083
diff
changeset
|
501 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
502 |
(*Attempts to remove occurrences of split, and pair-valued parameters*) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
503 |
val remove_split = rewrite_rule [split RS eq_reflection] o |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
504 |
rule_by_tactic (TRYALL split_all_tac); |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
505 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
506 |
local |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
507 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
508 |
(*In ap_split S T u, term u expects separate arguments for the factors of S, |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
509 |
with result type T. The call creates a new term expecting one argument |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
510 |
of type S.*) |
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
511 |
fun ap_split (Type ("*", [T1, T2])) T3 u = |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
512 |
HOLogic.split_const (T1, T2, T3) $ |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
513 |
Abs("v", T1, |
2031 | 514 |
ap_split T2 T3 |
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
515 |
((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ |
2031 | 516 |
Bound 0)) |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
517 |
| ap_split T T3 u = u; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
518 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
519 |
(*Curries any Var of function type in the rule*) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
520 |
fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) = |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
521 |
let val T' = HOLogic.prodT_factors T1 ---> T2 |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
522 |
val newt = ap_split T1 T2 (Var (v, T')) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
523 |
val cterm = Thm.cterm_of (#sign (rep_thm rl)) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
524 |
in |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
525 |
instantiate ([], [(cterm t, cterm newt)]) rl |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
526 |
end |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
527 |
| split_rule_var' (t, rl) = rl; |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
528 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
529 |
in |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
530 |
|
5096
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
531 |
val split_rule_var = standard o remove_split o split_rule_var'; |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
532 |
|
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
533 |
(*Curries ALL function variables occurring in a rule's conclusion*) |
84b00be693b4
Moved most of the Prod_Syntax - stuff to HOLogic.
berghofe
parents:
5088
diff
changeset
|
534 |
fun split_rule rl = remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)) |
1746
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
535 |
|> standard; |
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
536 |
|
f0c6aabc6c02
Moved split_rule et al from ind_syntax.ML to Prod.ML.
nipkow
parents:
1727
diff
changeset
|
537 |
end; |
5810 | 538 |
|
539 |