# HG changeset patch # User skalberg # Date 1065716012 -7200 # Node ID 0ee05eef881bc0d380c674bb8625270ed85dbb8b # Parent 1e61f23fd359eec1c0a3d67f3678f98d175f54a0 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). diff -r 1e61f23fd359 -r 0ee05eef881b etc/isar-keywords.el --- 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" diff -r 1e61f23fd359 -r 0ee05eef881b src/HOL/HOL.ML --- 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; diff -r 1e61f23fd359 -r 0ee05eef881b src/HOL/HOL.thy --- 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 *} diff -r 1e61f23fd359 -r 0ee05eef881b src/HOL/HOL_lemmas.ML --- 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"; diff -r 1e61f23fd359 -r 0ee05eef881b src/HOL/Tools/specification_package.ML --- 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 diff -r 1e61f23fd359 -r 0ee05eef881b src/Pure/Isar/isar_syn.ML --- 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, diff -r 1e61f23fd359 -r 0ee05eef881b src/Pure/display.ML --- 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 ""] + 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; diff -r 1e61f23fd359 -r 0ee05eef881b src/Pure/pure_thy.ML --- 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 diff -r 1e61f23fd359 -r 0ee05eef881b src/Pure/theory.ML --- 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;