more antiquotations;
authorwenzelm
Sat Mar 22 18:15:09 2014 +0100 (2014-03-22)
changeset 56252b72e0a9d62b9
parent 56251 73e2e1912571
child 56253 83b3c110f22d
more antiquotations;
src/HOL/Library/bnf_decl.ML
src/HOL/Library/refute.ML
src/HOL/Library/simps_case_conv.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
     1.1 --- a/src/HOL/Library/bnf_decl.ML	Sat Mar 22 18:12:08 2014 +0100
     1.2 +++ b/src/HOL/Library/bnf_decl.ML	Sat Mar 22 18:15:09 2014 +0100
     1.3 @@ -94,7 +94,7 @@
     1.4  
     1.5  val bnf_decl = prepare_decl (K I) (K I);
     1.6  
     1.7 -fun read_constraint _ NONE = HOLogic.typeS
     1.8 +fun read_constraint _ NONE = @{sort type}
     1.9    | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
    1.10  
    1.11  val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
     2.1 --- a/src/HOL/Library/refute.ML	Sat Mar 22 18:12:08 2014 +0100
     2.2 +++ b/src/HOL/Library/refute.ML	Sat Mar 22 18:15:09 2014 +0100
     2.3 @@ -579,7 +579,7 @@
     2.4            Type ("fun", [@{typ nat}, @{typ nat}])])) => t
     2.5        | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
     2.6            Type ("fun", [@{typ nat}, @{typ nat}])])) => t
     2.7 -      | Const (@{const_name List.append}, _) => t
     2.8 +      | Const (@{const_name append}, _) => t
     2.9  (* UNSOUND
    2.10        | Const (@{const_name lfp}, _) => t
    2.11        | Const (@{const_name gfp}, _) => t
    2.12 @@ -684,11 +684,11 @@
    2.13      and collect_type_axioms T axs =
    2.14        case T of
    2.15        (* simple types *)
    2.16 -        Type ("prop", []) => axs
    2.17 -      | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
    2.18 +        Type (@{type_name prop}, []) => axs
    2.19 +      | Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
    2.20        | Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs
    2.21        (* axiomatic type classes *)
    2.22 -      | Type ("itself", [T1]) => collect_type_axioms T1 axs
    2.23 +      | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
    2.24        | Type (s, Ts) =>
    2.25          (case Datatype.get_info thy s of
    2.26            SOME _ =>  (* inductive datatype *)
    2.27 @@ -761,7 +761,7 @@
    2.28        | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
    2.29          Type ("fun", [@{typ nat}, @{typ nat}])])) =>
    2.30            collect_type_axioms T axs
    2.31 -      | Const (@{const_name List.append}, T) => collect_type_axioms T axs
    2.32 +      | Const (@{const_name append}, T) => collect_type_axioms T axs
    2.33  (* UNSOUND
    2.34        | Const (@{const_name lfp}, T) => collect_type_axioms T axs
    2.35        | Const (@{const_name gfp}, T) => collect_type_axioms T axs
    2.36 @@ -819,8 +819,8 @@
    2.37      val thy = Proof_Context.theory_of ctxt
    2.38      fun collect_types T acc =
    2.39        (case T of
    2.40 -        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
    2.41 -      | Type ("prop", []) => acc
    2.42 +        Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc)
    2.43 +      | Type (@{type_name prop}, []) => acc
    2.44        | Type (@{type_name set}, [T1]) => collect_types T1 acc
    2.45        | Type (s, Ts) =>
    2.46            (case Datatype.get_info thy s of
    2.47 @@ -2620,11 +2620,12 @@
    2.48  
    2.49  fun List_append_interpreter ctxt model args t =
    2.50    case t of
    2.51 -    Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
    2.52 -        [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
    2.53 +    Const (@{const_name append},
    2.54 +      Type (@{type_name fun}, [Type (@{type_name list}, [T]),
    2.55 +        Type (@{type_name fun}, [Type (@{type_name list}, [_]), Type (@{type_name list}, [_])])])) =>
    2.56        let
    2.57          val size_elem = size_of_type ctxt model T
    2.58 -        val size_list = size_of_type ctxt model (Type ("List.list", [T]))
    2.59 +        val size_list = size_of_type ctxt model (Type (@{type_name list}, [T]))
    2.60          (* maximal length of lists; 0 if we only consider the empty list *)
    2.61          val list_length =
    2.62            let
    2.63 @@ -2866,7 +2867,7 @@
    2.64          in
    2.65            SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
    2.66          end
    2.67 -    | Type ("prop", []) =>
    2.68 +    | Type (@{type_name prop}, []) =>
    2.69          (case index_from_interpretation intr of
    2.70            ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
    2.71          | 0  => SOME (HOLogic.mk_Trueprop @{term True})
     3.1 --- a/src/HOL/Library/simps_case_conv.ML	Sat Mar 22 18:12:08 2014 +0100
     3.2 +++ b/src/HOL/Library/simps_case_conv.ML	Sat Mar 22 18:15:09 2014 +0100
     3.3 @@ -152,13 +152,12 @@
     3.4  
     3.5  fun was_split t =
     3.6    let
     3.7 -    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
     3.8 -              o fst o HOLogic.dest_imp
     3.9 +    val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
    3.10      val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
    3.11 -    fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
    3.12 +    fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
    3.13        | dest_alls t = t
    3.14    in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
    3.15 -        handle TERM _ => false
    3.16 +  handle TERM _ => false
    3.17  
    3.18  fun apply_split ctxt split thm = Seq.of_list
    3.19    let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
     4.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Mar 22 18:12:08 2014 +0100
     4.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat Mar 22 18:15:09 2014 +0100
     4.3 @@ -999,15 +999,15 @@
     4.4      val is =
     4.5        upto (1, arity)
     4.6        |> map Int.toString
     4.7 -    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)) is
     4.8 -    val res_ty = TFree ("res" ^ "_ty", HOLogic.typeS)
     4.9 +    val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is
    4.10 +    val res_ty = TFree ("res" ^ "_ty", @{sort type})
    4.11      val f_ty = arg_tys ---> res_ty
    4.12      val f = Free ("f", f_ty)
    4.13      val xs = map (fn i =>
    4.14 -      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
    4.15 +      Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
    4.16      (*FIXME DRY principle*)
    4.17      val ys = map (fn i =>
    4.18 -      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
    4.19 +      Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
    4.20  
    4.21      val hyp_lhs = list_comb (f, xs)
    4.22      val hyp_rhs = list_comb (f, ys)
    4.23 @@ -1018,7 +1018,7 @@
    4.24        |> HOLogic.mk_Trueprop
    4.25      fun conc_eq i =
    4.26        let
    4.27 -        val ty = TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)
    4.28 +        val ty = TFree ("arg" ^ i ^ "_ty", @{sort type})
    4.29          val x = Free ("x" ^ i, ty)
    4.30          val y = Free ("y" ^ i, ty)
    4.31          val eq = HOLogic.eq_const ty $ x $ y