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