# HG changeset patch # User haftmann # Date 1282066599 -7200 # Node ID d5477ee358209d0d4479cfb525cf9e4b36654e61 # Parent 8f0cd11238a75907a802028bc398acaa3d24cb8f more antiquotations diff -r 8f0cd11238a7 -r d5477ee35820 src/CCL/Wfd.thy --- 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 diff -r 8f0cd11238a7 -r d5477ee35820 src/FOL/fologic.ML --- 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)); diff -r 8f0cd11238a7 -r d5477ee35820 src/FOL/intprover.ML --- 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) = diff -r 8f0cd11238a7 -r d5477ee35820 src/FOL/simpdata.ML --- 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 diff -r 8f0cd11238a7 -r d5477ee35820 src/Sequents/modal.ML --- 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 _ = []; diff -r 8f0cd11238a7 -r d5477ee35820 src/Sequents/prover.ML --- 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 _ = []; diff -r 8f0cd11238a7 -r d5477ee35820 src/Sequents/simpdata.ML --- 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));