more antiquotations;
authorwenzelm
Sat Mar 22 20:42:16 2014 +0100 (2014-03-22)
changeset 562561e01c159e7d9
parent 56255 968667bbb8d2
child 56257 589fafcc7cb6
more antiquotations;
src/HOL/Import/import_rule.ML
src/HOL/Library/refute.ML
src/HOL/NSA/StarDef.thy
src/HOL/NSA/transfer.ML
src/HOL/TLA/Action.thy
src/HOL/TLA/Intensional.thy
src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
     1.1 --- a/src/HOL/Import/import_rule.ML	Sat Mar 22 19:33:39 2014 +0100
     1.2 +++ b/src/HOL/Import/import_rule.ML	Sat Mar 22 20:42:16 2014 +0100
     1.3 @@ -409,7 +409,7 @@
     1.4            end
     1.5        | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
     1.6        | process (thy, state) (#"t", [n]) =
     1.7 -          setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), ["HOL.type"]))) (thy, state)
     1.8 +          setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), @{sort type}))) (thy, state)
     1.9        | process (thy, state) (#"a", n :: l) =
    1.10            fold_map getty l (thy, state) |>>
    1.11              (fn tys => ctyp_of thy (Type (gettyname n thy, map typ_of tys))) |-> setty
     2.1 --- a/src/HOL/Library/refute.ML	Sat Mar 22 19:33:39 2014 +0100
     2.2 +++ b/src/HOL/Library/refute.ML	Sat Mar 22 20:42:16 2014 +0100
     2.3 @@ -4,11 +4,6 @@
     2.4  Finite model generation for HOL formulas, using a SAT solver.
     2.5  *)
     2.6  
     2.7 -(* ------------------------------------------------------------------------- *)
     2.8 -(* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
     2.9 -(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
    2.10 -(* ------------------------------------------------------------------------- *)
    2.11 -
    2.12  signature REFUTE =
    2.13  sig
    2.14  
    2.15 @@ -638,6 +633,16 @@
    2.16  (* To avoid collecting the same axiom multiple times, we use an           *)
    2.17  (* accumulator 'axs' which contains all axioms collected so far.          *)
    2.18  
    2.19 +local
    2.20 +
    2.21 +fun get_axiom thy xname =
    2.22 +  Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);
    2.23 +
    2.24 +val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial";
    2.25 +val someI = get_axiom @{theory Hilbert_Choice} "someI";
    2.26 +
    2.27 +in
    2.28 +
    2.29  fun collect_axioms ctxt t =
    2.30    let
    2.31      val thy = Proof_Context.theory_of ctxt
    2.32 @@ -724,17 +729,15 @@
    2.33        | Const (@{const_name undefined}, T) => collect_type_axioms T axs
    2.34        | Const (@{const_name The}, T) =>
    2.35            let
    2.36 -            val ax = specialize_type thy (@{const_name The}, T)
    2.37 -              (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
    2.38 +            val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial)
    2.39            in
    2.40 -            collect_this_axiom ("HOL.the_eq_trivial", ax) axs
    2.41 +            collect_this_axiom (#1 the_eq_trivial, ax) axs
    2.42            end
    2.43        | Const (@{const_name Hilbert_Choice.Eps}, T) =>
    2.44            let
    2.45 -            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
    2.46 -              (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
    2.47 +            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI)
    2.48            in
    2.49 -            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
    2.50 +            collect_this_axiom (#1 someI, ax) axs
    2.51            end
    2.52        | Const (@{const_name All}, T) => collect_type_axioms T axs
    2.53        | Const (@{const_name Ex}, T) => collect_type_axioms T axs
    2.54 @@ -806,6 +809,8 @@
    2.55      result
    2.56    end;
    2.57  
    2.58 +end;
    2.59 +
    2.60  (* ------------------------------------------------------------------------- *)
    2.61  (* ground_types: collects all ground types in a term (including argument     *)
    2.62  (*               types of other types), suppressing duplicates.  Does not    *)
    2.63 @@ -3032,7 +3037,7 @@
    2.64  (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
    2.65  (*       subterms that are then passed to other interpreters!                *)
    2.66  (* ------------------------------------------------------------------------- *)
    2.67 -
    2.68 +(* FIXME formal @{const_name} for some entries (!??) *)
    2.69  val setup =
    2.70     add_interpreter "stlc"    stlc_interpreter #>
    2.71     add_interpreter "Pure"    Pure_interpreter #>
     3.1 --- a/src/HOL/NSA/StarDef.thy	Sat Mar 22 19:33:39 2014 +0100
     3.2 +++ b/src/HOL/NSA/StarDef.thy	Sat Mar 22 20:42:16 2014 +0100
     3.3 @@ -172,7 +172,7 @@
     3.4    "Standard = range star_of"
     3.5  
     3.6  text {* Transfer tactic should remove occurrences of @{term star_of} *}
     3.7 -setup {* Transfer_Principle.add_const "StarDef.star_of" *}
     3.8 +setup {* Transfer_Principle.add_const @{const_name star_of} *}
     3.9  
    3.10  declare star_of_def [transfer_intro]
    3.11  
    3.12 @@ -199,7 +199,7 @@
    3.13      UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
    3.14  
    3.15  text {* Transfer tactic should remove occurrences of @{term Ifun} *}
    3.16 -setup {* Transfer_Principle.add_const "StarDef.Ifun" *}
    3.17 +setup {* Transfer_Principle.add_const @{const_name Ifun} *}
    3.18  
    3.19  lemma transfer_Ifun [transfer_intro]:
    3.20    "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
    3.21 @@ -306,7 +306,7 @@
    3.22  by (simp add: unstar_def star_of_inject)
    3.23  
    3.24  text {* Transfer tactic should remove occurrences of @{term unstar} *}
    3.25 -setup {* Transfer_Principle.add_const "StarDef.unstar" *}
    3.26 +setup {* Transfer_Principle.add_const @{const_name unstar} *}
    3.27  
    3.28  lemma transfer_unstar [transfer_intro]:
    3.29    "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
    3.30 @@ -348,7 +348,7 @@
    3.31  by (simp add: Iset_def starP2_star_n)
    3.32  
    3.33  text {* Transfer tactic should remove occurrences of @{term Iset} *}
    3.34 -setup {* Transfer_Principle.add_const "StarDef.Iset" *}
    3.35 +setup {* Transfer_Principle.add_const @{const_name Iset} *}
    3.36  
    3.37  lemma transfer_mem [transfer_intro]:
    3.38    "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
     4.1 --- a/src/HOL/NSA/transfer.ML	Sat Mar 22 19:33:39 2014 +0100
     4.2 +++ b/src/HOL/NSA/transfer.ML	Sat Mar 22 20:42:16 2014 +0100
     4.3 @@ -35,7 +35,7 @@
     4.4      consts = Library.merge (op =) (consts1, consts2)};
     4.5  );
     4.6  
     4.7 -fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
     4.8 +fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
     4.9    | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
    4.10    | unstar_typ T = T
    4.11  
     5.1 --- a/src/HOL/TLA/Action.thy	Sat Mar 22 19:33:39 2014 +0100
     5.2 +++ b/src/HOL/TLA/Action.thy	Sat Mar 22 20:42:16 2014 +0100
     5.3 @@ -117,7 +117,7 @@
     5.4  
     5.5  fun action_use ctxt th =
     5.6      case (concl_of th) of
     5.7 -      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
     5.8 +      Const _ $ (Const (@{const_name Valid}, _) $ _) =>
     5.9                (flatten (action_unlift ctxt th) handle THM _ => th)
    5.10      | _ => th;
    5.11  *}
     6.1 --- a/src/HOL/TLA/Intensional.thy	Sat Mar 22 19:33:39 2014 +0100
     6.2 +++ b/src/HOL/TLA/Intensional.thy	Sat Mar 22 20:42:16 2014 +0100
     6.3 @@ -283,7 +283,7 @@
     6.4  
     6.5  fun int_use ctxt th =
     6.6      case (concl_of th) of
     6.7 -      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
     6.8 +      Const _ $ (Const (@{const_name Valid}, _) $ _) =>
     6.9                (flatten (int_unlift ctxt th) handle THM _ => th)
    6.10      | _ => th
    6.11  *}
     7.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Sat Mar 22 19:33:39 2014 +0100
     7.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Sat Mar 22 20:42:16 2014 +0100
     7.3 @@ -256,11 +256,11 @@
     7.4    in
     7.5      case thf_ty of
     7.6         Prod_type (thf_ty1, thf_ty2) =>
     7.7 -         Type ("Product_Type.prod",
     7.8 +         Type (@{type_name prod},
     7.9            [interpret_type config thy type_map thf_ty1,
    7.10             interpret_type config thy type_map thf_ty2])
    7.11       | Fn_type (thf_ty1, thf_ty2) =>
    7.12 -         Type ("fun",
    7.13 +         Type (@{type_name fun},
    7.14            [interpret_type config thy type_map thf_ty1,
    7.15             interpret_type config thy type_map thf_ty2])
    7.16       | Atom_type _ =>
    7.17 @@ -398,8 +398,7 @@
    7.18  (*As above, but for products*)
    7.19  fun mtimes thy =
    7.20    fold (fn x => fn y =>
    7.21 -    Sign.mk_const thy
    7.22 -    ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x)
    7.23 +    Sign.mk_const thy (@{const_name Pair}, [dummyT, dummyT]) $ y $ x)
    7.24  
    7.25  fun mtimes' (args, thy) f =
    7.26    let
    7.27 @@ -456,11 +455,11 @@
    7.28    end
    7.29  
    7.30  (*Next batch of functions give info about Isabelle/HOL types*)
    7.31 -fun is_fun (Type ("fun", _)) = true
    7.32 +fun is_fun (Type (@{type_name fun}, _)) = true
    7.33    | is_fun _ = false
    7.34 -fun is_prod (Type ("Product_Type.prod", _)) = true
    7.35 +fun is_prod (Type (@{type_name prod}, _)) = true
    7.36    | is_prod _ = false
    7.37 -fun dom_type (Type ("fun", [ty1, _])) = ty1
    7.38 +fun dom_type (Type (@{type_name fun}, [ty1, _])) = ty1
    7.39  fun is_prod_typed thy config symb =
    7.40    let
    7.41      fun symb_type const_name =
     8.1 --- a/src/HOL/ex/SVC_Oracle.thy	Sat Mar 22 19:33:39 2014 +0100
     8.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Sat Mar 22 20:42:16 2014 +0100
     8.3 @@ -11,12 +11,12 @@
     8.4  imports Main
     8.5  begin
     8.6  
     8.7 -ML_file "svc_funcs.ML"
     8.8 -
     8.9  consts
    8.10    iff_keep :: "[bool, bool] => bool"
    8.11    iff_unfold :: "[bool, bool] => bool"
    8.12  
    8.13 +ML_file "svc_funcs.ML"
    8.14 +
    8.15  hide_const iff_keep iff_unfold
    8.16  
    8.17  oracle svc_oracle = Svc.oracle
     9.1 --- a/src/HOL/ex/svc_funcs.ML	Sat Mar 22 19:33:39 2014 +0100
     9.2 +++ b/src/HOL/ex/svc_funcs.ML	Sat Mar 22 20:42:16 2014 +0100
     9.3 @@ -199,10 +199,10 @@
     9.4              Buildin("NOT", [fm (not pos) p])
     9.5        | fm pos (Const(@{const_name True}, _)) = TrueExpr
     9.6        | fm pos (Const(@{const_name False}, _)) = FalseExpr
     9.7 -      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
     9.8 +      | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) =
     9.9               (*polarity doesn't matter*)
    9.10              Buildin("=", [fm pos p, fm pos q])
    9.11 -      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
    9.12 +      | fm pos (Const(@{const_name iff_unfold}, _) $ p $ q) =
    9.13              Buildin("AND",   (*unfolding uses both polarities*)
    9.14                           [Buildin("=>", [fm (not pos) p, fm pos q]),
    9.15                            Buildin("=>", [fm (not pos) q, fm pos p])])