moved theorem tags from Drule to PureThy;
authorwenzelm
Fri Jan 27 19:03:02 2006 +0100 (2006-01-27)
changeset 18799f137c5e971f5
parent 18798 ca02a2077955
child 18800 c0f90bbf3865
moved theorem tags from Drule to PureThy;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/pcpodef_package.ML
src/Provers/induct_method.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Thy/thm_deps.ML
src/Pure/axclass.ML
src/Pure/drule.ML
src/ZF/Tools/ind_cases.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 27 18:29:33 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 27 19:03:02 2006 +0100
     1.3 @@ -369,7 +369,7 @@
     1.4        [(("", proj index), [InductAttrib.induct_type name]),
     1.5         (("", exhaustion), [InductAttrib.cases_type name])];
     1.6      fun unnamed_rule i =
     1.7 -      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type ""]);
     1.8 +      (("", proj i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
     1.9    in
    1.10      PureThy.add_thms
    1.11        (List.concat (map named_rules infos) @
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jan 27 18:29:33 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jan 27 19:03:02 2006 +0100
     2.3 @@ -570,7 +570,7 @@
     2.4  
     2.5      val facts = args |> map (fn ((a, atts), props) =>
     2.6       ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
     2.7 -  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
     2.8 +  in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
     2.9  
    2.10  val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
    2.11  val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jan 27 18:29:33 2006 +0100
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Jan 27 19:03:02 2006 +0100
     3.3 @@ -280,7 +280,7 @@
     3.4      val tc = List.nth (tcs, i - 1) handle Subscript =>
     3.5        error ("No termination condition #" ^ string_of_int i ^
     3.6          " in recdef definition of " ^ quote name);
     3.7 -  in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
     3.8 +  in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
     3.9  
    3.10  val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
    3.11  val recdef_tc_i = gen_recdef_tc (K I) (K I);
     4.1 --- a/src/HOL/Tools/specification_package.ML	Fri Jan 27 18:29:33 2006 +0100
     4.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Jan 27 19:03:02 2006 +0100
     4.3 @@ -231,7 +231,7 @@
     4.4              fun post_proc (context, th) =
     4.5                  post_process (Context.theory_of context, th) |>> Context.Theory;
     4.6      in
     4.7 -      IsarThy.theorem_i Drule.internalK
     4.8 +      IsarThy.theorem_i PureThy.internalK
     4.9          ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
    4.10          (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
    4.11      end
     5.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jan 27 18:29:33 2006 +0100
     5.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Jan 27 19:03:02 2006 +0100
     5.3 @@ -256,7 +256,7 @@
     5.4      val (_, goal, goal_pat, att_result) =
     5.5        prepare_typedef prep_term def name typ set opt_morphs thy;
     5.6      val att = #1 o att_result;
     5.7 -  in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
     5.8 +  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
     5.9  
    5.10  in
    5.11  
     6.1 --- a/src/HOLCF/pcpodef_package.ML	Fri Jan 27 18:29:33 2006 +0100
     6.2 +++ b/src/HOLCF/pcpodef_package.ML	Fri Jan 27 19:03:02 2006 +0100
     6.3 @@ -178,7 +178,7 @@
     6.4    let
     6.5      val (goal, att) =
     6.6        gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
     6.7 -  in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([], [])) thy end;
     6.8 +  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([], [])) thy end;
     6.9  
    6.10  fun pcpodef_proof x = gen_pcpodef_proof read_term true x;
    6.11  fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x;
     7.1 --- a/src/Provers/induct_method.ML	Fri Jan 27 18:29:33 2006 +0100
     7.2 +++ b/src/Provers/induct_method.ML	Fri Jan 27 19:03:02 2006 +0100
     7.3 @@ -363,7 +363,7 @@
     7.4  fun find_inductT ctxt insts =
     7.5    fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
     7.6      |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]]
     7.7 -  |> filter_out (forall Drule.is_internal);
     7.8 +  |> filter_out (forall PureThy.is_internal);
     7.9  
    7.10  fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact))
    7.11    | find_inductS _ _ = [];
     8.1 --- a/src/Pure/Isar/attrib.ML	Fri Jan 27 18:29:33 2006 +0100
     8.2 +++ b/src/Pure/Isar/attrib.ML	Fri Jan 27 19:03:02 2006 +0100
     8.3 @@ -202,8 +202,8 @@
     8.4  
     8.5  (* tags *)
     8.6  
     8.7 -fun tagged x = syntax (tag >> Drule.tag) x;
     8.8 -fun untagged x = syntax (Scan.lift Args.name >> Drule.untag) x;
     8.9 +fun tagged x = syntax (tag >> PureThy.tag) x;
    8.10 +fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x;
    8.11  
    8.12  
    8.13  (* rule composition *)
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jan 27 18:29:33 2006 +0100
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 27 19:03:02 2006 +0100
     9.3 @@ -212,10 +212,10 @@
     9.4    >> (Toplevel.theory_context o uncurry (IsarThy.smart_theorems kind));
     9.5  
     9.6  val theoremsP =
     9.7 -  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Drule.theoremK);
     9.8 +  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK);
     9.9  
    9.10  val lemmasP =
    9.11 -  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Drule.lemmaK);
    9.12 +  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems PureThy.lemmaK);
    9.13  
    9.14  val declareP =
    9.15    OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
    9.16 @@ -322,7 +322,7 @@
    9.17      ((P.opt_keyword "open" >> not) -- P.name
    9.18          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
    9.19        >> (Toplevel.theory_context o (fn ((x, y), (z, w)) =>
    9.20 -          Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt)))));
    9.21 +          Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (ctxt, thy)))));
    9.22  
    9.23  val opt_inst =
    9.24    Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
    9.25 @@ -359,9 +359,9 @@
    9.26        general_statement >> (fn ((x, y), (z, w)) =>
    9.27        (Toplevel.print o Toplevel.theory_to_proof (Locale.smart_theorem kind x y z w))));
    9.28  
    9.29 -val theoremP = gen_theorem Drule.theoremK;
    9.30 -val lemmaP = gen_theorem Drule.lemmaK;
    9.31 -val corollaryP = gen_theorem Drule.corollaryK;
    9.32 +val theoremP = gen_theorem PureThy.theoremK;
    9.33 +val lemmaP = gen_theorem PureThy.lemmaK;
    9.34 +val corollaryP = gen_theorem PureThy.corollaryK;
    9.35  
    9.36  val haveP =
    9.37    OuterSyntax.command "have" "state local goal"
    10.1 --- a/src/Pure/Isar/proof_display.ML	Fri Jan 27 18:29:33 2006 +0100
    10.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Jan 27 19:03:02 2006 +0100
    10.3 @@ -65,7 +65,7 @@
    10.4    | print_results false = K (K ());
    10.5  
    10.6  fun present_results ctxt ((kind, name), res) =
    10.7 -  if kind = "" orelse kind = Drule.internalK then ()
    10.8 +  if kind = "" orelse kind = PureThy.internalK then ()
    10.9    else (print_results true ctxt ((kind, name), res);
   10.10      Context.setmp (SOME (ProofContext.theory_of ctxt))
   10.11        (Present.results kind) (name_results name res));
    11.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Jan 27 18:29:33 2006 +0100
    11.2 +++ b/src/Pure/Isar/rule_cases.ML	Fri Jan 27 19:03:02 2006 +0100
    11.3 @@ -225,8 +225,8 @@
    11.4  
    11.5  fun put_consumes NONE th = th
    11.6    | put_consumes (SOME n) th = th
    11.7 -      |> Drule.untag_rule consumes_tagN
    11.8 -      |> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
    11.9 +      |> PureThy.untag_rule consumes_tagN
   11.10 +      |> PureThy.tag_rule (consumes_tagN, [Library.string_of_int n]);
   11.11  
   11.12  fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
   11.13  
   11.14 @@ -244,8 +244,8 @@
   11.15  
   11.16  fun add_case_names NONE = I
   11.17    | add_case_names (SOME names) =
   11.18 -      Drule.untag_rule case_names_tagN
   11.19 -      #> Drule.tag_rule (case_names_tagN, names);
   11.20 +      PureThy.untag_rule case_names_tagN
   11.21 +      #> PureThy.tag_rule (case_names_tagN, names);
   11.22  
   11.23  fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN;
   11.24  
   11.25 @@ -262,7 +262,7 @@
   11.26  fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name)
   11.27    | is_case_concl _ _ = false;
   11.28  
   11.29 -fun add_case_concl (name, cs) = Drule.map_tags (fn tags =>
   11.30 +fun add_case_concl (name, cs) = PureThy.map_tags (fn tags =>
   11.31    filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
   11.32  
   11.33  fun get_case_concls th name =
    12.1 --- a/src/Pure/Thy/thm_deps.ML	Fri Jan 27 18:29:33 2006 +0100
    12.2 +++ b/src/Pure/Thy/thm_deps.ML	Fri Jan 27 19:03:02 2006 +0100
    12.3 @@ -39,7 +39,7 @@
    12.4    | make_deps_graph prf = (fn p as (gra, parents) =>
    12.5        let val ((name, tags), prf') = dest_thm_axm prf
    12.6        in
    12.7 -        if name <> "" andalso not (Drule.has_internal tags) then
    12.8 +        if name <> "" andalso not (PureThy.has_internal tags) then
    12.9            if not (Symtab.defined gra name) then
   12.10              let
   12.11                val (gra', parents') = make_deps_graph prf' (gra, []);
    13.1 --- a/src/Pure/axclass.ML	Fri Jan 27 18:29:33 2006 +0100
    13.2 +++ b/src/Pure/axclass.ML	Fri Jan 27 19:03:02 2006 +0100
    13.3 @@ -306,7 +306,7 @@
    13.4  fun gen_instance mk_prop add_thms after_qed inst thy =
    13.5    thy
    13.6    |> ProofContext.init
    13.7 -  |> Proof.theorem_i Drule.internalK NONE (after_qed oo fold add_thms) NONE ("", [])
    13.8 +  |> Proof.theorem_i PureThy.internalK NONE (after_qed oo fold add_thms) NONE ("", [])
    13.9         (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
   13.10  
   13.11  in
    14.1 --- a/src/Pure/drule.ML	Fri Jan 27 18:29:33 2006 +0100
    14.2 +++ b/src/Pure/drule.ML	Fri Jan 27 19:03:02 2006 +0100
    14.3 @@ -92,20 +92,6 @@
    14.4    val beta_conv: cterm -> cterm -> cterm
    14.5    val plain_prop_of: thm -> term
    14.6    val add_used: thm -> string list -> string list
    14.7 -  val map_tags: (tag list -> tag list) -> thm -> thm
    14.8 -  val tag_rule: tag -> thm -> thm
    14.9 -  val untag_rule: string -> thm -> thm
   14.10 -  val tag: tag -> attribute
   14.11 -  val untag: string -> attribute
   14.12 -  val get_kind: thm -> string
   14.13 -  val kind: string -> attribute
   14.14 -  val theoremK: string
   14.15 -  val lemmaK: string
   14.16 -  val corollaryK: string
   14.17 -  val internalK: string
   14.18 -  val kind_internal: attribute
   14.19 -  val has_internal: tag list -> bool
   14.20 -  val is_internal: thm -> bool
   14.21    val flexflex_unique: thm -> thm
   14.22    val close_derivation: thm -> thm
   14.23    val local_standard: thm -> thm
   14.24 @@ -322,42 +308,6 @@
   14.25  
   14.26  
   14.27  
   14.28 -(** theorem tags **)
   14.29 -
   14.30 -(* add / delete tags *)
   14.31 -
   14.32 -fun map_tags f thm =
   14.33 -  Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
   14.34 -
   14.35 -fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
   14.36 -fun untag_rule s = map_tags (filter_out (equal s o #1));
   14.37 -
   14.38 -fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
   14.39 -fun untag s x = Thm.rule_attribute (K (untag_rule s)) x;
   14.40 -
   14.41 -fun simple_tag name x = tag (name, []) x;
   14.42 -
   14.43 -
   14.44 -(* theorem kinds *)
   14.45 -
   14.46 -val theoremK = "theorem";
   14.47 -val lemmaK = "lemma";
   14.48 -val corollaryK = "corollary";
   14.49 -val internalK = "internal";
   14.50 -
   14.51 -fun get_kind thm =
   14.52 -  (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of
   14.53 -    SOME (k :: _) => k
   14.54 -  | _ => "unknown");
   14.55 -
   14.56 -fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind";
   14.57 -fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x;
   14.58 -fun kind_internal x = kind internalK x;
   14.59 -fun has_internal tags = exists (fn ("kind", [k]) => k = internalK | _ => false) tags;
   14.60 -val is_internal = has_internal o Thm.tags_of_thm;
   14.61 -
   14.62 -
   14.63 -
   14.64  (** Standardization of rules **)
   14.65  
   14.66  (*vars in left-to-right order*)
   14.67 @@ -984,9 +934,9 @@
   14.68    val prop_def = #1 (freeze_thaw ProtoPure.prop_def);
   14.69  in
   14.70    val protect = Thm.capply (cert Logic.protectC);
   14.71 -  val protectI = store_thm "protectI" (kind_rule internalK (standard
   14.72 +  val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
   14.73        (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   14.74 -  val protectD = store_thm "protectD" (kind_rule internalK (standard
   14.75 +  val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard
   14.76        (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   14.77    val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
   14.78  end;
    15.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Jan 27 18:29:33 2006 +0100
    15.2 +++ b/src/ZF/Tools/ind_cases.ML	Fri Jan 27 19:03:02 2006 +0100
    15.3 @@ -55,7 +55,7 @@
    15.4      val facts = args |> map (fn ((name, srcs), props) =>
    15.5        ((name, map (Attrib.attribute thy) srcs),
    15.6          map (Thm.no_attributes o single o mk_cases) props));
    15.7 -  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
    15.8 +  in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
    15.9  
   15.10  
   15.11  (* ind_cases method *)