author | wenzelm |
Tue, 20 Oct 1998 16:36:21 +0200 | |
changeset 5695 | 898429dbb162 |
parent 5680 | 4f526bcd3a68 |
child 5704 | 1ddf7e1e8b19 |
permissions | -rw-r--r-- |
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Provers/split_paired_all.ML |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
4 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
5 |
Derived rule for turning meta-level surjective pairing into split rule: |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
6 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
7 |
p == (fst p, snd p) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
8 |
-------------------------------------- |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
9 |
!!a b. PROP (a, b) == !! x. PROP P x |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
10 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
11 |
*) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
12 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
13 |
signature SPLIT_PAIRED_ALL = |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
14 |
sig |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
15 |
val rule: thm -> thm |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
16 |
end; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
17 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
18 |
structure SplitPairedAll: SPLIT_PAIRED_ALL = |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
19 |
struct |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
20 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
21 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
22 |
fun all x T t = Term.all T $ Abs (x, T, t); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
23 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
24 |
infixr ==>; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
25 |
val op ==> = Logic.mk_implies; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
26 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
27 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
28 |
fun rule raw_surj_pair = |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
29 |
let |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
30 |
val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
31 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
32 |
val surj_pair = Drule.unvarify raw_surj_pair; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
33 |
val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
34 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
35 |
val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair)); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
36 |
val pT as Type (_, [aT, bT]) = fastype_of p; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
37 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
38 |
val P = Free (variant used "P", pT --> propT); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
39 |
val x_name = variant used "x"; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
40 |
val x = Free (x_name, pT); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
41 |
val a = variant used "a"; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
42 |
val b = variant used "b"; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
43 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
44 |
(*"P x == P (fst x, snd x)"*) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
45 |
val lem1 = |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
46 |
Thm.combination (Thm.reflexive (ct P)) surj_pair |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
47 |
|> Thm.forall_intr (ct p) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
48 |
|> Thm.forall_elim (ct x); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
49 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
50 |
(*"!!a b. PROP (a, b) ==> PROP P x"*) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
51 |
val lem2 = prove_goalw_cterm [lem1] |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
52 |
(ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> P $ x)) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
53 |
(fn prems => [resolve_tac prems 1]); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
54 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
55 |
(*"!!a b. PROP (a, b) ==> !! x. PROP P x"*) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
56 |
val lem3 = prove_goalw_cterm [] |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
57 |
(ct (all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))) ==> all x_name pT (P $ Bound 0))) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
58 |
(fn prems => [rtac lem2 1, resolve_tac prems 1]); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
59 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
60 |
(*"!! x. PROP P x ==> !!a b. PROP (a, b)"*) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
61 |
val lem4 = prove_goalw_cterm [] |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
62 |
(ct (all x_name pT (P $ Bound 0) ==> all a aT (all a bT (P $ (con $ Bound 1 $ Bound 0))))) |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
63 |
(fn prems => [resolve_tac prems 1]); |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
64 |
in standard (Thm.equal_intr lem4 lem3) end; |
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
65 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
66 |
|
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff
changeset
|
67 |
end; |