src/Pure/theory.ML
author blanchet
Mon, 06 Dec 2010 13:29:23 +0100
changeset 40996 63112be4a469
parent 39134 917b4b6ba3d2
child 42016 3b6826b3ed37
permissions -rw-r--r--
added "Neq" operator to monotonicity inference module
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     1
(*  Title:      Pure/theory.ML
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson and Markus Wenzel
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     3
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
     4
Logical theory content: axioms, definitions, and begin/end wrappers.
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
     5
*)
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
     6
26668
65023d4fd226 removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
wenzelm
parents: 26631
diff changeset
     7
signature THEORY =
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
     8
sig
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
     9
  val eq_thy: theory * theory -> bool
3996
b7548325adc4 tuned names;
wenzelm
parents: 3971
diff changeset
    10
  val subthy: theory * theory -> bool
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    11
  val assert_super: theory -> theory -> theory
22684
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
    12
  val parents_of: theory -> theory list
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
    13
  val ancestors_of: theory -> theory list
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    14
  val check_thy: theory -> theory_ref
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    15
  val deref: theory_ref -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    16
  val merge: theory * theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    17
  val merge_refs: theory_ref * theory_ref -> theory_ref
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    18
  val merge_list: theory list -> theory
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    19
  val checkpoint: theory -> theory
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    20
  val copy: theory -> theory
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    21
  val requires: theory -> string -> string -> unit
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
    22
  val axiom_space: theory -> Name_Space.T
22684
a614c5f506ea tuned signature;
wenzelm
parents: 22600
diff changeset
    23
  val axiom_table: theory -> term Symtab.table
16339
b02b6da609c3 axioms and oracles: NameSpace.table;
wenzelm
parents: 16313
diff changeset
    24
  val axioms_of: theory -> (string * term) list
b02b6da609c3 axioms and oracles: NameSpace.table;
wenzelm
parents: 16313
diff changeset
    25
  val all_axioms_of: theory -> (string * term) list
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    26
  val defs_of: theory -> Defs.T
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    27
  val at_begin: (theory -> theory option) -> theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    28
  val at_end: (theory -> theory option) -> theory -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    29
  val begin_theory: string -> theory list -> theory
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    30
  val end_theory: theory -> theory
35857
28e73b3e7b6c replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents: 35845
diff changeset
    31
  val add_axiom: binding * term -> theory -> theory
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
    32
  val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
    33
  val add_def: bool -> bool -> binding * term -> theory -> theory
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
    34
  val add_finals_i: bool -> term list -> theory -> theory
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    35
  val add_finals: bool -> string list -> theory -> theory
33173
b8ca12f6681a eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents: 33168
diff changeset
    36
  val specify_const: (binding * typ) * mixfix -> theory -> term * theory
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    37
end
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
    38
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    39
structure Theory: THEORY =
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    40
struct
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    41
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
    42
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    43
(** theory context operations **)
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    44
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    45
val eq_thy = Context.eq_thy;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    46
val subthy = Context.subthy;
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
    47
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    48
fun assert_super thy1 thy2 =
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    49
  if subthy (thy1, thy2) then thy2
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    50
  else raise THEORY ("Not a super theory", [thy1, thy2]);
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24199
diff changeset
    51
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    52
val parents_of = Context.parents_of;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    53
val ancestors_of = Context.ancestors_of;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    54
24137
8d7896398147 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents: 23655
diff changeset
    55
val check_thy = Context.check_thy;
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    56
val deref = Context.deref;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    57
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    58
val merge = Context.merge;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    59
val merge_refs = Context.merge_refs;
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
    60
23600
5a5332e1351b removed comments -- no exception TERM;
wenzelm
parents: 23086
diff changeset
    61
fun merge_list [] = raise THEORY ("Empty merge of theories", [])
21608
2ca27eeb2841 added merge_list;
wenzelm
parents: 20549
diff changeset
    62
  | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
2ca27eeb2841 added merge_list;
wenzelm
parents: 20549
diff changeset
    63
16495
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    64
val checkpoint = Context.checkpoint_thy;
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    65
val copy = Context.copy_thy;
2e99aca906a7 added begin_theory, end_theory;
wenzelm
parents: 16443
diff changeset
    66
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    67
fun requires thy name what =
29092
466a83cb6f5f requires: check ancestors directly;
wenzelm
parents: 29004
diff changeset
    68
  if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then ()
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    69
  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    70
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    71
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    72
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    73
(** datatype thy **)
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    74
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    75
type wrapper = (theory -> theory option) * stamp;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    76
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    77
fun apply_wrappers (wrappers: wrapper list) =
25059
e6e0ee56a672 apply_wrappers: perhaps_apply/loop;
wenzelm
parents: 25017
diff changeset
    78
  perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    79
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    80
datatype thy = Thy of
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
    81
 {axioms: term Name_Space.table,
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    82
  defs: Defs.T,
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    83
  wrappers: wrapper list * wrapper list};
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    84
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
    85
fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    86
34259
2ba492b8b6e8 discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents: 34245
diff changeset
    87
structure ThyData = Theory_Data_PP
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    88
(
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    89
  type T = thy;
33159
369da293bbd4 make SML/NJ happy;
wenzelm
parents: 33096
diff changeset
    90
  val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    91
  val empty = make_thy (empty_axioms, Defs.empty, ([], []));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    92
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
    93
  fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    94
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    95
  fun merge pp (thy1, thy2) =
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    96
    let
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
    97
      val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
    98
      val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
    99
33096
db3c18fd9708 maintain explicit name space kind;
wenzelm
parents: 33095
diff changeset
   100
      val axioms' = empty_axioms;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   101
      val defs' = Defs.merge pp (defs1, defs2);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   102
      val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   103
      val ens' = Library.merge (eq_snd op =) (ens1, ens2);
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   104
    in make_thy (axioms', defs', (bgs', ens')) end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   105
);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   106
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   107
fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   108
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   109
fun map_thy f = ThyData.map (fn (Thy {axioms, defs, wrappers}) =>
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   110
  make_thy (f (axioms, defs, wrappers)));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   111
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   112
28290
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   113
fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   114
fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
4cc2b6046258 simplified oracle interface;
wenzelm
parents: 28112
diff changeset
   115
fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   116
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   117
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   118
(* basic operations *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   119
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   120
val axiom_space = #1 o #axioms o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   121
val axiom_table = #2 o #axioms o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   122
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   123
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   124
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   125
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   126
val defs_of = #defs o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   127
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   128
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   129
(* begin/end theory *)
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   130
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   131
val begin_wrappers = rev o #1 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   132
val end_wrappers = rev o #2 o #wrappers o rep_theory;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   133
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   134
fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   135
fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   136
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   137
fun begin_theory name imports =
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   138
  let
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26668
diff changeset
   139
    val thy = Context.begin_thy Syntax.pp_global name imports;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   140
    val wrappers = begin_wrappers thy;
33168
853493e5d5d4 begin_theory: set theory_name here;
wenzelm
parents: 33159
diff changeset
   141
  in
853493e5d5d4 begin_theory: set theory_name here;
wenzelm
parents: 33159
diff changeset
   142
    thy
853493e5d5d4 begin_theory: set theory_name here;
wenzelm
parents: 33159
diff changeset
   143
    |> Sign.local_path
853493e5d5d4 begin_theory: set theory_name here;
wenzelm
parents: 33159
diff changeset
   144
    |> Sign.map_naming (Name_Space.set_theory_name name)
853493e5d5d4 begin_theory: set theory_name here;
wenzelm
parents: 33159
diff changeset
   145
    |> apply_wrappers wrappers
853493e5d5d4 begin_theory: set theory_name here;
wenzelm
parents: 33159
diff changeset
   146
  end;
24666
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   147
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   148
fun end_theory thy =
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   149
  thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
9885a86f14a8 tuned signature;
wenzelm
parents: 24626
diff changeset
   150
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   151
3996
b7548325adc4 tuned names;
wenzelm
parents: 3971
diff changeset
   152
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   153
(** primitive specifications **)
3814
b0dc68aa1b6a improved oracles: named, many per theory;
wenzelm
parents: 3806
diff changeset
   154
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   155
(* raw axioms *)
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   156
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   157
fun cert_axm thy (b, raw_tm) =
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   158
  let
32789
d89327de0b3c removed redundant Sign.certify_prop, use Sign.cert_prop instead;
wenzelm
parents: 30466
diff changeset
   159
    val t = Sign.cert_prop thy raw_tm
2979
db6941221197 improved type check error messages;
wenzelm
parents: 2693
diff changeset
   160
      handle TYPE (msg, _, _) => error msg
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   161
        | TERM (msg, _) => error msg;
35987
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   162
    val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   163
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   164
    val ctxt = Syntax.init_pretty_global thy
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   165
      |> Config.put show_sorts true;
35987
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   166
    val bad_sorts =
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   167
      rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   168
    val _ = null bad_sorts orelse
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   169
      error ("Illegal sort constraints in primitive specification: " ^
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   170
        commas (map (Syntax.string_of_typ ctxt) bad_sorts));
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   171
  in
39133
70d3915c92f0 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents: 36610
diff changeset
   172
    (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
35987
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   173
  end handle ERROR msg =>
7c728daf4876 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
wenzelm
parents: 35985
diff changeset
   174
    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   175
35857
28e73b3e7b6c replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents: 35845
diff changeset
   176
fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   177
  let
35857
28e73b3e7b6c replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents: 35845
diff changeset
   178
    val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
28e73b3e7b6c replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents: 35845
diff changeset
   179
    val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms;
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   180
  in axioms' end);
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   181
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   182
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   183
(* dependencies *)
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   184
33701
9dd1079cec3a primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents: 33173
diff changeset
   185
fun dependencies thy unchecked def description lhs rhs =
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   186
  let
39133
70d3915c92f0 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents: 36610
diff changeset
   187
    val ctxt = Syntax.init_pretty_global thy;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   188
    val consts = Sign.consts_of thy;
19727
wenzelm
parents: 19708
diff changeset
   189
    fun prep const =
39133
70d3915c92f0 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents: 36610
diff changeset
   190
      let val Const (c, T) = Sign.no_vars ctxt (Const const)
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 34259
diff changeset
   191
      in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   192
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   193
    val lhs_vars = Term.add_tfreesT (#2 lhs) [];
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   194
    val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   195
      if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   196
    val _ =
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   197
      if null rhs_extras then ()
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   198
      else error ("Specification depends on extra type variables: " ^
39133
70d3915c92f0 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents: 36610
diff changeset
   199
        commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
33701
9dd1079cec3a primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents: 33173
diff changeset
   200
        "\nThe error(s) above occurred in " ^ quote description);
39133
70d3915c92f0 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents: 36610
diff changeset
   201
  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
19708
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   202
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   203
fun add_deps a raw_lhs raw_rhs thy =
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   204
  let
a508bde37a81 added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents: 19700
diff changeset
   205
    val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
33701
9dd1079cec3a primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents: 33173
diff changeset
   206
    val description = if a = "" then #1 lhs ^ " axiom" else a;
9dd1079cec3a primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents: 33173
diff changeset
   207
  in thy |> map_defs (dependencies thy false NONE description lhs rhs) end;
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   208
33173
b8ca12f6681a eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents: 33168
diff changeset
   209
fun specify_const decl thy =
b8ca12f6681a eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
wenzelm
parents: 33168
diff changeset
   210
  let val (t as Const const, thy') = Sign.declare_const decl thy
28112
691993ef6abe simplified specify_const: canonical args, global deps;
wenzelm
parents: 28017
diff changeset
   211
  in (t, add_deps "" const [] thy') end;
25017
e82ab4962f80 Theory.specify_const: added deps argument;
wenzelm
parents: 24981
diff changeset
   212
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   213
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   214
(* overloading *)
9280
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   215
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   216
fun check_overloading thy overloaded (c, T) =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   217
  let
24763
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   218
    val declT = Sign.the_const_constraint thy c
da4a9986eccd Sign.the_const_constraint;
wenzelm
parents: 24708
diff changeset
   219
      handle TYPE (msg, _, _) => error msg;
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 34259
diff changeset
   220
    val T' = Logic.varifyT_global T;
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   221
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   222
    val ctxt = Syntax.init_pretty_global thy;
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   223
    fun message sorts txt =
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   224
      [Pretty.block [Pretty.str "Specification of constant ",
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   225
        Pretty.str c, Pretty.str " ::", Pretty.brk 1,
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   226
        Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   227
        Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   228
  in
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   229
    if Sign.typ_instance thy (declT, T') then ()
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   230
    else if Type.raw_instance (declT, T') then
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   231
      error (message true "imposes additional sort constraints on the constant declaration")
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   232
    else if overloaded then ()
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   233
    else warning (message false "is strictly less general than the declared type")
9280
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   234
  end;
78a9bca983ac Tightened up check of types in constant defs.
nipkow
parents: 8897
diff changeset
   235
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   236
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   237
(* definitional axioms *)
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   238
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   239
local
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   240
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   241
fun check_def thy unchecked overloaded (b, tm) defs =
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   242
  let
36610
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 35988
diff changeset
   243
    val ctxt = ProofContext.init_global thy;
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   244
    val name = Sign.full_name thy b;
35988
76ca601c941e disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents: 35987
diff changeset
   245
    val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
76ca601c941e disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents: 35987
diff changeset
   246
      handle TERM (msg, _) => error msg;
76ca601c941e disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
wenzelm
parents: 35987
diff changeset
   247
    val lhs_const = Term.dest_Const (Term.head_of lhs);
16944
83ea7e3c6ec9 check_overloading replaces datatype overloading;
wenzelm
parents: 16883
diff changeset
   248
    val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
18943
947d3a694654 moved no_vars to sign.ML;
wenzelm
parents: 18857
diff changeset
   249
    val _ = check_overloading thy overloaded lhs_const;
33701
9dd1079cec3a primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents: 33173
diff changeset
   250
  in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18338
diff changeset
   251
  handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
30218
cdd82ba2b4fd Binding.str_of;
wenzelm
parents: 29606
diff changeset
   252
   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26668
diff changeset
   253
    Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   254
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   255
in
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   256
35985
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   257
fun add_def unchecked overloaded raw_axm thy =
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   258
  let val axm = cert_axm thy raw_axm in
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   259
    thy
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   260
    |> map_defs (check_def thy unchecked overloaded axm)
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   261
    |> add_axiom axm
0bbf0d2348f9 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents: 35857
diff changeset
   262
  end;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   263
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   264
end;
3767
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   265
e2bb53d8dd26 moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents: 2979
diff changeset
   266
16443
82a116532e3e type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents: 16369
diff changeset
   267
(* add_finals(_i) *)
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   268
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   269
local
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   270
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   271
fun gen_add_finals prep_term overloaded args thy =
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   272
  let
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   273
    fun const_of (Const const) = const
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   274
      | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   275
      | const_of _ = error "Attempt to finalize non-constant term";
33701
9dd1079cec3a primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents: 33173
diff changeset
   276
    fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39133
diff changeset
   277
    val finalize = specify o tap (check_overloading thy overloaded) o const_of o
24708
d9b00117365e Syntax.parse/check/read;
wenzelm
parents: 24666
diff changeset
   278
      Sign.cert_term thy o prep_term thy;
17706
e534e39f3531 back to simple 'defs' (cf. revision 1.79);
wenzelm
parents: 17496
diff changeset
   279
  in thy |> map_defs (fold finalize args) end;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   280
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   281
in
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   282
29581
b3b33e0298eb binding is alias for Binding.T
haftmann
parents: 29092
diff changeset
   283
val add_finals_i = gen_add_finals (K I);
24708
d9b00117365e Syntax.parse/check/read;
wenzelm
parents: 24666
diff changeset
   284
val add_finals = gen_add_finals Syntax.read_term_global;
16291
ea4e64b2f25a renamed const_deps to defs;
wenzelm
parents: 16198
diff changeset
   285
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   286
end;
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 14204
diff changeset
   287
1526
6be6ea6f8b5d New file of just the theory primitives
paulson
parents:
diff changeset
   288
end;