Added support for making constants final, that is, ensuring that no
authorskalberg
Thu Oct 09 18:13:32 2003 +0200 (2003-10-09)
changeset 142230ee05eef881b
parent 14222 1e61f23fd359
child 14224 442c097c1437
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).
etc/isar-keywords.el
src/HOL/HOL.ML
src/HOL/HOL.thy
src/HOL/HOL_lemmas.ML
src/HOL/Tools/specification_package.ML
src/Pure/Isar/isar_syn.ML
src/Pure/display.ML
src/Pure/pure_thy.ML
src/Pure/theory.ML
     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