# HG changeset patch # User wenzelm # Date 1395517336 -3600 # Node ID 1e01c159e7d91ebba19a071ca44e0137396fda5d # Parent 968667bbb8d24393817e49bfad3488f13c6fbdee more antiquotations; diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/Import/import_rule.ML Sat Mar 22 20:42:16 2014 +0100 @@ -409,7 +409,7 @@ end | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state) | process (thy, state) (#"t", [n]) = - setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), ["HOL.type"]))) (thy, state) + setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), @{sort type}))) (thy, state) | process (thy, state) (#"a", n :: l) = fold_map getty l (thy, state) |>> (fn tys => ctyp_of thy (Type (gettyname n thy, map typ_of tys))) |-> setty diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/Library/refute.ML Sat Mar 22 20:42:16 2014 +0100 @@ -4,11 +4,6 @@ Finite model generation for HOL formulas, using a SAT solver. *) -(* ------------------------------------------------------------------------- *) -(* Declares the 'REFUTE' signature as well as a structure 'Refute'. *) -(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'. *) -(* ------------------------------------------------------------------------- *) - signature REFUTE = sig @@ -638,6 +633,16 @@ (* To avoid collecting the same axiom multiple times, we use an *) (* accumulator 'axs' which contains all axioms collected so far. *) +local + +fun get_axiom thy xname = + Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none); + +val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial"; +val someI = get_axiom @{theory Hilbert_Choice} "someI"; + +in + fun collect_axioms ctxt t = let val thy = Proof_Context.theory_of ctxt @@ -724,17 +729,15 @@ | Const (@{const_name undefined}, T) => collect_type_axioms T axs | Const (@{const_name The}, T) => let - val ax = specialize_type thy (@{const_name The}, T) - (the (AList.lookup (op =) axioms "HOL.the_eq_trivial")) + val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial) in - collect_this_axiom ("HOL.the_eq_trivial", ax) axs + collect_this_axiom (#1 the_eq_trivial, ax) axs end | Const (@{const_name Hilbert_Choice.Eps}, T) => let - val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) - (the (AList.lookup (op =) axioms "Hilbert_Choice.someI")) + val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI) in - collect_this_axiom ("Hilbert_Choice.someI", ax) axs + collect_this_axiom (#1 someI, ax) axs end | Const (@{const_name All}, T) => collect_type_axioms T axs | Const (@{const_name Ex}, T) => collect_type_axioms T axs @@ -806,6 +809,8 @@ result end; +end; + (* ------------------------------------------------------------------------- *) (* ground_types: collects all ground types in a term (including argument *) (* types of other types), suppressing duplicates. Does not *) @@ -3032,7 +3037,7 @@ (* applied before the 'stlc_interpreter' breaks the term apart into *) (* subterms that are then passed to other interpreters! *) (* ------------------------------------------------------------------------- *) - +(* FIXME formal @{const_name} for some entries (!??) *) val setup = add_interpreter "stlc" stlc_interpreter #> add_interpreter "Pure" Pure_interpreter #> diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/NSA/StarDef.thy Sat Mar 22 20:42:16 2014 +0100 @@ -172,7 +172,7 @@ "Standard = range star_of" text {* Transfer tactic should remove occurrences of @{term star_of} *} -setup {* Transfer_Principle.add_const "StarDef.star_of" *} +setup {* Transfer_Principle.add_const @{const_name star_of} *} declare star_of_def [transfer_intro] @@ -199,7 +199,7 @@ UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2]) text {* Transfer tactic should remove occurrences of @{term Ifun} *} -setup {* Transfer_Principle.add_const "StarDef.Ifun" *} +setup {* Transfer_Principle.add_const @{const_name Ifun} *} lemma transfer_Ifun [transfer_intro]: "\f \ star_n F; x \ star_n X\ \ f \ x \ star_n (\n. F n (X n))" @@ -306,7 +306,7 @@ by (simp add: unstar_def star_of_inject) text {* Transfer tactic should remove occurrences of @{term unstar} *} -setup {* Transfer_Principle.add_const "StarDef.unstar" *} +setup {* Transfer_Principle.add_const @{const_name unstar} *} lemma transfer_unstar [transfer_intro]: "p \ star_n P \ unstar p \ {n. P n} \ \" @@ -348,7 +348,7 @@ by (simp add: Iset_def starP2_star_n) text {* Transfer tactic should remove occurrences of @{term Iset} *} -setup {* Transfer_Principle.add_const "StarDef.Iset" *} +setup {* Transfer_Principle.add_const @{const_name Iset} *} lemma transfer_mem [transfer_intro]: "\x \ star_n X; a \ Iset (star_n A)\ diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/NSA/transfer.ML Sat Mar 22 20:42:16 2014 +0100 @@ -35,7 +35,7 @@ consts = Library.merge (op =) (consts1, consts2)}; ); -fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t +fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts) | unstar_typ T = T diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/TLA/Action.thy Sat Mar 22 20:42:16 2014 +0100 @@ -117,7 +117,7 @@ fun action_use ctxt th = case (concl_of th) of - Const _ $ (Const ("Intensional.Valid", _) $ _) => + Const _ $ (Const (@{const_name Valid}, _) $ _) => (flatten (action_unlift ctxt th) handle THM _ => th) | _ => th; *} diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/TLA/Intensional.thy Sat Mar 22 20:42:16 2014 +0100 @@ -283,7 +283,7 @@ fun int_use ctxt th = case (concl_of th) of - Const _ $ (Const ("Intensional.Valid", _) $ _) => + Const _ $ (Const (@{const_name Valid}, _) $ _) => (flatten (int_unlift ctxt th) handle THM _ => th) | _ => th *} diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Sat Mar 22 20:42:16 2014 +0100 @@ -256,11 +256,11 @@ in case thf_ty of Prod_type (thf_ty1, thf_ty2) => - Type ("Product_Type.prod", + Type (@{type_name prod}, [interpret_type config thy type_map thf_ty1, interpret_type config thy type_map thf_ty2]) | Fn_type (thf_ty1, thf_ty2) => - Type ("fun", + Type (@{type_name fun}, [interpret_type config thy type_map thf_ty1, interpret_type config thy type_map thf_ty2]) | Atom_type _ => @@ -398,8 +398,7 @@ (*As above, but for products*) fun mtimes thy = fold (fn x => fn y => - Sign.mk_const thy - ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x) + Sign.mk_const thy (@{const_name Pair}, [dummyT, dummyT]) $ y $ x) fun mtimes' (args, thy) f = let @@ -456,11 +455,11 @@ end (*Next batch of functions give info about Isabelle/HOL types*) -fun is_fun (Type ("fun", _)) = true +fun is_fun (Type (@{type_name fun}, _)) = true | is_fun _ = false -fun is_prod (Type ("Product_Type.prod", _)) = true +fun is_prod (Type (@{type_name prod}, _)) = true | is_prod _ = false -fun dom_type (Type ("fun", [ty1, _])) = ty1 +fun dom_type (Type (@{type_name fun}, [ty1, _])) = ty1 fun is_prod_typed thy config symb = let fun symb_type const_name = diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/ex/SVC_Oracle.thy Sat Mar 22 20:42:16 2014 +0100 @@ -11,12 +11,12 @@ imports Main begin -ML_file "svc_funcs.ML" - consts iff_keep :: "[bool, bool] => bool" iff_unfold :: "[bool, bool] => bool" +ML_file "svc_funcs.ML" + hide_const iff_keep iff_unfold oracle svc_oracle = Svc.oracle diff -r 968667bbb8d2 -r 1e01c159e7d9 src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Sat Mar 22 19:33:39 2014 +0100 +++ b/src/HOL/ex/svc_funcs.ML Sat Mar 22 20:42:16 2014 +0100 @@ -199,10 +199,10 @@ Buildin("NOT", [fm (not pos) p]) | fm pos (Const(@{const_name True}, _)) = TrueExpr | fm pos (Const(@{const_name False}, _)) = FalseExpr - | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = + | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) = (*polarity doesn't matter*) Buildin("=", [fm pos p, fm pos q]) - | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = + | fm pos (Const(@{const_name iff_unfold}, _) $ p $ q) = Buildin("AND", (*unfolding uses both polarities*) [Buildin("=>", [fm (not pos) p, fm pos q]), Buildin("=>", [fm (not pos) q, fm pos p])])