src/Pure/drule.ML
 changeset 4016 90aebb69c04e parent 3991 4cb2f2422695 child 4057 edd8cb346109
equal 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;`