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