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;
     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_params: string -> string -> thm -> thm
    16   val rule: thm -> thm
    17 end;
    18 
    19 structure SplitPairedAll: SPLIT_PAIRED_ALL =
    20 struct
    21 
    22 
    23 fun all x T t = Term.all T $ Abs (x, T, t);
    24 
    25 infixr ==>;
    26 val op ==> = Logic.mk_implies;
    27 
    28 
    29 fun rule_params a b raw_surj_pair =
    30   let
    31     val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair);
    32 
    33     val surj_pair = Drule.unvarify (standard raw_surj_pair);
    34     val used = Term.add_term_names (#prop (Thm.rep_thm surj_pair), []);
    35 
    36     val (p, con $ _ $ _) = Logic.dest_equals (#prop (rep_thm surj_pair));
    37     val pT as Type (_, [aT, bT]) = fastype_of p;
    38     val P = Free (variant used "P", pT --> propT);
    39 
    40    (*"!!a b. PROP (a, b)"*)
    41    val all_a_b = all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0)));
    42    (*"!!x. PROP P x"*)
    43    val all_x = all "x" pT (P $ Bound 0);
    44 
    45    (*lemma "P p == P (fst p, snd p)"*)
    46    val lem1 = Thm.combination (Thm.reflexive (ct P)) surj_pair;
    47 
    48    (*lemma "(!!a b. PROP P (a,b)) ==> PROP P p"*)
    49    val lem2 = prove_goalw_cterm [lem1] (ct (all_a_b ==> P $ p))
    50      (fn prems => [resolve_tac prems 1]);
    51 
    52    (*lemma "(!!a b. PROP P (a,b)) ==> !!x. PROP P x"*)
    53    val lem3 = prove_goalw_cterm [] (ct (all_a_b ==> all_x))
    54      (fn prems => [rtac lem2 1, resolve_tac prems 1]);
    55 
    56    (*lemma "(!!x. PROP P x) ==> !!a b. PROP P (a,b)"*)
    57    val lem4 = prove_goalw_cterm [] (ct (all_x ==> all_a_b))
    58      (fn prems => [resolve_tac prems 1]);
    59   in standard (Thm.equal_intr lem4 lem3) end;
    60 
    61 val rule = rule_params "a" "b";
    62 
    63 
    64 end;