src/Pure/more_thm.ML
author haftmann
Mon Dec 03 16:04:16 2007 +0100 (2007-12-03)
changeset 25518 00d5cc16e891
parent 24980 16a74cfca971
child 26628 63306cb94313
permissions -rw-r--r--
interface for unchecked definitions
     1 (*  Title:      Pure/more_thm.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Further operations on type ctyp/cterm/thm, outside the inference kernel.
     6 *)
     7 
     8 infix aconvc;
     9 
    10 signature THM =
    11 sig
    12   include THM
    13   val aconvc: cterm * cterm -> bool
    14   val add_cterm_frees: cterm -> cterm list -> cterm list
    15   val mk_binop: cterm -> cterm -> cterm -> cterm
    16   val dest_binop: cterm -> cterm * cterm
    17   val dest_implies: cterm -> cterm * cterm
    18   val dest_equals: cterm -> cterm * cterm
    19   val dest_equals_lhs: cterm -> cterm
    20   val dest_equals_rhs: cterm -> cterm
    21   val lhs_of: thm -> cterm
    22   val rhs_of: thm -> cterm
    23   val thm_ord: thm * thm -> order
    24   val is_reflexive: thm -> bool
    25   val eq_thm: thm * thm -> bool
    26   val eq_thms: thm list * thm list -> bool
    27   val eq_thm_thy: thm * thm -> bool
    28   val eq_thm_prop: thm * thm -> bool
    29   val equiv_thm: thm * thm -> bool
    30   val is_dummy: thm -> bool
    31   val plain_prop_of: thm -> term
    32   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
    33   val add_thm: thm -> thm list -> thm list
    34   val del_thm: thm -> thm list -> thm list
    35   val merge_thms: thm list * thm list -> thm list
    36   val axiomK: string
    37   val assumptionK: string
    38   val definitionK: string
    39   val theoremK: string
    40   val lemmaK: string
    41   val corollaryK: string
    42   val internalK: string
    43   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
    44   val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
    45   val theory_attributes: attribute list -> theory * thm -> theory * thm
    46   val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
    47   val no_attributes: 'a -> 'a * 'b list
    48   val simple_fact: 'a -> ('a * 'b list) list
    49   val read_def_cterms:
    50     theory * (indexname -> typ option) * (indexname -> sort option) ->
    51     string list -> bool -> (string * typ)list
    52     -> cterm list * (indexname * typ)list
    53   val read_cterm: theory -> string * typ -> cterm
    54   val elim_implies: thm -> thm -> thm
    55   val unvarify: thm -> thm
    56   val add_axiom: term list -> bstring * term -> theory -> thm * theory
    57   val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
    58 end;
    59 
    60 structure Thm: THM =
    61 struct
    62 
    63 (** basic operations **)
    64 
    65 (* collecting cterms *)
    66 
    67 val op aconvc = op aconv o pairself Thm.term_of;
    68 
    69 fun add_cterm_frees ct =
    70   let
    71     val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
    72     val t = Thm.term_of ct;
    73   in Term.fold_aterms (fn v as Free _ => insert (op aconvc) (cert v) | _ => I) t end;
    74 
    75 
    76 (* cterm constructors and destructors *)
    77 
    78 fun mk_binop c a b = Thm.capply (Thm.capply c a) b;
    79 fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
    80 
    81 fun dest_implies ct =
    82   (case Thm.term_of ct of
    83     Const ("==>", _) $ _ $ _ => dest_binop ct
    84   | _ => raise TERM ("dest_implies", [Thm.term_of ct]));
    85 
    86 fun dest_equals ct =
    87   (case Thm.term_of ct of
    88     Const ("==", _) $ _ $ _ => dest_binop ct
    89   | _ => raise TERM ("dest_equals", [Thm.term_of ct]));
    90 
    91 fun dest_equals_lhs ct =
    92   (case Thm.term_of ct of
    93     Const ("==", _) $ _ $ _ => Thm.dest_arg1 ct
    94   | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
    95 
    96 fun dest_equals_rhs ct =
    97   (case Thm.term_of ct of
    98     Const ("==", _) $ _ $ _ => Thm.dest_arg ct
    99   | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
   100 
   101 val lhs_of = dest_equals_lhs o Thm.cprop_of;
   102 val rhs_of = dest_equals_rhs o Thm.cprop_of;
   103 
   104 
   105 (* thm order: ignores theory context! *)
   106 
   107 fun thm_ord (th1, th2) =
   108   let
   109     val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1;
   110     val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2;
   111   in
   112     (case Term.fast_term_ord (prop1, prop2) of
   113       EQUAL =>
   114         (case list_ord (prod_ord Term.fast_term_ord Term.fast_term_ord) (tpairs1, tpairs2) of
   115           EQUAL =>
   116             (case list_ord Term.fast_term_ord (hyps1, hyps2) of
   117               EQUAL => list_ord Term.sort_ord (shyps1, shyps2)
   118             | ord => ord)
   119         | ord => ord)
   120     | ord => ord)
   121   end;
   122 
   123 
   124 (* equality *)
   125 
   126 fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th))
   127   handle TERM _ => false;
   128 
   129 fun eq_thm ths =
   130   Context.joinable (pairself Thm.theory_of_thm ths) andalso
   131   thm_ord ths = EQUAL;
   132 
   133 val eq_thms = eq_list eq_thm;
   134 
   135 val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
   136 val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
   137 
   138 
   139 (* pattern equivalence *)
   140 
   141 fun equiv_thm ths =
   142   Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
   143 
   144 
   145 (* misc operations *)
   146 
   147 fun is_dummy thm =
   148   (case try Logic.dest_term (Thm.concl_of thm) of
   149     NONE => false
   150   | SOME t => Term.is_dummy_pattern t);
   151 
   152 fun plain_prop_of raw_thm =
   153   let
   154     val thm = Thm.strip_shyps raw_thm;
   155     fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
   156     val {hyps, prop, tpairs, ...} = Thm.rep_thm thm;
   157   in
   158     if not (null hyps) then
   159       err "theorem may not contain hypotheses"
   160     else if not (null (Thm.extra_shyps thm)) then
   161       err "theorem may not contain sort hypotheses"
   162     else if not (null tpairs) then
   163       err "theorem may not contain flex-flex pairs"
   164     else prop
   165   end;
   166 
   167 fun fold_terms f th =
   168   let val {tpairs, prop, hyps, ...} = Thm.rep_thm th
   169   in fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps end;
   170 
   171 
   172 (* lists of theorems in canonical order *)
   173 
   174 val add_thm = update eq_thm_prop;
   175 val del_thm = remove eq_thm_prop;
   176 val merge_thms = merge eq_thm_prop;
   177 
   178 
   179 
   180 (** theorem kinds **)
   181 
   182 val axiomK = "axiom";
   183 val assumptionK = "assumption";
   184 val definitionK = "definition";
   185 val theoremK = "theorem";
   186 val lemmaK = "lemma";
   187 val corollaryK = "corollary";
   188 val internalK = Markup.internalK;
   189 
   190 
   191 
   192 (** attributes **)
   193 
   194 fun rule_attribute f (x, th) = (x, f x th);
   195 fun declaration_attribute f (x, th) = (f th x, th);
   196 
   197 fun apply_attributes mk dest =
   198   let
   199     fun app [] = I
   200       | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs;
   201   in app end;
   202 
   203 val theory_attributes = apply_attributes Context.Theory Context.the_theory;
   204 val proof_attributes = apply_attributes Context.Proof Context.the_proof;
   205 
   206 fun no_attributes x = (x, []);
   207 fun simple_fact x = [(x, [])];
   208 
   209 
   210 (** read/certify terms (obsolete) **)    (*exception ERROR*)
   211 
   212 fun read_def_cterms (thy, types, sorts) used freeze sTs =
   213   let
   214     val (ts', tye) = Sign.read_def_terms (thy, types, sorts) used freeze sTs;
   215     val cts = map (Thm.cterm_of thy) ts'
   216       handle TYPE (msg, _, _) => error msg
   217            | TERM (msg, _) => error msg;
   218   in (cts, tye) end;
   219 
   220 fun read_cterm thy sT =
   221   let val ([ct], _) = read_def_cterms (thy, K NONE, K NONE) [] true [sT]
   222   in ct end;
   223 
   224 
   225 
   226 (** basic derived rules **)
   227 
   228 (*Elimination of implication
   229   A    A ==> B
   230   ------------
   231         B
   232 *)
   233 fun elim_implies thA thAB = Thm.implies_elim thAB thA;
   234 
   235 (*global schematic variables*)
   236 fun unvarify th =
   237   let
   238     val thy = Thm.theory_of_thm th;
   239     val cert = Thm.cterm_of thy;
   240     val certT = Thm.ctyp_of thy;
   241 
   242     val prop = Thm.full_prop_of th;
   243     val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
   244       handle TERM (msg, _) => raise THM (msg, 0, [th]);
   245 
   246     val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
   247     val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
   248     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
   249       let val T' = TermSubst.instantiateT instT0 T
   250       in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
   251   in Thm.instantiate (instT, inst) th end;
   252 
   253 
   254 
   255 (** specification primitives **)
   256 
   257 fun add_axiom hyps (name, prop) thy =
   258   let
   259     val name' = if name = "" then "axiom_" ^ serial_string () else name;
   260     val prop' = Logic.list_implies (hyps, prop);
   261     val thy' = thy |> Theory.add_axioms_i [(name', prop')];
   262     val axm = unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
   263     val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
   264     val thm = fold elim_implies prems axm;
   265   in (thm, thy') end;
   266 
   267 fun add_def unchecked overloaded (name, prop) thy =
   268   let
   269     val tfrees = rev (map TFree (Term.add_tfrees prop []));
   270     val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
   271     val strip_sorts = tfrees ~~ tfrees';
   272     val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
   273 
   274     val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
   275     val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
   276     val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
   277     val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   278   in (thm, thy') end;
   279 
   280 open Thm;
   281 
   282 end;
   283 
   284 val op aconvc = Thm.aconvc;
   285 
   286 structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord);