# HG changeset patch # User wenzelm # Date 916150657 -3600 # Node ID 87bf8c03b16978cf4c6c75164cce7ee5d2b10f08 # Parent d9db67970c73bf0e42a9dde283f2a1333c0293fc eliminated global/local names; diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/Fixedpt.thy --- a/src/ZF/Fixedpt.thy Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/Fixedpt.thy Tue Jan 12 15:17:37 1999 +0100 @@ -8,14 +8,10 @@ Fixedpt = domrange + -global - consts bnd_mono :: [i,i=>i]=>o lfp, gfp :: [i,i=>i]=>i -local - defs (*monotone operator from Pow(D) to itself*) bnd_mono_def diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/Inductive.ML --- a/src/ZF/Inductive.ML Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/Inductive.ML Tue Jan 12 15:17:37 1999 +0100 @@ -17,8 +17,8 @@ structure Lfp = struct - val oper = Const("lfp", [iT,iT-->iT]--->iT) - val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) + val oper = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT) + val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT) val bnd_monoI = bnd_monoI val subs = def_lfp_subset val Tarski = def_lfp_Tarski @@ -64,8 +64,8 @@ structure Gfp = struct - val oper = Const("gfp", [iT,iT-->iT]--->iT) - val bnd_mono = Const("bnd_mono", [iT,iT-->iT]--->oT) + val oper = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT) + val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT) val bnd_monoI = bnd_monoI val subs = def_gfp_subset val Tarski = def_gfp_Tarski @@ -74,9 +74,9 @@ structure Quine_Prod = struct - val sigma = Const("QSigma", [iT, iT-->iT]--->iT) - val pair = Const("QPair", [iT,iT]--->iT) - val split_name = "qsplit" + val sigma = Const("QPair.QSigma", [iT, iT-->iT]--->iT) + val pair = Const("QPair.QPair", [iT,iT]--->iT) + val split_name = "QPair.qsplit" val pair_iff = QPair_iff val split_eq = qsplit val fsplitI = qsplitI @@ -88,10 +88,10 @@ structure Quine_Sum = struct - val sum = Const("op <+>", [iT,iT]--->iT) - val inl = Const("QInl", iT-->iT) - val inr = Const("QInr", iT-->iT) - val elim = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT) + val sum = Const("QPair.op <+>", [iT,iT]--->iT) + val inl = Const("QPair.QInl", iT-->iT) + val inr = Const("QPair.QInr", iT-->iT) + val elim = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT) val case_inl = qcase_QInl val case_inr = qcase_QInr val inl_iff = QInl_iff diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/OrdQuant.ML --- a/src/ZF/OrdQuant.ML Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/OrdQuant.ML Tue Jan 12 15:17:37 1999 +0100 @@ -95,7 +95,7 @@ AddSEs [oexE, OUN_E]; AddEs [rev_oallE]; -val Ord_atomize = atomize (("oall", [ospec])::ZF_conn_pairs, +val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs); simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all) diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/OrdQuant.thy Tue Jan 12 15:17:37 1999 +0100 @@ -7,8 +7,6 @@ OrdQuant = Ordinal + -global - consts (* Ordinal Quantifiers *) @@ -32,8 +30,6 @@ "@oex" :: [idt, i, o] => o ("(3\\ _<_./ _)" 10) "@OUNION" :: [idt, i, i] => i ("(3\\ _<_./ _)" 10) -local - defs (* Ordinal Quantifiers *) diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/QPair.thy Tue Jan 12 15:17:37 1999 +0100 @@ -13,8 +13,6 @@ QPair = Sum + -global - consts QPair :: [i, i] => i ("<(_;/ _)>") qfst,qsnd :: i => i @@ -34,7 +32,6 @@ "QSUM x:A. B" => "QSigma(A, %x. B)" "A <*> B" => "QSigma(A, _K(B))" -local defs QPair_def " == a+b" diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/QUniv.thy --- a/src/ZF/QUniv.thy Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/QUniv.thy Tue Jan 12 15:17:37 1999 +0100 @@ -1,21 +1,15 @@ -(* Title: ZF/univ.thy +(* Title: ZF/QUniv.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -A small universe for lazy recursive types +A small universe for lazy recursive types. *) QUniv = Univ + QPair + mono + equalities + -global - -consts - quniv :: i=>i - -local - -defs - quniv_def "quniv(A) == Pow(univ(eclose(A)))" +constdefs + quniv :: i => i + "quniv(A) == Pow(univ(eclose(A)))" end diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/Tools/datatype_package.ML Tue Jan 12 15:17:37 1999 +0100 @@ -80,7 +80,7 @@ val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists) val dummy = - writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype" + writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype" else "Codatatype") ^ " definition " ^ big_rec_name) @@ -239,7 +239,7 @@ (* Build the new theory *) val need_recursor = - (#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ); + (#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ); fun add_recursor thy = if need_recursor then @@ -415,7 +415,7 @@ val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms val dom_sum = if sdom = "" then - Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms + Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "Fixedpt.lfp") rec_tms else readtm sign Ind_Syntax.iT sdom and con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists in diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/Tools/inductive_package.ML Tue Jan 12 15:17:37 1999 +0100 @@ -141,7 +141,7 @@ val dummy = if verbose then - writeln ((if #1 (dest_Const Fp.oper) = "lfp" then "Inductive" + writeln ((if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then "Inductive" else "Coinductive") ^ " definition " ^ big_rec_name) else (); @@ -528,7 +528,7 @@ val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct) val (thy2, induct, mutual_induct) = - if #1 (dest_Const Fp.oper) = "lfp" then induction_rules raw_induct thy1 + if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then induction_rules raw_induct thy1 else (thy1, raw_induct, TrueI) and defs = big_rec_def :: part_rec_defs diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/Univ.thy --- a/src/ZF/Univ.thy Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/Univ.thy Tue Jan 12 15:17:37 1999 +0100 @@ -8,13 +8,11 @@ Standard notation for Vset(i) is V(i), but users might want V for a variable NOTE: univ(A) could be a translation; would simplify many proofs! - But Ind_Syntax.univ refers to the constant "univ" + But Ind_Syntax.univ refers to the constant "Univ.univ" *) Univ = Arith + Sum + Finite + mono + -global - consts Vfrom :: [i,i]=>i Vset :: i=>i @@ -25,7 +23,6 @@ translations "Vset(x)" == "Vfrom(0,x)" -local defs Vfrom_def "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))" diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/ind_syntax.ML Tue Jan 12 15:17:37 1999 +0100 @@ -35,7 +35,7 @@ val apply_const = Const("op `", [iT,iT]--->iT); -val Vrecursor_const = Const("Vrecursor", [[iT,iT]--->iT, iT]--->iT); +val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT); val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT); fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); @@ -103,8 +103,8 @@ val Un = Const("op Un", [iT,iT]--->iT) and empty = Const("0", iT) -and univ = Const("univ", iT-->iT) -and quniv = Const("quniv", iT-->iT); +and univ = Const("Univ.univ", iT-->iT) +and quniv = Const("QUniv.quniv", iT-->iT); (*Make a datatype's domain: form the union of its set parameters*) fun union_params rec_tm = diff -r d9db67970c73 -r 87bf8c03b169 src/ZF/thy_syntax.ML --- a/src/ZF/thy_syntax.ML Tue Jan 12 13:54:51 1999 +0100 +++ b/src/ZF/thy_syntax.ML Tue Jan 12 15:17:37 1999 +0100 @@ -14,7 +14,7 @@ (*ML identifiers for introduction rules.*) fun mk_intr_name suffix s = - if Syntax.is_identifier s then + if ThmDatabase.is_ml_identifier s then "op " ^ s ^ suffix (*the "op" cancels any infix status*) else "_"; (*bad name, don't try to bind*)