1.1 --- a/etc/isar-keywords.el Wed Oct 08 16:02:54 2003 +0200
1.2 +++ b/etc/isar-keywords.el Thu Oct 09 18:13:32 2003 +0200
1.3 @@ -24,6 +24,7 @@
1.4 "arities"
1.5 "assume"
1.6 "automaton"
1.7 + "ax_specification"
1.8 "axclass"
1.9 "axioms"
1.10 "back"
1.11 @@ -57,6 +58,7 @@
1.12 "exit"
1.13 "extract"
1.14 "extract_type"
1.15 + "finalconsts"
1.16 "finally"
1.17 "fix"
1.18 "from"
1.19 @@ -331,6 +333,7 @@
1.20 "domain"
1.21 "extract"
1.22 "extract_type"
1.23 + "finalconsts"
1.24 "generate_code"
1.25 "global"
1.26 "hide"
1.27 @@ -370,7 +373,8 @@
1.28 "inductive_cases"))
1.29
1.30 (defconst isar-keywords-theory-goal
1.31 - '("corollary"
1.32 + '("ax_specification"
1.33 + "corollary"
1.34 "instance"
1.35 "lemma"
1.36 "recdef_tc"
2.1 --- a/src/HOL/HOL.ML Wed Oct 08 16:02:54 2003 +0200
2.2 +++ b/src/HOL/HOL.ML Thu Oct 09 18:13:32 2003 +0200
2.3 @@ -79,7 +79,6 @@
2.4 val True_or_False = True_or_False;
2.5 val Let_def = Let_def;
2.6 val if_def = if_def;
2.7 - val arbitrary_def = arbitrary_def;
2.8 end;
2.9
2.10 open HOL;
3.1 --- a/src/HOL/HOL.thy Wed Oct 08 16:02:54 2003 +0200
3.2 +++ b/src/HOL/HOL.thy Thu Oct 09 18:13:32 2003 +0200
3.3 @@ -146,10 +146,11 @@
3.4 Let_def: "Let s f == f(s)"
3.5 if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
3.6
3.7 - arbitrary_def: "False ==> arbitrary == (THE x. False)"
3.8 - -- {* @{term arbitrary} is completely unspecified, but is made to appear as a
3.9 - definition syntactically *}
3.10 -
3.11 +finalconsts
3.12 + "op ="
3.13 + "op -->"
3.14 + The
3.15 + arbitrary
3.16
3.17 subsubsection {* Generic algebraic operations *}
3.18
4.1 --- a/src/HOL/HOL_lemmas.ML Wed Oct 08 16:02:54 2003 +0200
4.2 +++ b/src/HOL/HOL_lemmas.ML Thu Oct 09 18:13:32 2003 +0200
4.3 @@ -29,7 +29,6 @@
4.4 val True_or_False = thm "True_or_False";
4.5 val Let_def = thm "Let_def";
4.6 val if_def = thm "if_def";
4.7 -val arbitrary_def = thm "arbitrary_def";
4.8
4.9
4.10 section "Equality";
5.1 --- a/src/HOL/Tools/specification_package.ML Wed Oct 08 16:02:54 2003 +0200
5.2 +++ b/src/HOL/Tools/specification_package.ML Thu Oct 09 18:13:32 2003 +0200
5.3 @@ -72,9 +72,7 @@
5.4 then Thm.def_name (Sign.base_name cname)
5.5 else thname
5.6 val co = Const(cname_full,ctype)
5.7 - val def = Logic.mk_implies(HOLogic.mk_Trueprop HOLogic.false_const,
5.8 - Logic.mk_equals (co,choice_const ctype $ P))
5.9 - val (thy',_) = PureThy.add_defs_i covld [((cdefname,def),[])] thy
5.10 + val thy' = Theory.add_finals_i covld [co] thy
5.11 val tm' = case P of
5.12 Abs(_, _, bodt) => subst_bound (co, bodt)
5.13 | _ => P $ co
6.1 --- a/src/Pure/Isar/isar_syn.ML Wed Oct 08 16:02:54 2003 +0200
6.2 +++ b/src/Pure/Isar/isar_syn.ML Thu Oct 09 18:13:32 2003 +0200
6.3 @@ -131,6 +131,12 @@
6.4 OuterSyntax.command "consts" "declare constants" K.thy_decl
6.5 (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
6.6
6.7 +val opt_overloaded =
6.8 + Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
6.9 +
6.10 +val finalconstsP =
6.11 + OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
6.12 + (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
6.13
6.14 val mode_spec =
6.15 (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
6.16 @@ -167,9 +173,6 @@
6.17 OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
6.18 (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
6.19
6.20 -val opt_overloaded =
6.21 - Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
6.22 -
6.23 val defsP =
6.24 OuterSyntax.command "defs" "define constants" K.thy_decl
6.25 (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
6.26 @@ -740,12 +743,12 @@
6.27 text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
6.28 (*theory sections*)
6.29 classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
6.30 - aritiesP, judgmentP, constsP, syntaxP, translationsP, axiomsP,
6.31 - defsP, constdefsP, theoremsP, lemmasP, declareP, globalP, localP,
6.32 - hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP,
6.33 - parse_ast_translationP, parse_translationP, print_translationP,
6.34 - typed_print_translationP, print_ast_translationP,
6.35 - token_translationP, oracleP, localeP,
6.36 + aritiesP, judgmentP, constsP, finalconstsP, syntaxP, translationsP,
6.37 + axiomsP, defsP, constdefsP, theoremsP, lemmasP, declareP, globalP,
6.38 + localP, hideP, useP, mlP, ml_commandP, ml_setupP, setupP,
6.39 + method_setupP, parse_ast_translationP, parse_translationP,
6.40 + print_translationP, typed_print_translationP,
6.41 + print_ast_translationP, token_translationP, oracleP, localeP,
6.42 (*proof commands*)
6.43 theoremP, lemmaP, corollaryP, showP, haveP, thusP, henceP, fixP,
6.44 assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP,
7.1 --- a/src/Pure/display.ML Wed Oct 08 16:02:54 2003 +0200
7.2 +++ b/src/Pure/display.ML Thu Oct 09 18:13:32 2003 +0200
7.3 @@ -213,6 +213,11 @@
7.4
7.5 fun pretty_arities (t, ars) = map (prt_arity t) ars;
7.6
7.7 + fun pretty_final (c:string, tys:typ list) = Pretty.block
7.8 + ([Pretty.str c, Pretty.str " ::", Pretty.brk 1] @
7.9 + (if null tys then [Pretty.str "<all instances>"]
7.10 + else Pretty.commas (map prt_typ_no_tvars tys)));
7.11 +
7.12 fun pretty_const (c, ty) = Pretty.block
7.13 [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
7.14
7.15 @@ -224,6 +229,7 @@
7.16 val spaces' = Library.sort_wrt fst spaces;
7.17 val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
7.18 Type.rep_tsig tsig;
7.19 + val finals = Symtab.dest (#final_consts (rep_theory thy));
7.20 val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
7.21 val consts = Sign.cond_extern_table sg Sign.constK const_tab;
7.22 val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
7.23 @@ -242,6 +248,7 @@
7.24 Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
7.25 Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
7.26 Pretty.big_list "consts:" (map pretty_const consts),
7.27 + Pretty.big_list "finals:" (map pretty_final finals),
7.28 Pretty.big_list "axioms:" (map prt_axm axms),
7.29 Pretty.strs ("oracles:" :: (map #1 oras))]
7.30 end;
8.1 --- a/src/Pure/pure_thy.ML Wed Oct 08 16:02:54 2003 +0200
8.2 +++ b/src/Pure/pure_thy.ML Thu Oct 09 18:13:32 2003 +0200
8.3 @@ -547,6 +547,11 @@
8.4 ("Goal", "prop => prop", NoSyn),
8.5 ("TYPE", "'a itself", NoSyn),
8.6 (Term.dummy_patternN, "'a", Delimfix "'_")]
8.7 + |> Theory.add_finals_i false
8.8 + [Const("==",[TFree("'a",[]),TFree("'a",[])]--->propT),
8.9 + Const("==>",[propT,propT]--->propT),
8.10 + Const("all",(TFree("'a",logicS)-->propT)-->propT),
8.11 + Const("TYPE",a_itselfT)]
8.12 |> Theory.add_modesyntax ("", false)
8.13 (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
8.14 |> Theory.add_trfuns Syntax.pure_trfuns
9.1 --- a/src/Pure/theory.ML Wed Oct 08 16:02:54 2003 +0200
9.2 +++ b/src/Pure/theory.ML Thu Oct 09 18:13:32 2003 +0200
9.3 @@ -13,6 +13,7 @@
9.4 val rep_theory: theory ->
9.5 {sign: Sign.sg,
9.6 const_deps: unit Graph.T,
9.7 + final_consts: typ list Symtab.table,
9.8 axioms: term Symtab.table,
9.9 oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
9.10 parents: theory list,
9.11 @@ -73,6 +74,8 @@
9.12 val add_axioms: (bstring * string) list -> theory -> theory
9.13 val add_axioms_i: (bstring * term) list -> theory -> theory
9.14 val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
9.15 + val add_finals: bool -> string list -> theory -> theory
9.16 + val add_finals_i: bool -> term list -> theory -> theory
9.17 val add_defs: bool -> (bstring * string) list -> theory -> theory
9.18 val add_defs_i: bool -> (bstring * term) list -> theory -> theory
9.19 val add_path: string -> theory -> theory
9.20 @@ -116,14 +119,15 @@
9.21 Theory of {
9.22 sign: Sign.sg,
9.23 const_deps: unit Graph.T,
9.24 + final_consts: typ list Symtab.table,
9.25 axioms: term Symtab.table,
9.26 oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
9.27 parents: theory list,
9.28 ancestors: theory list};
9.29
9.30 -fun make_theory sign const_deps axioms oracles parents ancestors =
9.31 - Theory {sign = sign, const_deps = const_deps, axioms = axioms, oracles = oracles,
9.32 - parents = parents, ancestors = ancestors};
9.33 +fun make_theory sign const_deps final_consts axioms oracles parents ancestors =
9.34 + Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms,
9.35 + oracles = oracles, parents = parents, ancestors = ancestors};
9.36
9.37 fun rep_theory (Theory args) = args;
9.38
9.39 @@ -151,7 +155,7 @@
9.40
9.41 (*partial Pure theory*)
9.42 val pre_pure =
9.43 - make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty [] [];
9.44 + make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty Symtab.empty [] [];
9.45
9.46
9.47
9.48 @@ -172,7 +176,7 @@
9.49
9.50 fun ext_theory thy ext_sg ext_deps new_axms new_oras =
9.51 let
9.52 - val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
9.53 + val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
9.54 val draft = Sign.is_draft sign;
9.55 val axioms' =
9.56 Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
9.57 @@ -183,7 +187,7 @@
9.58 val (parents', ancestors') =
9.59 if draft then (parents, ancestors) else ([thy], thy :: ancestors);
9.60 in
9.61 - make_theory (ext_sg sign) (ext_deps const_deps) axioms' oracles' parents' ancestors'
9.62 + make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors'
9.63 end;
9.64
9.65
9.66 @@ -386,9 +390,14 @@
9.67 let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G
9.68 in foldl declare (deps, c :: cs) |> Graph.add_deps_acyclic (c, cs) end;
9.69
9.70 +fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
9.71 + let
9.72 + fun is_final (c, ty) =
9.73 + case Symtab.lookup(final_consts,c) of
9.74 + Some [] => true
9.75 + | Some tys => exists (curry (Sign.typ_instance sg) ty) tys
9.76 + | None => false;
9.77
9.78 -fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
9.79 - let
9.80 fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
9.81 Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
9.82
9.83 @@ -410,6 +419,11 @@
9.84 if not (null clashed) then
9.85 err_in_defn sg name (Pretty.string_of (Pretty.chunks
9.86 (def_txt (c_ty, " clashes with") :: map (show_defn c) clashed)))
9.87 + else if is_final c_ty then
9.88 + err_in_defn sg name (Pretty.string_of (Pretty.block
9.89 + ([Pretty.str "The constant",Pretty.brk 1] @
9.90 + pretty_const c_ty @
9.91 + [Pretty.brk 1,Pretty.str "has been declared final"])))
9.92 else
9.93 (case overloading sg c_decl ty of
9.94 NoOverloading =>
9.95 @@ -432,13 +446,13 @@
9.96
9.97 fun ext_defns prep_axm overloaded raw_axms thy =
9.98 let
9.99 - val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
9.100 + val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
9.101 val all_axioms = flat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
9.102
9.103 val axms = map (prep_axm sign) raw_axms;
9.104 - val (const_deps', _) = foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
9.105 + val (const_deps', _) = foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms);
9.106 in
9.107 - make_theory sign const_deps' axioms oracles parents ancestors
9.108 + make_theory sign const_deps' final_consts axioms oracles parents ancestors
9.109 |> add_axioms_i axms
9.110 end;
9.111
9.112 @@ -446,6 +460,66 @@
9.113 val add_defs = ext_defns read_axm;
9.114
9.115
9.116 +(* add_finals *)
9.117 +
9.118 +fun ext_finals prep_term overloaded raw_terms thy =
9.119 + let
9.120 + val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
9.121 + fun mk_final (finals,tm) =
9.122 + let
9.123 + fun err msg = raise TERM(msg,[tm]);
9.124 + val (c,ty) = dest_Const tm
9.125 + handle TERM _ => err "Can only make constants final";
9.126 + val c_decl =
9.127 + (case Sign.const_type sign c of Some T => T
9.128 + | None => err ("Undeclared constant " ^ quote c));
9.129 + val simple =
9.130 + case overloading sign c_decl ty of
9.131 + NoOverloading => true
9.132 + | Useless => err "Sort restrictions too strong"
9.133 + | Plain => if overloaded then false
9.134 + else err "Type is more general than declared";
9.135 + val typ_instance = Sign.typ_instance sign;
9.136 + in
9.137 + if simple then
9.138 + (case Symtab.lookup(finals,c) of
9.139 + Some [] => err "Constant already final"
9.140 + | _ => Symtab.update((c,[]),finals))
9.141 + else
9.142 + (case Symtab.lookup(finals,c) of
9.143 + Some [] => err "Constant already completely final"
9.144 + | Some tys => if exists (curry typ_instance ty) tys
9.145 + then err "Instance of constant is already final"
9.146 + else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals)
9.147 + | None => Symtab.update((c,[ty]),finals))
9.148 + end;
9.149 + val consts = map (prep_term sign) raw_terms;
9.150 + val final_consts' = foldl mk_final (final_consts,consts);
9.151 + in
9.152 + make_theory sign const_deps final_consts' axioms oracles parents ancestors
9.153 + end;
9.154 +
9.155 +local
9.156 + fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
9.157 + val cert_term = #1 oo Sign.certify_term;
9.158 +in
9.159 +val add_finals = ext_finals read_term;
9.160 +val add_finals_i = ext_finals cert_term;
9.161 +end;
9.162 +
9.163 +fun merge_final sg =
9.164 + let
9.165 + fun merge_single (tys,ty) =
9.166 + if exists (curry (Sign.typ_instance sg) ty) tys
9.167 + then tys
9.168 + else (ty::gen_rem (Sign.typ_instance sg) (tys,ty));
9.169 + fun merge ([],_) = []
9.170 + | merge (_,[]) = []
9.171 + | merge input = foldl merge_single input;
9.172 + in
9.173 + Some o merge
9.174 + end;
9.175 +
9.176
9.177 (** additional theory data **)
9.178
9.179 @@ -478,6 +552,9 @@
9.180 val deps' = foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
9.181 handle Graph.CYCLES namess => error (cycle_msg namess);
9.182
9.183 + val final_constss = map (#final_consts o rep_theory) thys;
9.184 + val final_consts' = foldl (Symtab.join (merge_final sign')) (hd final_constss,
9.185 + tl final_constss);
9.186 val axioms' = Symtab.empty;
9.187
9.188 fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
9.189 @@ -490,7 +567,7 @@
9.190 val ancestors' =
9.191 gen_distinct eq_thy (parents' @ flat (map ancestors_of thys));
9.192 in
9.193 - make_theory sign' deps' axioms' oracles' parents' ancestors'
9.194 + make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
9.195 end;
9.196
9.197