# HG changeset patch # User wenzelm # Date 1172528307 -3600 # Node ID 6470ce514b6e170ab97c6294a2ef27af220815e7 # Parent d8d96d0122a76c1e3d79afae0633c4524a89f25f Further operations on type thm, outside the inference kernel. diff -r d8d96d0122a7 -r 6470ce514b6e src/Pure/more_thm.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/more_thm.ML Mon Feb 26 23:18:27 2007 +0100 @@ -0,0 +1,102 @@ +(* Title: Pure/more_thm.ML + ID: $Id$ + Author: Makarius + +Further operations on type thm, outside the inference kernel. +*) + +signature THM = +sig + include THM + val thm_ord: thm * thm -> order + val eq_thm: thm * thm -> bool + val eq_thms: thm list * thm list -> bool + val eq_thm_thy: thm * thm -> bool + val eq_thm_prop: thm * thm -> bool + val equiv_thm: thm * thm -> bool + val axiomK: string + val assumptionK: string + val definitionK: string + val theoremK: string + val lemmaK: string + val corollaryK: string + val internalK: string + val rule_attribute: (Context.generic -> thm -> thm) -> attribute + val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute + val theory_attributes: attribute list -> theory * thm -> theory * thm + val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm + val no_attributes: 'a -> 'a * 'b list + val simple_fact: 'a -> ('a * 'b list) list +end; + +structure Thm: THM = +struct + +(* compare theorems *) + +(*order: ignores theory context!*) +fun thm_ord (th1, th2) = + let + val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1; + val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2; + in + (case Term.fast_term_ord (prop1, prop2) of + EQUAL => + (case list_ord (prod_ord Term.fast_term_ord Term.fast_term_ord) (tpairs1, tpairs2) of + EQUAL => + (case list_ord Term.fast_term_ord (hyps1, hyps2) of + EQUAL => list_ord Term.sort_ord (shyps1, shyps2) + | ord => ord) + | ord => ord) + | ord => ord) + end; + +fun eq_thm ths = + Context.joinable (pairself Thm.theory_of_thm ths) andalso + thm_ord ths = EQUAL; + +val eq_thms = eq_list eq_thm; + +val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm; +val eq_thm_prop = op aconv o pairself Thm.full_prop_of; + +(*pattern equivalence*) +fun equiv_thm ths = + Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths); + + +(* theorem kinds *) + +val axiomK = "axiom"; +val assumptionK = "assumption"; +val definitionK = "definition"; +val theoremK = "theorem"; +val lemmaK = "lemma"; +val corollaryK = "corollary"; +val internalK = "internal"; + + + +(* attributes *) + +fun rule_attribute f (x, th) = (x, f x th); +fun declaration_attribute f (x, th) = (f th x, th); + +fun apply_attributes mk dest = + let + fun app [] = I + | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs; + in app end; + +val theory_attributes = apply_attributes Context.Theory Context.the_theory; +val proof_attributes = apply_attributes Context.Proof Context.the_proof; + +fun no_attributes x = (x, []); +fun simple_fact x = [(x, [])]; + + +open Thm; + +end; + +structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord);