src/Provers/split_paired_all.ML
author paulson
Mon, 18 Oct 1999 15:20:21 +0200
changeset 7879 4547f0bd9454
parent 5704 1ddf7e1e8b19
child 9039 20ff649a0fd1
permissions -rw-r--r--
fixed comments
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    32
    val surj_pair = Drule.unvarify (standard raw_surj_pair);
5680
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
    val P = Free (variant used "P", pT --> propT);
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    38
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    39
   (*"!!a b. PROP (a, b)"*)
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    40
   val all_a_b = all "a" aT (all "b" bT (P $ (con $ Bound 1 $ Bound 0)));
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    41
   (*"!!x. PROP P x"*)
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    42
   val all_x = all "x" pT (P $ Bound 0);
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    43
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    44
   (*lemma "P p == P (fst p, snd p)"*)
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    45
   val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    46
7879
4547f0bd9454 fixed comments
paulson
parents: 5704
diff changeset
    47
   (*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*)
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    48
   val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    49
     (fn prems => [resolve_tac prems 1]);
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    50
7879
4547f0bd9454 fixed comments
paulson
parents: 5704
diff changeset
    51
   (*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*)
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    52
   val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x))
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    53
     (fn prems => [rtac lem2 1, resolve_tac prems 1]);
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    54
7879
4547f0bd9454 fixed comments
paulson
parents: 5704
diff changeset
    55
   (*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*)
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    56
   val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b))
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    57
     (fn prems => [resolve_tac prems 1]);
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    58
  in standard (Thm.equal_intr lem4 lem3) end;
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
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    61
end;