--- a/NEWS Tue Jun 01 11:25:26 2004 +0200
+++ b/NEWS Tue Jun 01 12:33:50 2004 +0200
@@ -32,6 +32,11 @@
instead of 'nonterminals'/'syntax'. Some very exotic syntax
specifications may require further adaption (e.g. Cube/Base.thy).
+* Pure: removed obsolete type class "logic", use the top sort {}
+ instead. Note that non-logical types should be declared as
+ 'nonterminals' rather than 'types'. INCOMPATIBILITY for new
+ object-logic specifications.
+
* Pure/Syntax: inner syntax includes (*(*nested*) comments*).
* Pure/Syntax: pretty pinter now supports unbreakable blocks,
--- a/src/CTT/CTT.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/CTT/CTT.thy Tue Jun 01 12:33:50 2004 +0200
@@ -13,9 +13,6 @@
t
o
-arities
- i,t,o :: logic
-
consts
(*Types*)
F,T :: "t" (*F is empty, T contains one element*)
--- a/src/Cube/Base.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Cube/Base.thy Tue Jun 01 12:33:50 2004 +0200
@@ -10,8 +10,6 @@
types
term
-arities
- term :: logic
types
context typing
--- a/src/FOL/IFOL.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/FOL/IFOL.thy Tue Jun 01 12:33:50 2004 +0200
@@ -13,7 +13,7 @@
global
-classes "term" < logic
+classes "term"
defaultsort "term"
typedecl o
@@ -264,7 +264,7 @@
nonterminals letbinds letbind
constdefs
- Let :: "['a::logic, 'a => 'b] => ('b::logic)"
+ Let :: "['a::{}, 'a => 'b] => ('b::{})"
"Let(s, f) == f(s)"
syntax
--- a/src/FOLP/IFOLP.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/FOLP/IFOLP.thy Tue Jun 01 12:33:50 2004 +0200
@@ -10,17 +10,13 @@
global
-classes term < logic
-
+classes term
default term
types
p
o
-arities
- p,o :: logic
-
consts
(*** Judgements ***)
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [51,10] 5)
--- a/src/HOL/HOL.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/HOL/HOL.thy Tue Jun 01 12:33:50 2004 +0200
@@ -14,7 +14,7 @@
subsubsection {* Core syntax *}
-classes type < logic
+classes type
defaultsort type
global
--- a/src/HOL/Import/shuffler.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Jun 01 12:33:50 2004 +0200
@@ -132,8 +132,8 @@
val def_norm =
let
val cert = cterm_of (sign_of ProtoPure.thy)
- val aT = TFree("'a",logicS)
- val bT = TFree("'b",logicS)
+ val aT = TFree("'a",[])
+ val bT = TFree("'b",[])
val v = Free("v",aT)
val P = Free("P",aT-->bT)
val Q = Free("Q",aT-->bT)
@@ -159,8 +159,8 @@
val all_comm =
let
val cert = cterm_of (sign_of ProtoPure.thy)
- val xT = TFree("'a",logicS)
- val yT = TFree("'b",logicS)
+ val xT = TFree("'a",[])
+ val yT = TFree("'b",[])
val P = Free("P",xT-->yT-->propT)
val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
@@ -404,7 +404,7 @@
end
handle e => (writeln "eta_expand internal error";print_exn e)
-fun mk_tfree s = TFree("'"^s,logicS)
+fun mk_tfree s = TFree("'"^s,[])
val xT = mk_tfree "a"
val yT = mk_tfree "b"
val P = Var(("P",0),xT-->yT-->propT)
@@ -495,8 +495,6 @@
end
handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
-fun is_logic_var sg v =
- Type.of_sort (Sign.tsig_of sg) (type_of v,logicS)
(* Closes a theorem with respect to free and schematic variables (does
not touch type variables, though). *)
@@ -505,10 +503,9 @@
let
val sg = sign_of_thm th
val c = prop_of th
- val all_vars = add_term_frees (c,add_term_vars(c,[]))
- val all_rel_vars = filter (is_logic_var sg) all_vars
+ val vars = add_term_frees (c,add_term_vars(c,[]))
in
- Drule.forall_intr_list (map (cterm_of sg) all_rel_vars) th
+ Drule.forall_intr_list (map (cterm_of sg) vars) th
end
handle e => (writeln "close_thm internal error"; print_exn e)
@@ -572,10 +569,9 @@
fun set_prop thy t =
let
val sg = sign_of thy
- val all_vars = add_term_frees (t,add_term_vars (t,[]))
- val all_rel_vars = filter (is_logic_var sg) all_vars
+ val vars = add_term_frees (t,add_term_vars (t,[]))
val closed_t = foldr (fn (v,body) => let val vT = type_of v
- in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (all_rel_vars,t)
+ in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
val rew_th = norm_term thy closed_t
val rhs = snd (dest_equals (cprop_of rew_th))
@@ -596,7 +592,7 @@
val closed_th = equal_elim (symmetric rew_th) mod_th
in
message ("Shuffler.set_prop succeeded by " ^ name);
- Some (name,forall_elim_list (map (cterm_of sg) all_rel_vars) closed_th)
+ Some (name,forall_elim_list (map (cterm_of sg) vars) closed_th)
end
| None => process thms
end
--- a/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Tue Jun 01 12:33:50 2004 +0200
@@ -32,7 +32,7 @@
"ALL " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10)
"EX " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10)
- "_lambda" :: [idts, 'a::logic] => 'b::logic ("(3L _./ _)" 10)
+ "_lambda" :: [idts, 'a] => 'b ("(3L _./ _)" 10)
"_applC" :: [('b => 'a), cargs] => aprop ("(1_/ '(_'))" [1000,1000] 999)
"_cargs" :: ['a, cargs] => cargs ("_,/ _" [1000,1000] 1000)
--- a/src/HOL/Tools/record_package.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Jun 01 12:33:50 2004 +0200
@@ -615,7 +615,7 @@
val tsig = Sign.tsig_of sg
fun mk_type_abbr subst name alphas =
- let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
+ let val abbrT = Type (name, map (fn a => TVar ((a, 0), [])) alphas);
in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
--- a/src/HOL/ex/Higher_Order_Logic.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy Tue Jun 01 12:33:50 2004 +0200
@@ -20,7 +20,7 @@
subsection {* Pure Logic *}
-classes type \<subseteq> logic
+classes type
defaultsort type
typedecl o
--- a/src/Provers/splitter.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Provers/splitter.ML Tue Jun 01 12:33:50 2004 +0200
@@ -76,8 +76,8 @@
val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
val lift =
let val ct = read_cterm (#sign(rep_thm Data.iffD))
- ("[| !!x. (Q::('b::logic)=>('c::logic))(x) == R(x) |] ==> \
- \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT)
+ ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \
+ \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT)
in prove_goalw_cterm [] ct
(fn [prem] => [rewtac prem, rtac reflexive_thm 1])
end;
--- a/src/Pure/Isar/object_logic.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/Isar/object_logic.ML Tue Jun 01 12:33:50 2004 +0200
@@ -115,7 +115,7 @@
fun fixed_judgment sg x =
let (*be robust wrt. low-level errors*)
val c = judgment_name sg;
- val aT = TFree ("'a", logicS);
+ val aT = TFree ("'a", []);
val T =
if_none (Sign.const_type sg c) (aT --> propT)
|> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
--- a/src/Pure/Proof/extraction.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Jun 01 12:33:50 2004 +0200
@@ -42,12 +42,11 @@
|> Theory.copy
|> Theory.root_path
|> Theory.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
- |> Theory.add_arities [("Type", [], "logic"), ("Null", [], "logic")]
|> Theory.add_consts
- [("typeof", "'b::logic => Type", NoSyn),
- ("Type", "'a::logic itself => Type", NoSyn),
+ [("typeof", "'b::{} => Type", NoSyn),
+ ("Type", "'a::{} itself => Type", NoSyn),
("Null", "Null", NoSyn),
- ("realizes", "'a::logic => 'b::logic => 'b", NoSyn)];
+ ("realizes", "'a::{} => 'b::{} => 'b", NoSyn)];
val nullT = Type ("Null", []);
val nullt = Const ("Null", nullT);
--- a/src/Pure/Proof/proof_syntax.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jun 01 12:33:50 2004 +0200
@@ -34,7 +34,7 @@
val paramT = Type ("param", []);
val paramsT = Type ("params", []);
val idtT = Type ("idt", []);
-val aT = TFree ("'a", ["logic"]);
+val aT = TFree ("'a", []);
(** constants for theorems and axioms **)
@@ -49,9 +49,8 @@
sg
|> Sign.copy
|> Sign.add_path "/"
- |> Sign.add_defsort_i ["logic"]
+ |> Sign.add_defsort_i []
|> Sign.add_types [("proof", 0, NoSyn)]
- |> Sign.add_arities [("proof", [], "logic")]
|> Sign.add_consts_i
[("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
--- a/src/Pure/Proof/reconstruct.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Jun 01 12:33:50 2004 +0200
@@ -162,7 +162,7 @@
| mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
let
val (env', T) = (case opT of
- None => mk_tvar (env, logicS) | Some T => (env, T));
+ None => mk_tvar (env, []) | Some T => (env, T));
val (t, prf, cnstrts, env'', vTs') =
mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
in (Const ("all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, Some T, prf),
@@ -216,7 +216,7 @@
end
| (u, prf, cnstrts, env', vTs') =>
let
- val (env1, T) = mk_tvar (env', ["logic"]);
+ val (env1, T) = mk_tvar (env', []);
val (env2, v) = mk_var env1 Ts (T --> propT);
val (env3, t) = mk_var env2 Ts T
in
--- a/src/Pure/axclass.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/axclass.ML Tue Jun 01 12:33:50 2004 +0200
@@ -214,9 +214,6 @@
(* errors *)
-fun err_not_logic c =
- error ("Axiomatic class " ^ quote c ^ " not subclass of " ^ quote logicC);
-
fun err_bad_axsort ax c =
error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c);
@@ -243,19 +240,16 @@
(*prepare abstract axioms*)
fun abs_axm ax =
if null (term_tfrees ax) then
- Logic.mk_implies (Logic.mk_inclass (aT logicS, class), ax)
+ Logic.mk_implies (Logic.mk_inclass (aT [], class), ax)
else map_term_tfrees (K (aT [class])) ax;
val abs_axms = map (abs_axm o #2) axms;
- (*prepare introduction rule*)
- val _ = if Sign.subsort class_sign ([class], logicS) then () else err_not_logic class;
-
fun axm_sort (name, ax) =
(case term_tfrees ax of
[] => []
| [(_, S)] => if Sign.subsort class_sign ([class], S) then S else err_bad_axsort name class
| _ => err_bad_tfrees name);
- val axS = Sign.certify_sort class_sign (logicC :: flat (map axm_sort axms));
+ val axS = Sign.certify_sort class_sign (flat (map axm_sort axms));
val int_axm = Logic.close_form o map_term_tfrees (K (aT axS));
fun inclass c = Logic.mk_inclass (aT axS, c);
--- a/src/Pure/drule.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/drule.ML Tue Jun 01 12:33:50 2004 +0200
@@ -548,16 +548,16 @@
fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
val reflexive_thm =
- let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
+ let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),[])))
in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
val symmetric_thm =
- let val xy = read_prop "x::'a::logic == y"
+ let val xy = read_prop "x == y"
in store_standard_thm_open "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
val transitive_thm =
- let val xy = read_prop "x::'a::logic == y"
- val yz = read_prop "y::'a::logic == z"
+ let val xy = read_prop "x == y"
+ val yz = read_prop "y == z"
val xythm = Thm.assume xy and yzthm = Thm.assume yz
in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
@@ -698,7 +698,7 @@
val norm_hhf_eq =
let
val cert = Thm.cterm_of proto_sign;
- val aT = TFree ("'a", Term.logicS);
+ val aT = TFree ("'a", []);
val all = Term.all aT;
val x = Free ("x", aT);
val phi = Free ("phi", propT);
--- a/src/Pure/proofterm.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/proofterm.ML Tue Jun 01 12:33:50 2004 +0200
@@ -685,8 +685,8 @@
(***** axioms for equality *****)
-val aT = TFree ("'a", ["logic"]);
-val bT = TFree ("'b", ["logic"]);
+val aT = TFree ("'a", []);
+val bT = TFree ("'b", []);
val x = Free ("x", aT);
val y = Free ("y", aT);
val z = Free ("z", aT);
--- a/src/Pure/pure_thy.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/pure_thy.ML Tue Jun 01 12:33:50 2004 +0200
@@ -500,17 +500,7 @@
fun type_of (raw_name, vs, mx) =
if null (duplicates vs) then (raw_name, length vs, mx)
else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
-
- fun arity_of (raw_name, len, mx) =
- (full (Syntax.type_name raw_name mx), replicate len logicS, logicS);
-
- val types = map type_of decls;
- val arities = map arity_of types;
- in
- thy
- |> Theory.add_types types
- |> Theory.add_arities_i arities
- end;
+ in thy |> Theory.add_types (map type_of decls) end;
@@ -531,12 +521,6 @@
("prop", 0, NoSyn),
("itself", 1, NoSyn),
("dummy", 0, NoSyn)]
- |> Theory.add_classes_i [(logicC, [])]
- |> Theory.add_defsort_i logicS
- |> Theory.add_arities_i
- [("fun", [logicS, logicS], logicS),
- ("prop", [], logicS),
- ("itself", [logicS], logicS)]
|> Theory.add_nonterminals Syntax.pure_nonterms
|> Theory.add_syntax Syntax.pure_syntax
|> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
@@ -544,17 +528,17 @@
[("==>", "[prop, prop] => prop", Delimfix "op ==>"),
(Term.dummy_patternN, "aprop", Delimfix "'_")]
|> Theory.add_consts
- [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
+ [("==", "['a, 'a] => prop", InfixrName ("==", 2)),
("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
("Goal", "prop => prop", NoSyn),
("TYPE", "'a itself", NoSyn),
(Term.dummy_patternN, "'a", Delimfix "'_")]
|> Theory.add_finals_i false
- [Const("==",[TFree("'a",[]),TFree("'a",[])]--->propT),
- Const("==>",[propT,propT]--->propT),
- Const("all",(TFree("'a",logicS)-->propT)-->propT),
- Const("TYPE",a_itselfT)]
+ [Const("==", [TFree ("'a", []), TFree ("'a", [])] ---> propT),
+ Const("==>", [propT, propT] ---> propT),
+ Const("all", (TFree("'a", []) --> propT) --> propT),
+ Const("TYPE", a_itselfT)]
|> Theory.add_modesyntax ("", false)
(Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
|> Theory.add_trfuns Syntax.pure_trfuns
--- a/src/Pure/term.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/term.ML Tue Jun 01 12:33:50 2004 +0200
@@ -76,8 +76,6 @@
val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
val dummyT: typ
- val logicC: class
- val logicS: sort
val itselfT: typ -> typ
val a_itselfT: typ
val propT: typ
@@ -415,11 +413,8 @@
(** Connectives of higher order logic **)
-val logicC: class = "logic";
-val logicS: sort = [logicC];
-
fun itselfT ty = Type ("itself", [ty]);
-val a_itselfT = itselfT (TFree ("'a", logicS));
+val a_itselfT = itselfT (TFree ("'a", []));
val propT : typ = Type("prop",[]);
--- a/src/Pure/type_infer.ML Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Pure/type_infer.ML Tue Jun 01 12:33:50 2004 +0200
@@ -103,7 +103,7 @@
(* pretyp(s)_of *)
fun anyT S = TFree ("'_dummy_", S);
-val logicT = anyT logicS;
+val logicT = anyT [];
(*indicate polymorphic Vars*)
fun polymorphicT T = Type ("_polymorphic_", [T]);
--- a/src/Sequents/ILL/ILL_predlog.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Sequents/ILL/ILL_predlog.thy Tue Jun 01 12:33:50 2004 +0200
@@ -7,13 +7,8 @@
ILL_predlog = ILL +
types
-
plf
-arities
-
- plf :: logic
-
consts
"&" :: "[plf,plf] => plf" (infixr 35)
--- a/src/Sequents/LK0.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Sequents/LK0.thy Tue Jun 01 12:33:50 2004 +0200
@@ -13,11 +13,8 @@
global
-classes
- term < logic
-
-default
- term
+classes term
+default term
consts
--- a/src/Sequents/Sequents.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/Sequents/Sequents.thy Tue Jun 01 12:33:50 2004 +0200
@@ -14,9 +14,6 @@
types
o
-arities
- o :: logic
-
(* Sequences *)
--- a/src/ZF/Constructible/MetaExists.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/ZF/Constructible/MetaExists.thy Tue Jun 01 12:33:50 2004 +0200
@@ -11,7 +11,7 @@
quantify over classes. Yields a proposition rather than a FOL formula.*}
constdefs
- ex :: "(('a::logic) => prop) => prop" (binder "?? " 0)
+ ex :: "(('a::{}) => prop) => prop" (binder "?? " 0)
"ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
syntax (xsymbols)
--- a/src/ZF/QPair.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/ZF/QPair.thy Tue Jun 01 12:33:50 2004 +0200
@@ -31,7 +31,7 @@
qsnd :: "i => i"
"qsnd(p) == THE b. EX a. p=<a;b>"
- qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
+ qsplit :: "[[i, i] => 'a, i] => 'a::{}" (*for pattern-matching*)
"qsplit(c,p) == c(qfst(p), qsnd(p))"
qconverse :: "i => i"
--- a/src/ZF/ZF.thy Tue Jun 01 11:25:26 2004 +0200
+++ b/src/ZF/ZF.thy Tue Jun 01 12:33:50 2004 +0200
@@ -61,7 +61,7 @@
Pair :: "[i, i] => i"
fst :: "i => i"
snd :: "i => i"
- split :: "[[i, i] => 'a, i] => 'a::logic" --{*for pattern-matching*}
+ split :: "[[i, i] => 'a, i] => 'a::{}" --{*for pattern-matching*}
text {*Sigma and Pi Operators *}
consts