Added support for making constants final, that is, ensuring that no
definition can be given later (useful for constants whose behaviour is
fixed axiomatically rather than definitionally).

--- a/etc/isar-keywords.el	Wed Oct 08 16:02:54 2003 +0200
+++ b/etc/isar-keywords.el	Thu Oct 09 18:13:32 2003 +0200
@@ -24,6 +24,7 @@
     "arities"
     "assume"
     "automaton"
+    "ax_specification"
     "axclass"
     "axioms"
     "back"
@@ -57,6 +58,7 @@
     "exit"
     "extract"
     "extract_type"
+    "finalconsts"
     "finally"
     "fix"
     "from"
@@ -331,6 +333,7 @@
     "domain"
     "extract"
     "extract_type"
+    "finalconsts"
     "generate_code"
     "global"
     "hide"
@@ -370,7 +373,8 @@
     "inductive_cases"))
 
 (defconst isar-keywords-theory-goal
-  '("corollary"
+  '("ax_specification"
+    "corollary"
     "instance"
     "lemma"
     "recdef_tc"

--- a/src/HOL/HOL.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/HOL/HOL.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -79,7 +79,6 @@
   val True_or_False = True_or_False;
   val Let_def = Let_def;
   val if_def = if_def;
-  val arbitrary_def = arbitrary_def;
 end;
 
 open HOL;

--- a/src/HOL/HOL.thy	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 09 18:13:32 2003 +0200
@@ -146,10 +146,11 @@
   Let_def:      "Let s f == f(s)"
   if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
-  arbitrary_def:  "False ==> arbitrary == (THE x. False)"
-    -- {* @{term arbitrary} is completely unspecified, but is made to appear as a
-    definition syntactically *}
-
+finalconsts
+  "op ="
+  "op -->"
+  The
+  arbitrary
 
 subsubsection {* Generic algebraic operations *}
 

--- a/src/HOL/HOL_lemmas.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/HOL/HOL_lemmas.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -29,7 +29,6 @@
 val True_or_False = thm "True_or_False";
 val Let_def = thm "Let_def";
 val if_def = thm "if_def";
-val arbitrary_def = thm "arbitrary_def";
 
 
 section "Equality";

--- a/src/HOL/Tools/specification_package.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/HOL/Tools/specification_package.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -72,9 +72,7 @@
 				       then Thm.def_name (Sign.base_name cname)
 				       else thname
 			val co = Const(cname_full,ctype)
-			val def = Logic.mk_implies(HOLogic.mk_Trueprop HOLogic.false_const,
-						   Logic.mk_equals (co,choice_const ctype $ P))
-			val (thy',_) = PureThy.add_defs_i covld [((cdefname,def),[])] thy
+			val thy' = Theory.add_finals_i covld [co] thy
 			val tm' = case P of
 				      Abs(_, _, bodt) => subst_bound (co, bodt)
 				    | _ => P $ co

--- a/src/Pure/Isar/isar_syn.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -131,6 +131,12 @@
   OuterSyntax.command "consts" "declare constants" K.thy_decl
     (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
 
+val opt_overloaded =
+  Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
+
+val finalconstsP =
+  OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
+    (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
 
 val mode_spec =
   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
@@ -167,9 +173,6 @@
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
     (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
 
-val opt_overloaded =
-  Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
-
 val defsP =
   OuterSyntax.command "defs" "define constants" K.thy_decl
     (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
@@ -740,12 +743,12 @@
   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   (*theory sections*)
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
-  aritiesP, judgmentP, constsP, syntaxP, translationsP, axiomsP,
-  defsP, constdefsP, theoremsP, lemmasP, declareP, globalP, localP,
-  hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP,
-  parse_ast_translationP, parse_translationP, print_translationP,
-  typed_print_translationP, print_ast_translationP,
-  token_translationP, oracleP, localeP,
+  aritiesP, judgmentP, constsP, finalconstsP, syntaxP, translationsP,
+  axiomsP, defsP, constdefsP, theoremsP, lemmasP, declareP, globalP,
+  localP, hideP, useP, mlP, ml_commandP, ml_setupP, setupP,
+  method_setupP, parse_ast_translationP, parse_translationP,
+  print_translationP, typed_print_translationP,
+  print_ast_translationP, token_translationP, oracleP, localeP,
   (*proof commands*)
   theoremP, lemmaP, corollaryP, showP, haveP, thusP, henceP, fixP,
   assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP,

--- a/src/Pure/display.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/Pure/display.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -213,6 +213,11 @@
 
     fun pretty_arities (t, ars) = map (prt_arity t) ars;
 
+    fun pretty_final (c:string, tys:typ list) = Pretty.block
+      ([Pretty.str c, Pretty.str " ::", Pretty.brk 1] @
+         (if null tys then [Pretty.str "<all instances>"]
+	  else Pretty.commas (map prt_typ_no_tvars tys)));
+
     fun pretty_const (c, ty) = Pretty.block
       [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
 
@@ -224,6 +229,7 @@
     val spaces' = Library.sort_wrt fst spaces;
     val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
       Type.rep_tsig tsig;
+    val finals = Symtab.dest (#final_consts (rep_theory thy));
     val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
     val consts = Sign.cond_extern_table sg Sign.constK const_tab;
     val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
@@ -242,6 +248,7 @@
       Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
       Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
       Pretty.big_list "consts:" (map pretty_const consts),
+      Pretty.big_list "finals:" (map pretty_final finals),
       Pretty.big_list "axioms:" (map prt_axm axms),
       Pretty.strs ("oracles:" :: (map #1 oras))]
   end;

--- a/src/Pure/pure_thy.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/Pure/pure_thy.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -547,6 +547,11 @@
     ("Goal", "prop => prop", NoSyn),
     ("TYPE", "'a itself", NoSyn),
     (Term.dummy_patternN, "'a", Delimfix "'_")]
+  |> Theory.add_finals_i false
+    [Const("==",[TFree("'a",[]),TFree("'a",[])]--->propT),
+     Const("==>",[propT,propT]--->propT),
+     Const("all",(TFree("'a",logicS)-->propT)-->propT),
+     Const("TYPE",a_itselfT)]
   |> Theory.add_modesyntax ("", false)
     (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   |> Theory.add_trfuns Syntax.pure_trfuns

--- a/src/Pure/theory.ML	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/Pure/theory.ML	Thu Oct 09 18:13:32 2003 +0200
@@ -13,6 +13,7 @@
   val rep_theory: theory ->
     {sign: Sign.sg,
       const_deps: unit Graph.T,
+      final_consts: typ list Symtab.table,
       axioms: term Symtab.table,
       oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
       parents: theory list,
@@ -73,6 +74,8 @@
   val add_axioms: (bstring * string) list -> theory -> theory
   val add_axioms_i: (bstring * term) list -> theory -> theory
   val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
+  val add_finals: bool -> string list -> theory -> theory
+  val add_finals_i: bool -> term list -> theory -> theory
   val add_defs: bool -> (bstring * string) list -> theory -> theory
   val add_defs_i: bool -> (bstring * term) list -> theory -> theory
   val add_path: string -> theory -> theory
@@ -116,14 +119,15 @@
   Theory of {
     sign: Sign.sg,
     const_deps: unit Graph.T,
+    final_consts: typ list Symtab.table,
     axioms: term Symtab.table,
     oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
     parents: theory list,
     ancestors: theory list};
 
-fun make_theory sign const_deps axioms oracles parents ancestors =
-  Theory {sign = sign, const_deps = const_deps, axioms = axioms, oracles = oracles,
-    parents = parents, ancestors = ancestors};
+fun make_theory sign const_deps final_consts axioms oracles parents ancestors =
+  Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms,
+    oracles = oracles,  parents = parents, ancestors = ancestors};
 
 fun rep_theory (Theory args) = args;
 
@@ -151,7 +155,7 @@
 
 (*partial Pure theory*)
 val pre_pure =
-  make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty [] [];
+  make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty Symtab.empty [] [];
 
 
 
@@ -172,7 +176,7 @@
 
 fun ext_theory thy ext_sg ext_deps new_axms new_oras =
   let
-    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
+    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
     val draft = Sign.is_draft sign;
     val axioms' =
       Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
@@ -183,7 +187,7 @@
     val (parents', ancestors') =
       if draft then (parents, ancestors) else ([thy], thy :: ancestors);
   in
-    make_theory (ext_sg sign) (ext_deps const_deps) axioms' oracles' parents' ancestors'
+    make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors'
   end;
 
 
@@ -386,9 +390,14 @@
   let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G
   in foldl declare (deps, c :: cs) |> Graph.add_deps_acyclic (c, cs) end;
 
+fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
+  let
+    fun is_final (c, ty) =
+      case Symtab.lookup(final_consts,c) of
+        Some [] => true
+      | Some tys => exists (curry (Sign.typ_instance sg) ty) tys
+      | None => false;
 
-fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
-  let
     fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
       Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
 
@@ -410,6 +419,11 @@
     if not (null clashed) then
       err_in_defn sg name (Pretty.string_of (Pretty.chunks
         (def_txt (c_ty, " clashes with") :: map (show_defn c) clashed)))
+    else if is_final c_ty then
+      err_in_defn sg name (Pretty.string_of (Pretty.block
+        ([Pretty.str "The constant",Pretty.brk 1] @
+	 pretty_const c_ty @
+	 [Pretty.brk 1,Pretty.str "has been declared final"])))
     else
       (case overloading sg c_decl ty of
         NoOverloading =>
@@ -432,13 +446,13 @@
 
 fun ext_defns prep_axm overloaded raw_axms thy =
   let
-    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
+    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
     val all_axioms = flat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
 
     val axms = map (prep_axm sign) raw_axms;
-    val (const_deps', _) = foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
+    val (const_deps', _) = foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms);
   in
-    make_theory sign const_deps' axioms oracles parents ancestors
+    make_theory sign const_deps' final_consts axioms oracles parents ancestors
     |> add_axioms_i axms
   end;
 
@@ -446,6 +460,66 @@
 val add_defs = ext_defns read_axm;
 
 
+(* add_finals *)
+
+fun ext_finals prep_term overloaded raw_terms thy =
+  let
+    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
+    fun mk_final (finals,tm) =
+      let
+        fun err msg = raise TERM(msg,[tm]);
+        val (c,ty) = dest_Const tm
+          handle TERM _ => err "Can only make constants final";
+        val c_decl =
+          (case Sign.const_type sign c of Some T => T
+          | None => err ("Undeclared constant " ^ quote c));
+        val simple =
+	  case overloading sign c_decl ty of
+	    NoOverloading => true
+	  | Useless => err "Sort restrictions too strong"
+	  | Plain => if overloaded then false
+		     else err "Type is more general than declared";
+        val typ_instance = Sign.typ_instance sign;
+      in
+        if simple then
+	  (case Symtab.lookup(finals,c) of
+	    Some [] => err "Constant already final"
+	  | _ => Symtab.update((c,[]),finals))
+	else
+	  (case Symtab.lookup(finals,c) of
+	    Some [] => err "Constant already completely final"
+          | Some tys => if exists (curry typ_instance ty) tys
+			then err "Instance of constant is already final"
+			else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals)
+	  | None => Symtab.update((c,[ty]),finals))
+      end;
+    val consts = map (prep_term sign) raw_terms;
+    val final_consts' = foldl mk_final (final_consts,consts);
+  in
+    make_theory sign const_deps final_consts' axioms oracles parents ancestors
+  end;
+
+local
+  fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
+  val cert_term = #1 oo Sign.certify_term;
+in
+val add_finals = ext_finals read_term;
+val add_finals_i = ext_finals cert_term;
+end;
+
+fun merge_final sg =
+  let
+    fun merge_single (tys,ty) =
+      if exists (curry (Sign.typ_instance sg) ty) tys
+      then tys
+      else (ty::gen_rem (Sign.typ_instance sg) (tys,ty));
+    fun merge ([],_) = []
+      | merge (_,[]) = []
+      | merge input = foldl merge_single input;
+  in
+    Some o merge
+  end;
+
 
 (** additional theory data **)
 
@@ -478,6 +552,9 @@
       val deps' = foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
         handle Graph.CYCLES namess => error (cycle_msg namess);
 
+      val final_constss = map (#final_consts o rep_theory) thys;
+      val final_consts' = foldl (Symtab.join (merge_final sign')) (hd final_constss,
+								   tl final_constss);
       val axioms' = Symtab.empty;
 
       fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
@@ -490,7 +567,7 @@
       val ancestors' =
         gen_distinct eq_thy (parents' @ flat (map ancestors_of thys));
     in
-      make_theory sign' deps' axioms' oracles' parents' ancestors'
+      make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
     end;