src/Provers/split_paired_all.ML
author wenzelm
Tue, 06 Jun 2000 20:31:43 +0200
changeset 9039 20ff649a0fd1
parent 7879 4547f0bd9454
permissions -rw-r--r--
added rule_params;
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
9039
20ff649a0fd1 added rule_params;
wenzelm
parents: 7879
diff changeset
    15
  val rule_params: string -> string -> thm -> thm
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    16
  val rule: thm -> thm
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    17
end;
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    18
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    19
structure SplitPairedAll: SPLIT_PAIRED_ALL =
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    20
struct
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
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    23
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
    24
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    25
infixr ==>;
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    26
val op ==> = Logic.mk_implies;
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
9039
20ff649a0fd1 added rule_params;
wenzelm
parents: 7879
diff changeset
    29
fun rule_params a b raw_surj_pair =
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    30
  let
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    31
    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
    32
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    33
    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
    34
    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
    35
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    36
    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
    37
    val pT as Type (_, [aT, bT]) = fastype_of p;
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
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    40
   (*"!!a b. PROP (a, b)"*)
9039
20ff649a0fd1 added rule_params;
wenzelm
parents: 7879
diff changeset
    41
   val all_a_b = all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0)));
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    42
   (*"!!x. PROP P x"*)
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    43
   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
    44
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    45
   (*lemma "P p == P (fst p, snd p)"*)
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    46
   val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    47
7879
4547f0bd9454 fixed comments
paulson
parents: 5704
diff changeset
    48
   (*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*)
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    49
   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
    50
     (fn prems => [resolve_tac prems 1]);
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    51
7879
4547f0bd9454 fixed comments
paulson
parents: 5704
diff changeset
    52
   (*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*)
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    53
   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
    54
     (fn prems => [rtac lem2 1, resolve_tac prems 1]);
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    55
7879
4547f0bd9454 fixed comments
paulson
parents: 5704
diff changeset
    56
   (*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*)
5704
1ddf7e1e8b19 improved var names;
wenzelm
parents: 5680
diff changeset
    57
   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
    58
     (fn prems => [resolve_tac prems 1]);
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    59
  in standard (Thm.equal_intr lem4 lem3) end;
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    60
9039
20ff649a0fd1 added rule_params;
wenzelm
parents: 7879
diff changeset
    61
val rule = rule_params "a" "b";
20ff649a0fd1 added rule_params;
wenzelm
parents: 7879
diff changeset
    62
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    63
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
diff changeset
    64
end;