eliminated global/local names;
authorwenzelm
Tue Jan 12 15:17:37 1999 +0100 (1999-01-12)
changeset 609387bf8c03b169
parent 6092 d9db67970c73
child 6094 fd0f737b1956
eliminated global/local names;
src/ZF/Fixedpt.thy
src/ZF/Inductive.ML
src/ZF/OrdQuant.ML
src/ZF/OrdQuant.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Univ.thy
src/ZF/ind_syntax.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/ZF/Fixedpt.thy	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/Fixedpt.thy	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -8,14 +8,10 @@
     1.4  
     1.5  Fixedpt = domrange +
     1.6  
     1.7 -global
     1.8 -
     1.9  consts
    1.10    bnd_mono    :: [i,i=>i]=>o
    1.11    lfp, gfp    :: [i,i=>i]=>i
    1.12  
    1.13 -local
    1.14 -
    1.15  defs
    1.16    (*monotone operator from Pow(D) to itself*)
    1.17    bnd_mono_def 
     2.1 --- a/src/ZF/Inductive.ML	Tue Jan 12 13:54:51 1999 +0100
     2.2 +++ b/src/ZF/Inductive.ML	Tue Jan 12 15:17:37 1999 +0100
     2.3 @@ -17,8 +17,8 @@
     2.4  
     2.5  structure Lfp =
     2.6    struct
     2.7 -  val oper      = Const("lfp",      [iT,iT-->iT]--->iT)
     2.8 -  val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
     2.9 +  val oper      = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT)
    2.10 +  val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
    2.11    val bnd_monoI = bnd_monoI
    2.12    val subs      = def_lfp_subset
    2.13    val Tarski    = def_lfp_Tarski
    2.14 @@ -64,8 +64,8 @@
    2.15  
    2.16  structure Gfp =
    2.17    struct
    2.18 -  val oper      = Const("gfp",      [iT,iT-->iT]--->iT)
    2.19 -  val bnd_mono  = Const("bnd_mono", [iT,iT-->iT]--->oT)
    2.20 +  val oper      = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT)
    2.21 +  val bnd_mono  = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
    2.22    val bnd_monoI = bnd_monoI
    2.23    val subs      = def_gfp_subset
    2.24    val Tarski    = def_gfp_Tarski
    2.25 @@ -74,9 +74,9 @@
    2.26  
    2.27  structure Quine_Prod =
    2.28    struct
    2.29 -  val sigma     = Const("QSigma", [iT, iT-->iT]--->iT)
    2.30 -  val pair      = Const("QPair", [iT,iT]--->iT)
    2.31 -  val split_name = "qsplit"
    2.32 +  val sigma     = Const("QPair.QSigma", [iT, iT-->iT]--->iT)
    2.33 +  val pair      = Const("QPair.QPair", [iT,iT]--->iT)
    2.34 +  val split_name = "QPair.qsplit"
    2.35    val pair_iff  = QPair_iff
    2.36    val split_eq  = qsplit
    2.37    val fsplitI   = qsplitI
    2.38 @@ -88,10 +88,10 @@
    2.39  
    2.40  structure Quine_Sum =
    2.41    struct
    2.42 -  val sum       = Const("op <+>", [iT,iT]--->iT)
    2.43 -  val inl       = Const("QInl", iT-->iT)
    2.44 -  val inr       = Const("QInr", iT-->iT)
    2.45 -  val elim      = Const("qcase", [iT-->iT, iT-->iT, iT]--->iT)
    2.46 +  val sum       = Const("QPair.op <+>", [iT,iT]--->iT)
    2.47 +  val inl       = Const("QPair.QInl", iT-->iT)
    2.48 +  val inr       = Const("QPair.QInr", iT-->iT)
    2.49 +  val elim      = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT)
    2.50    val case_inl  = qcase_QInl
    2.51    val case_inr  = qcase_QInr
    2.52    val inl_iff   = QInl_iff
     3.1 --- a/src/ZF/OrdQuant.ML	Tue Jan 12 13:54:51 1999 +0100
     3.2 +++ b/src/ZF/OrdQuant.ML	Tue Jan 12 15:17:37 1999 +0100
     3.3 @@ -95,7 +95,7 @@
     3.4  AddSEs [oexE, OUN_E];
     3.5  AddEs  [rev_oallE];
     3.6  
     3.7 -val Ord_atomize = atomize (("oall", [ospec])::ZF_conn_pairs, 
     3.8 +val Ord_atomize = atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, 
     3.9                             ZF_mem_pairs);
    3.10  
    3.11  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all)
     4.1 --- a/src/ZF/OrdQuant.thy	Tue Jan 12 13:54:51 1999 +0100
     4.2 +++ b/src/ZF/OrdQuant.thy	Tue Jan 12 15:17:37 1999 +0100
     4.3 @@ -7,8 +7,6 @@
     4.4  
     4.5  OrdQuant = Ordinal +
     4.6  
     4.7 -global
     4.8 -
     4.9  consts
    4.10    
    4.11    (* Ordinal Quantifiers *)
    4.12 @@ -32,8 +30,6 @@
    4.13    "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
    4.14    "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    4.15  
    4.16 -local
    4.17 -
    4.18  defs
    4.19    
    4.20    (* Ordinal Quantifiers *)
     5.1 --- a/src/ZF/QPair.thy	Tue Jan 12 13:54:51 1999 +0100
     5.2 +++ b/src/ZF/QPair.thy	Tue Jan 12 15:17:37 1999 +0100
     5.3 @@ -13,8 +13,6 @@
     5.4  
     5.5  QPair = Sum +
     5.6  
     5.7 -global
     5.8 -
     5.9  consts
    5.10    QPair     :: [i, i] => i                      ("<(_;/ _)>")
    5.11    qfst,qsnd :: i => i
    5.12 @@ -34,7 +32,6 @@
    5.13    "QSUM x:A. B"  => "QSigma(A, %x. B)"
    5.14    "A <*> B"      => "QSigma(A, _K(B))"
    5.15  
    5.16 -local
    5.17  
    5.18  defs
    5.19    QPair_def       "<a;b> == a+b"
     6.1 --- a/src/ZF/QUniv.thy	Tue Jan 12 13:54:51 1999 +0100
     6.2 +++ b/src/ZF/QUniv.thy	Tue Jan 12 15:17:37 1999 +0100
     6.3 @@ -1,21 +1,15 @@
     6.4 -(*  Title:      ZF/univ.thy
     6.5 +(*  Title:      ZF/QUniv.thy
     6.6      ID:         $Id$
     6.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.8      Copyright   1993  University of Cambridge
     6.9  
    6.10 -A small universe for lazy recursive types
    6.11 +A small universe for lazy recursive types.
    6.12  *)
    6.13  
    6.14  QUniv = Univ + QPair + mono + equalities +
    6.15  
    6.16 -global
    6.17 -
    6.18 -consts
    6.19 -    quniv        :: i=>i
    6.20 -
    6.21 -local
    6.22 -
    6.23 -defs
    6.24 -    quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
    6.25 +constdefs
    6.26 +  quniv :: i => i
    6.27 +  "quniv(A) == Pow(univ(eclose(A)))"
    6.28  
    6.29  end
     7.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Jan 12 13:54:51 1999 +0100
     7.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Jan 12 15:17:37 1999 +0100
     7.3 @@ -80,7 +80,7 @@
     7.4    val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists)
     7.5  
     7.6    val dummy =	
     7.7 -	writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype" 
     7.8 +	writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype" 
     7.9  		  else "Codatatype")
    7.10  		 ^ " definition " ^ big_rec_name)
    7.11  
    7.12 @@ -239,7 +239,7 @@
    7.13    (* Build the new theory *)
    7.14  
    7.15    val need_recursor = 
    7.16 -      (#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ);
    7.17 +      (#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ);
    7.18  
    7.19    fun add_recursor thy = 
    7.20        if need_recursor then
    7.21 @@ -415,7 +415,7 @@
    7.22        val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
    7.23        val dom_sum = 
    7.24            if sdom = "" then
    7.25 -	      Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms
    7.26 +	      Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "Fixedpt.lfp") rec_tms
    7.27            else readtm sign Ind_Syntax.iT sdom
    7.28        and con_ty_lists	= Ind_Syntax.read_constructs sign scon_ty_lists
    7.29    in 
     8.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jan 12 13:54:51 1999 +0100
     8.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jan 12 15:17:37 1999 +0100
     8.3 @@ -141,7 +141,7 @@
     8.4    
     8.5    val dummy =
     8.6        if verbose then
     8.7 -	  writeln ((if #1 (dest_Const Fp.oper) = "lfp" then "Inductive" 
     8.8 +	  writeln ((if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then "Inductive" 
     8.9  		    else "Coinductive") ^ " definition " ^ big_rec_name)
    8.10        else ();
    8.11  
    8.12 @@ -528,7 +528,7 @@
    8.13    val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
    8.14  
    8.15    val (thy2, induct, mutual_induct) = 
    8.16 -      if #1 (dest_Const Fp.oper) = "lfp" then induction_rules raw_induct thy1
    8.17 +      if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then induction_rules raw_induct thy1
    8.18        else (thy1, raw_induct, TrueI)
    8.19    and defs = big_rec_def :: part_rec_defs
    8.20  
     9.1 --- a/src/ZF/Univ.thy	Tue Jan 12 13:54:51 1999 +0100
     9.2 +++ b/src/ZF/Univ.thy	Tue Jan 12 15:17:37 1999 +0100
     9.3 @@ -8,13 +8,11 @@
     9.4  Standard notation for Vset(i) is V(i), but users might want V for a variable
     9.5  
     9.6  NOTE: univ(A) could be a translation; would simplify many proofs!
     9.7 -  But Ind_Syntax.univ refers to the constant "univ"
     9.8 +  But Ind_Syntax.univ refers to the constant "Univ.univ"
     9.9  *)
    9.10  
    9.11  Univ = Arith + Sum + Finite + mono +
    9.12  
    9.13 -global
    9.14 -
    9.15  consts
    9.16      Vfrom       :: [i,i]=>i
    9.17      Vset        :: i=>i
    9.18 @@ -25,7 +23,6 @@
    9.19  translations
    9.20      "Vset(x)"   ==      "Vfrom(0,x)"
    9.21  
    9.22 -local
    9.23  
    9.24  defs
    9.25      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
    10.1 --- a/src/ZF/ind_syntax.ML	Tue Jan 12 13:54:51 1999 +0100
    10.2 +++ b/src/ZF/ind_syntax.ML	Tue Jan 12 15:17:37 1999 +0100
    10.3 @@ -35,7 +35,7 @@
    10.4  
    10.5  val apply_const = Const("op `", [iT,iT]--->iT);
    10.6  
    10.7 -val Vrecursor_const = Const("Vrecursor", [[iT,iT]--->iT, iT]--->iT);
    10.8 +val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
    10.9  
   10.10  val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
   10.11  fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
   10.12 @@ -103,8 +103,8 @@
   10.13  
   10.14  val Un          = Const("op Un", [iT,iT]--->iT)
   10.15  and empty       = Const("0", iT)
   10.16 -and univ        = Const("univ", iT-->iT)
   10.17 -and quniv       = Const("quniv", iT-->iT);
   10.18 +and univ        = Const("Univ.univ", iT-->iT)
   10.19 +and quniv       = Const("QUniv.quniv", iT-->iT);
   10.20  
   10.21  (*Make a datatype's domain: form the union of its set parameters*)
   10.22  fun union_params rec_tm =
    11.1 --- a/src/ZF/thy_syntax.ML	Tue Jan 12 13:54:51 1999 +0100
    11.2 +++ b/src/ZF/thy_syntax.ML	Tue Jan 12 15:17:37 1999 +0100
    11.3 @@ -14,7 +14,7 @@
    11.4  
    11.5  (*ML identifiers for introduction rules.*)
    11.6  fun mk_intr_name suffix s =  
    11.7 -    if Syntax.is_identifier s then
    11.8 +    if ThmDatabase.is_ml_identifier s then
    11.9  	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
   11.10      else "_";               (*bad name, don't try to bind*)
   11.11