--- a/NEWS Mon Dec 20 15:24:25 2010 +0100
+++ b/NEWS Mon Dec 20 16:44:33 2010 +0100
@@ -603,7 +603,9 @@
*** FOL and ZF ***
-* All constant names are now qualified. INCOMPATIBILITY.
+* All constant names are now qualified internally and use proper
+identifiers, e.g. "IFOL.eq" instead of "op =". INCOMPATIBILITY.
+
*** ML ***
--- a/src/CTT/CTT.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/CTT/CTT.thy Mon Dec 20 16:44:33 2010 +0100
@@ -54,7 +54,7 @@
lambda :: "(i => i) => i" (binder "lam " 10)
app :: "[i,i]=>i" (infixl "`" 60)
(*Natural numbers*)
- "0" :: "i" ("0")
+ Zero :: "i" ("0")
(*Pairing*)
pair :: "[i,i]=>i" ("(1<_,/_>)")
--- a/src/FOL/FOL.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/FOL.thy Mon Dec 20 16:44:33 2010 +0100
@@ -175,7 +175,7 @@
(
val thy = @{theory}
type claset = Cla.claset
- val equality_name = @{const_name "op ="}
+ val equality_name = @{const_name eq}
val not_name = @{const_name Not}
val notE = @{thm notE}
val ccontr = @{thm ccontr}
@@ -391,4 +391,7 @@
setup Induct.setup
declare case_split [cases type: o]
+
+hide_const (open) eq
+
end
--- a/src/FOL/IFOL.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/IFOL.thy Mon Dec 20 16:44:33 2010 +0100
@@ -42,13 +42,13 @@
(* Connectives *)
- "op =" :: "['a, 'a] => o" (infixl "=" 50)
+ eq :: "['a, 'a] => o" (infixl "=" 50)
Not :: "o => o" ("~ _" [40] 40)
- "op &" :: "[o, o] => o" (infixr "&" 35)
- "op |" :: "[o, o] => o" (infixr "|" 30)
- "op -->" :: "[o, o] => o" (infixr "-->" 25)
- "op <->" :: "[o, o] => o" (infixr "<->" 25)
+ conj :: "[o, o] => o" (infixr "&" 35)
+ disj :: "[o, o] => o" (infixr "|" 30)
+ imp :: "[o, o] => o" (infixr "-->" 25)
+ iff :: "[o, o] => o" (infixr "<->" 25)
(* Quantifiers *)
@@ -69,28 +69,24 @@
notation (xsymbols)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10) and
- "op -->" (infixr "\<longrightarrow>" 25) and
- "op <->" (infixr "\<longleftrightarrow>" 25)
+ imp (infixr "\<longrightarrow>" 25) and
+ iff (infixr "\<longleftrightarrow>" 25)
notation (HTML output)
Not ("\<not> _" [40] 40) and
- "op &" (infixr "\<and>" 35) and
- "op |" (infixr "\<or>" 30) and
+ conj (infixr "\<and>" 35) and
+ disj (infixr "\<or>" 30) and
All (binder "\<forall>" 10) and
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10)
finalconsts
- False All Ex
- "op ="
- "op &"
- "op |"
- "op -->"
+ False All Ex eq conj disj imp
axioms
--- a/src/FOL/ex/Nat.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/ex/Nat.thy Mon Dec 20 16:44:33 2010 +0100
@@ -13,7 +13,7 @@
arities nat :: "term"
consts
- 0 :: nat ("0")
+ Zero :: nat ("0")
Suc :: "nat => nat"
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/FOL/fologic.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/fologic.ML Mon Dec 20 16:44:33 2010 +0100
@@ -50,29 +50,29 @@
(* Logical constants *)
val not = Const (@{const_name Not}, oT --> oT);
-val conj = Const(@{const_name "op &"}, [oT,oT]--->oT);
-val disj = Const(@{const_name "op |"}, [oT,oT]--->oT);
-val imp = Const(@{const_name "op -->"}, [oT,oT]--->oT)
-val iff = Const(@{const_name "op <->"}, [oT,oT]--->oT);
+val conj = Const(@{const_name conj}, [oT,oT]--->oT);
+val disj = Const(@{const_name disj}, [oT,oT]--->oT);
+val imp = Const(@{const_name imp}, [oT,oT]--->oT)
+val iff = Const(@{const_name iff}, [oT,oT]--->oT);
fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2
and mk_imp (t1, t2) = imp $ t1 $ t2
and mk_iff (t1, t2) = iff $ t1 $ t2;
-fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B)
+fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
-fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B)
+fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
| dest_iff t = raise TERM ("dest_iff", [t]);
-fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT);
+fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
--- a/src/FOL/simpdata.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOL/simpdata.ML Mon Dec 20 16:44:33 2010 +0100
@@ -8,15 +8,15 @@
(*Make meta-equalities. The operator below is Trueprop*)
fun mk_meta_eq th = case concl_of th of
- _ $ (Const(@{const_name "op ="},_)$_$_) => th RS @{thm eq_reflection}
- | _ $ (Const(@{const_name "op <->"},_)$_$_) => th RS @{thm iff_reflection}
+ _ $ (Const(@{const_name eq},_)$_$_) => th RS @{thm eq_reflection}
+ | _ $ (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
| _ =>
error("conclusion must be a =-equality or <->");;
fun mk_eq th = case concl_of th of
Const("==",_)$_$_ => th
- | _ $ (Const(@{const_name "op ="},_)$_$_) => mk_meta_eq th
- | _ $ (Const(@{const_name "op <->"},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name eq},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name iff},_)$_$_) => mk_meta_eq th
| _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T};
@@ -32,7 +32,7 @@
error("Premises and conclusion of congruence rules must use =-equality or <->");
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]), (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name imp}, [@{thm mp}]), (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])];
fun mk_atomize pairs =
@@ -55,11 +55,11 @@
structure Quantifier1 = Quantifier1Fun(
struct
(*abstract syntax*)
- fun dest_eq((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_eq((c as Const(@{const_name eq},_)) $ s $ t) = SOME(c,s,t)
| dest_eq _ = NONE;
- fun dest_conj((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_conj((c as Const(@{const_name conj},_)) $ s $ t) = SOME(c,s,t)
| dest_conj _ = NONE;
- fun dest_imp((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME(c,s,t)
+ fun dest_imp((c as Const(@{const_name imp},_)) $ s $ t) = SOME(c,s,t)
| dest_imp _ = NONE;
val conj = FOLogic.conj
val imp = FOLogic.imp
--- a/src/FOLP/IFOLP.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/IFOLP.thy Mon Dec 20 16:44:33 2010 +0100
@@ -24,14 +24,14 @@
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)
(*** Logical Connectives -- Type Formers ***)
- "op =" :: "['a,'a] => o" (infixl "=" 50)
+ eq :: "['a,'a] => o" (infixl "=" 50)
True :: "o"
False :: "o"
Not :: "o => o" ("~ _" [40] 40)
- "op &" :: "[o,o] => o" (infixr "&" 35)
- "op |" :: "[o,o] => o" (infixr "|" 30)
- "op -->" :: "[o,o] => o" (infixr "-->" 25)
- "op <->" :: "[o,o] => o" (infixr "<->" 25)
+ conj :: "[o,o] => o" (infixr "&" 35)
+ disj :: "[o,o] => o" (infixr "|" 30)
+ imp :: "[o,o] => o" (infixr "-->" 25)
+ iff :: "[o,o] => o" (infixr "<->" 25)
(*Quantifiers*)
All :: "('a => o) => o" (binder "ALL " 10)
Ex :: "('a => o) => o" (binder "EX " 10)
@@ -51,9 +51,9 @@
inr :: "p=>p"
when :: "[p, p=>p, p=>p]=>p"
lambda :: "(p => p) => p" (binder "lam " 55)
- "op `" :: "[p,p]=>p" (infixl "`" 60)
+ App :: "[p,p]=>p" (infixl "`" 60)
alll :: "['a=>p]=>p" (binder "all " 55)
- "op ^" :: "[p,'a]=>p" (infixl "^" 55)
+ app :: "[p,'a]=>p" (infixl "^" 55)
exists :: "['a,p]=>p" ("(1[_,/_])")
xsplit :: "[p,['a,p]=>p]=>p"
ideq :: "'a=>p"
@@ -595,7 +595,7 @@
struct
(*Take apart an equality judgement; otherwise raise Match!*)
fun dest_eq (Const (@{const_name Proof}, _) $
- (Const (@{const_name "op ="}, _) $ t $ u) $ _) = (t, u);
+ (Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u);
val imp_intr = @{thm impI}
--- a/src/FOLP/ex/Nat.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/ex/Nat.thy Mon Dec 20 16:44:33 2010 +0100
@@ -13,7 +13,7 @@
arities nat :: "term"
consts
- 0 :: nat ("0")
+ Zero :: nat ("0")
Suc :: "nat => nat"
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/FOLP/simpdata.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/simpdata.ML Mon Dec 20 16:44:33 2010 +0100
@@ -17,15 +17,15 @@
(* Conversion into rewrite rules *)
fun mk_eq th = case concl_of th of
- _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
+ _ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
+ | _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
| _ => make_iff_T th;
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name imp}, [@{thm mp}]),
+ (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name "All"}, [@{thm spec}]),
(@{const_name True}, []),
(@{const_name False}, [])];
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy Mon Dec 20 16:44:33 2010 +0100
@@ -13,7 +13,7 @@
consts
- "{|}" :: "'a multiset" ("{|}")
+ emptym :: "'a multiset" ("{|}")
addm :: "['a multiset, 'a] => 'a multiset"
delm :: "['a multiset, 'a] => 'a multiset"
countm :: "['a multiset, 'a => bool] => nat"
--- a/src/HOL/Prolog/Test.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/HOL/Prolog/Test.thy Mon Dec 20 16:44:33 2010 +0100
@@ -37,9 +37,9 @@
sue :: person
ned :: person
- "23" :: nat ("23")
- "24" :: nat ("24")
- "25" :: nat ("25")
+ nat23 :: nat ("23")
+ nat24 :: nat ("24")
+ nat25 :: nat ("25")
age :: "[person, nat] => bool"
--- a/src/LCF/LCF.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/LCF/LCF.thy Mon Dec 20 16:44:33 2010 +0100
@@ -18,13 +18,13 @@
typedecl tr
typedecl void
-typedecl ('a,'b) "*" (infixl "*" 6)
-typedecl ('a,'b) "+" (infixl "+" 5)
+typedecl ('a,'b) prod (infixl "*" 6)
+typedecl ('a,'b) sum (infixl "+" 5)
arities
"fun" :: (cpo, cpo) cpo
- "*" :: (cpo, cpo) cpo
- "+" :: (cpo, cpo) cpo
+ prod :: (cpo, cpo) cpo
+ sum :: (cpo, cpo) cpo
tr :: cpo
void :: cpo
--- a/src/Sequents/LK/Nat.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/Sequents/LK/Nat.thy Mon Dec 20 16:44:33 2010 +0100
@@ -11,7 +11,7 @@
typedecl nat
arities nat :: "term"
-consts "0" :: nat ("0")
+consts Zero :: nat ("0")
Suc :: "nat=>nat"
rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
add :: "[nat, nat] => nat" (infixl "+" 60)
--- a/src/ZF/Tools/datatype_package.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML Mon Dec 20 16:44:33 2010 +0100
@@ -91,7 +91,7 @@
(** Define the constructors **)
(*The empty tuple is 0*)
- fun mk_tuple [] = @{const "0"}
+ fun mk_tuple [] = @{const zero}
| mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
fun mk_inject n k u = Balanced_Tree.access
--- a/src/ZF/Tools/induct_tacs.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Dec 20 16:44:33 2010 +0100
@@ -118,7 +118,7 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
+ fun const_of (Const(@{const_name IFOL.eq}, _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);
--- a/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 16:44:33 2010 +0100
@@ -19,12 +19,12 @@
(* bits *)
-fun mk_bit 0 = Syntax.const @{const_syntax "0"}
- | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
+fun mk_bit 0 = Syntax.const @{const_syntax zero}
+ | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax zero}
| mk_bit _ = raise Fail "mk_bit";
-fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
- | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax zero}, _)) = 0
+ | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1
| dest_bit _ = raise Match;
--- a/src/ZF/Tools/primrec_package.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Dec 20 16:44:33 2010 +0100
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const (@{const_name 0}, Ind_Syntax.iT),
- #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
+ (Const (@{const_name zero}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name zero}, Ind_Syntax.iT)))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/ZF.thy Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/ZF.thy Mon Dec 20 16:44:33 2010 +0100
@@ -17,7 +17,7 @@
consts
- "0" :: "i" ("0") --{*the empty set*}
+ zero :: "i" ("0") --{*the empty set*}
Pow :: "i => i" --{*power sets*}
Inf :: "i" --{*infinite set*}
--- a/src/ZF/arith_data.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/arith_data.ML Mon Dec 20 16:44:33 2010 +0100
@@ -24,7 +24,7 @@
val iT = Ind_Syntax.iT;
-val zero = Const(@{const_name 0}, iT);
+val zero = Const(@{const_name zero}, iT);
val succ = Const(@{const_name succ}, iT --> iT);
fun mk_succ t = succ $ t;
val one = mk_succ zero;
@@ -44,7 +44,7 @@
(* dest_sum *)
-fun dest_sum (Const(@{const_name 0},_)) = []
+fun dest_sum (Const(@{const_name zero},_)) = []
| dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
| dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
| dest_sum tm = [tm];
--- a/src/ZF/ind_syntax.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/ind_syntax.ML Mon Dec 20 16:44:33 2010 +0100
@@ -29,7 +29,7 @@
fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
(*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
+fun chk_prem rec_hd (Const (@{const_name conj}, _) $ _ $ _) =
error"Premises may not be conjuctive"
| chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
@@ -96,7 +96,7 @@
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
in case filter is_ind (args @ cs) of
- [] => @{const 0}
+ [] => @{const zero}
| u_args => Balanced_Tree.make mk_Un u_args
end;
--- a/src/ZF/simpdata.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/simpdata.ML Mon Dec 20 16:44:33 2010 +0100
@@ -32,8 +32,8 @@
val ZF_conn_pairs =
[(@{const_name Ball}, [@{thm bspec}]),
(@{const_name All}, [@{thm spec}]),
- (@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
+ (@{const_name imp}, [@{thm mp}]),
+ (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}])];
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =