--- a/src/CCL/Wfd.thy Tue Aug 17 19:36:38 2010 +0200
+++ b/src/CCL/Wfd.thy Tue Aug 17 19:36:39 2010 +0200
@@ -423,13 +423,13 @@
@{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
@{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
-fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
+fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l)
| bvars _ l = l
-fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
- | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
- | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
- | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
+fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
+ | get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t
+ | get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
+ | get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t
| get_bno l n (t $ s) = get_bno l n t
| get_bno l n (Bound m) = (m-length(l),n)
@@ -450,7 +450,7 @@
fun is_rigid_prog t =
case (Logic.strip_assums_concl t) of
- (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a [])
+ (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a [])
| _ => false
in
--- a/src/FOL/fologic.ML Tue Aug 17 19:36:38 2010 +0200
+++ b/src/FOL/fologic.ML Tue Aug 17 19:36:39 2010 +0200
@@ -37,48 +37,48 @@
structure FOLogic: FOLOGIC =
struct
-val oT = Type("o",[]);
+val oT = Type(@{type_name o},[]);
-val Trueprop = Const("Trueprop", oT-->propT);
+val Trueprop = Const(@{const_name Trueprop}, oT-->propT);
fun mk_Trueprop P = Trueprop $ P;
-fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
+fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
(* Logical constants *)
-val not = Const ("Not", oT --> oT);
-val conj = Const("op &", [oT,oT]--->oT);
-val disj = Const("op |", [oT,oT]--->oT);
-val imp = Const("op -->", [oT,oT]--->oT)
-val iff = Const("op <->", [oT,oT]--->oT);
+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);
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("op -->",_) $ A $ B) = (A, B)
+fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
-fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
+fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B)
| dest_iff t = raise TERM ("dest_iff", [t]);
-fun eq_const T = Const ("op =", [T, T] ---> oT);
+fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
-fun all_const T = Const ("All", [T --> oT] ---> oT);
+fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
-fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
+fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
--- a/src/FOL/intprover.ML Tue Aug 17 19:36:38 2010 +0200
+++ b/src/FOL/intprover.ML Tue Aug 17 19:36:39 2010 +0200
@@ -40,22 +40,22 @@
step of an intuitionistic proof.
*)
val safe_brls = sort (make_ord lessb)
- [ (true, thm "FalseE"), (false, thm "TrueI"), (false, thm "refl"),
- (false, thm "impI"), (false, thm "notI"), (false, thm "allI"),
- (true, thm "conjE"), (true, thm "exE"),
- (false, thm "conjI"), (true, thm "conj_impE"),
- (true, thm "disj_impE"), (true, thm "disjE"),
- (false, thm "iffI"), (true, thm "iffE"), (true, thm "not_to_imp") ];
+ [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}),
+ (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
+ (true, @{thm conjE}), (true, @{thm exE}),
+ (false, @{thm conjI}), (true, @{thm conj_impE}),
+ (true, @{thm disj_impE}), (true, @{thm disjE}),
+ (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
val haz_brls =
- [ (false, thm "disjI1"), (false, thm "disjI2"), (false, thm "exI"),
- (true, thm "allE"), (true, thm "not_impE"), (true, thm "imp_impE"), (true, thm "iff_impE"),
- (true, thm "all_impE"), (true, thm "ex_impE"), (true, thm "impE") ];
+ [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
+ (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
+ (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
val haz_dup_brls =
- [ (false, thm "disjI1"), (false, thm "disjI2"), (false, thm "exI"),
- (true, thm "all_dupE"), (true, thm "not_impE"), (true, thm "imp_impE"), (true, thm "iff_impE"),
- (true, thm "all_impE"), (true, thm "ex_impE"), (true, thm "impE") ];
+ [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
+ (true, @{thm all_dupE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
+ (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
(*0 subgoals vs 1 or more: the p in safep is for positive*)
val (safe0_brls, safep_brls) =
--- a/src/FOL/simpdata.ML Tue Aug 17 19:36:38 2010 +0200
+++ b/src/FOL/simpdata.ML Tue Aug 17 19:36:39 2010 +0200
@@ -8,16 +8,16 @@
(*Make meta-equalities. The operator below is Trueprop*)
fun mk_meta_eq th = case concl_of th of
- _ $ (Const("op =",_)$_$_) => th RS @{thm eq_reflection}
- | _ $ (Const("op <->",_)$_$_) => th RS @{thm iff_reflection}
+ _ $ (Const(@{const_name "op ="},_)$_$_) => th RS @{thm eq_reflection}
+ | _ $ (Const(@{const_name "op <->"},_)$_$_) => th RS @{thm iff_reflection}
| _ =>
error("conclusion must be a =-equality or <->");;
fun mk_eq th = case concl_of th of
Const("==",_)$_$_ => th
- | _ $ (Const("op =",_)$_$_) => mk_meta_eq th
- | _ $ (Const("op <->",_)$_$_) => mk_meta_eq th
- | _ $ (Const("Not",_)$_) => th RS @{thm iff_reflection_F}
+ | _ $ (Const(@{const_name "op ="},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name "op <->"},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T};
(*Replace premises x=y, X<->Y by X==Y*)
@@ -32,13 +32,13 @@
error("Premises and conclusion of congruence rules must use =-equality or <->");
val mksimps_pairs =
- [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
- ("All", [@{thm spec}]), ("True", []), ("False", [])];
+ [(@{const_name "op -->"}, [@{thm mp}]), (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ (@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])];
fun mk_atomize pairs =
let fun atoms th =
(case concl_of th of
- Const("Trueprop",_) $ p =>
+ Const(@{const_name Trueprop},_) $ p =>
(case head_of p of
Const(a,_) =>
(case AList.lookup (op =) pairs a of
@@ -55,11 +55,11 @@
structure Quantifier1 = Quantifier1Fun(
struct
(*abstract syntax*)
- fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t)
+ fun dest_eq((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME(c,s,t)
| dest_eq _ = NONE;
- fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t)
+ fun dest_conj((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME(c,s,t)
| dest_conj _ = NONE;
- fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t)
+ fun dest_imp((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME(c,s,t)
| dest_imp _ = NONE;
val conj = FOLogic.conj
val imp = FOLogic.imp
--- a/src/Sequents/modal.ML Tue Aug 17 19:36:38 2010 +0200
+++ b/src/Sequents/modal.ML Tue Aug 17 19:36:39 2010 +0200
@@ -29,7 +29,7 @@
in
(*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u
+fun forms_of_seq (Const(@{const_name SeqO'},_) $ P $ u) = P :: forms_of_seq u
| forms_of_seq (H $ u) = forms_of_seq u
| forms_of_seq _ = [];
--- a/src/Sequents/prover.ML Tue Aug 17 19:36:38 2010 +0200
+++ b/src/Sequents/prover.ML Tue Aug 17 19:36:39 2010 +0200
@@ -55,7 +55,7 @@
["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
(*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
+fun forms_of_seq (Const(@{const_name "SeqO'"},_) $ P $ u) = P :: forms_of_seq u
| forms_of_seq (H $ u) = forms_of_seq u
| forms_of_seq _ = [];
--- a/src/Sequents/simpdata.ML Tue Aug 17 19:36:38 2010 +0200
+++ b/src/Sequents/simpdata.ML Tue Aug 17 19:36:39 2010 +0200
@@ -13,16 +13,16 @@
(*Make atomic rewrite rules*)
fun atomize r =
case concl_of r of
- Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
+ Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (forms_of_seq a, forms_of_seq c) of
([], [p]) =>
(case p of
- Const("imp",_)$_$_ => atomize(r RS @{thm mp_R})
- | Const("conj",_)$_$_ => atomize(r RS @{thm conjunct1}) @
+ Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R})
+ | Const(@{const_name conj},_)$_$_ => atomize(r RS @{thm conjunct1}) @
atomize(r RS @{thm conjunct2})
- | Const("All",_)$_ => atomize(r RS @{thm spec})
- | Const("True",_) => [] (*True is DELETED*)
- | Const("False",_) => [] (*should False do something?*)
+ | Const(@{const_name All},_)$_ => atomize(r RS @{thm spec})
+ | Const(@{const_name True},_) => [] (*True is DELETED*)
+ | Const(@{const_name False},_) => [] (*should False do something?*)
| _ => [r])
| _ => []) (*ignore theorem unless it has precisely one conclusion*)
| _ => [r];
@@ -30,13 +30,13 @@
(*Make meta-equalities.*)
fun mk_meta_eq th = case concl_of th of
Const("==",_)$_$_ => th
- | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
+ | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (forms_of_seq a, forms_of_seq c) of
([], [p]) =>
(case p of
- (Const("equal",_)$_$_) => th RS @{thm eq_reflection}
- | (Const("iff",_)$_$_) => th RS @{thm iff_reflection}
- | (Const("Not",_)$_) => th RS @{thm iff_reflection_F}
+ (Const(@{const_name equal},_)$_$_) => th RS @{thm eq_reflection}
+ | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
+ | (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
| _ => error ("addsimps: unable to use theorem\n" ^
Display.string_of_thm_without_context th));