src/Pure/drule.ML
changeset 4016 90aebb69c04e
parent 3991 4cb2f2422695
child 4057 edd8cb346109
equal deleted inserted replaced
4015:92874142156b 4016:90aebb69c04e
   331            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   331            raise THM("cterm_instantiate: incompatible signatures",0,[th])
   332        | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
   332        | TYPE _ => raise THM("cterm_instantiate: types", 0, [th])
   333 end;
   333 end;
   334 
   334 
   335 
   335 
   336 (** theorem equality test is exported and used by BEST_FIRST **)
   336 (** theorem equality **)
   337 
   337 
   338 (*equality of theorems uses equality of signatures and
   338 val eq_thm = Thm.eq_thm;
   339   the a-convertible test for terms*)
       
   340 fun eq_thm (th1,th2) =
       
   341     let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
       
   342         and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
       
   343     in  Sign.eq_sg (sg1,sg2) andalso
       
   344         eq_set_sort (shyps1, shyps2) andalso
       
   345         aconvs(hyps1,hyps2) andalso
       
   346         prop1 aconv prop2
       
   347     end;
       
   348 
   339 
   349 (*equality of theorems using similarity of signatures,
   340 (*equality of theorems using similarity of signatures,
   350   i.e. the theorems belong to the same theory but not necessarily to the same
   341   i.e. the theorems belong to the same theory but not necessarily to the same
   351   version of this theory*)
   342   version of this theory*)
   352 fun same_thm (th1,th2) =
   343 fun same_thm (th1,th2) =
   386 
   377 
   387 
   378 
   388 
   379 
   389 (*** Meta-Rewriting Rules ***)
   380 (*** Meta-Rewriting Rules ***)
   390 
   381 
       
   382 fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
       
   383 
   391 val reflexive_thm =
   384 val reflexive_thm =
   392   let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
   385   let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
   393   in Thm.reflexive cx end;
   386   in store_thm "reflexive" (Thm.reflexive cx) end;
   394 
   387 
   395 val symmetric_thm =
   388 val symmetric_thm =
   396   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
   389   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
   397   in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
   390   in store_thm "symmetric" (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
   398 
   391 
   399 val transitive_thm =
   392 val transitive_thm =
   400   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
   393   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
   401       val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
   394       val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
   402       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   395       val xythm = Thm.assume xy and yzthm = Thm.assume yz
   403   in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   396   in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
   404 
   397 
   405 (** Below, a "conversion" has type cterm -> thm **)
   398 (** Below, a "conversion" has type cterm -> thm **)
   406 
   399 
   407 val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
   400 val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies);
   408 
   401 
   484 
   477 
   485 
   478 
   486 (*** Some useful meta-theorems ***)
   479 (*** Some useful meta-theorems ***)
   487 
   480 
   488 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   481 (*The rule V/V, obtains assumption solving for eresolve_tac*)
   489 val asm_rl = trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT));
   482 val asm_rl =
       
   483   store_thm "asm_rl" (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT)));
   490 
   484 
   491 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   485 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   492 val cut_rl = trivial(read_cterm (sign_of ProtoPure.thy)
   486 val cut_rl =
   493         ("PROP ?psi ==> PROP ?theta", propT));
   487   store_thm "cut_rl"
       
   488     (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi ==> PROP ?theta", propT)));
   494 
   489 
   495 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   490 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   496      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   491      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   497 val revcut_rl =
   492 val revcut_rl =
   498   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   493   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   499       and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
   494       and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
   500   in  standard (implies_intr V
   495   in
   501                 (implies_intr VW
   496     store_thm "revcut_rl"
   502                  (implies_elim (assume VW) (assume V))))
   497       (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   503   end;
   498   end;
   504 
   499 
   505 (*for deleting an unwanted assumption*)
   500 (*for deleting an unwanted assumption*)
   506 val thin_rl =
   501 val thin_rl =
   507   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   502   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   508       and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
   503       and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
   509   in  standard (implies_intr V (implies_intr W (assume W)))
   504   in  store_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   510   end;
   505   end;
   511 
   506 
   512 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   507 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   513 val triv_forall_equality =
   508 val triv_forall_equality =
   514   let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   509   let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
   515       and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
   510       and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
   516       and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
   511       and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
   517   in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   512   in
   518                            (implies_intr V  (forall_intr x (assume V))))
   513     store_thm "triv_forall_equality"
       
   514       (equal_intr (implies_intr QV (forall_elim x (assume QV)))
       
   515         (implies_intr V  (forall_intr x (assume V))))
   519   end;
   516   end;
   520 
   517 
   521 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   518 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   522    (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
   519    (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
   523    `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   520    `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   528       val major = assume cmajor;
   525       val major = assume cmajor;
   529       val cminor1 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiA", propT);
   526       val cminor1 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiA", propT);
   530       val minor1 = assume cminor1;
   527       val minor1 = assume cminor1;
   531       val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
   528       val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
   532       val minor2 = assume cminor2;
   529       val minor2 = assume cminor2;
   533   in standard
   530   in store_thm "swap_prems_rl"
   534        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   531        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   535          (implies_elim (implies_elim major minor1) minor2))))
   532          (implies_elim (implies_elim major minor1) minor2))))
   536   end;
   533   end;
   537 
   534 
   538 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
   535 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
   540    Introduction rule for == using ==> not meta-hyps.
   537    Introduction rule for == using ==> not meta-hyps.
   541 *)
   538 *)
   542 val equal_intr_rule =
   539 val equal_intr_rule =
   543   let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
   540   let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
   544       and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
   541       and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
   545   in  equal_intr (assume PQ) (assume QP)
   542   in
   546       |> implies_intr QP
   543     store_thm "equal_intr_rule"
   547       |> implies_intr PQ
   544       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   548       |> standard
       
   549   end;
   545   end;
   550 
   546 
   551 end;
   547 end;
   552 
   548 
   553 open Drule;
   549 open Drule;