more antiquotations
authorhaftmann
Wed Aug 18 12:08:21 2010 +0200 (2010-08-18)
changeset 3851333ab01218ae1
parent 38512 ed4703b416ed
child 38514 bd9c4e8281ec
more antiquotations
src/ZF/arith_data.ML
src/ZF/simpdata.ML
     1.1 --- a/src/ZF/arith_data.ML	Wed Aug 18 11:55:27 2010 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Wed Aug 18 12:08:21 2010 +0200
     1.3 @@ -24,12 +24,12 @@
     1.4  
     1.5  val iT = Ind_Syntax.iT;
     1.6  
     1.7 -val zero = Const("0", iT);
     1.8 -val succ = Const("succ", iT --> iT);
     1.9 +val zero = Const(@{const_name 0}, iT);
    1.10 +val succ = Const(@{const_name succ}, iT --> iT);
    1.11  fun mk_succ t = succ $ t;
    1.12  val one = mk_succ zero;
    1.13  
    1.14 -val mk_plus = FOLogic.mk_binop "Arith.add";
    1.15 +val mk_plus = FOLogic.mk_binop @{const_name Arith.add};
    1.16  
    1.17  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    1.18  fun mk_sum []        = zero
    1.19 @@ -40,13 +40,13 @@
    1.20  fun long_mk_sum []        = zero
    1.21    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.22  
    1.23 -val dest_plus = FOLogic.dest_bin "Arith.add" iT;
    1.24 +val dest_plus = FOLogic.dest_bin @{const_name Arith.add} iT;
    1.25  
    1.26  (* dest_sum *)
    1.27  
    1.28 -fun dest_sum (Const("0",_)) = []
    1.29 -  | dest_sum (Const("succ",_) $ t) = one :: dest_sum t
    1.30 -  | dest_sum (Const("Arith.add",_) $ t $ u) = dest_sum t @ dest_sum u
    1.31 +fun dest_sum (Const(@{const_name 0},_)) = []
    1.32 +  | dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
    1.33 +  | dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
    1.34    | dest_sum tm = [tm];
    1.35  
    1.36  (*Apply the given rewrite (if present) just once*)
    1.37 @@ -83,14 +83,14 @@
    1.38  (*** Use CancelNumerals simproc without binary numerals,
    1.39       just for cancellation ***)
    1.40  
    1.41 -val mk_times = FOLogic.mk_binop "Arith.mult";
    1.42 +val mk_times = FOLogic.mk_binop @{const_name Arith.mult};
    1.43  
    1.44  fun mk_prod [] = one
    1.45    | mk_prod [t] = t
    1.46    | mk_prod (t :: ts) = if t = one then mk_prod ts
    1.47                          else mk_times (t, mk_prod ts);
    1.48  
    1.49 -val dest_times = FOLogic.dest_bin "Arith.mult" iT;
    1.50 +val dest_times = FOLogic.dest_bin @{const_name Arith.mult} iT;
    1.51  
    1.52  fun dest_prod t =
    1.53        let val (t,u) = dest_times t
    1.54 @@ -174,8 +174,8 @@
    1.55    struct
    1.56    open CancelNumeralsCommon
    1.57    val prove_conv = prove_conv "natless_cancel_numerals"
    1.58 -  val mk_bal   = FOLogic.mk_binrel "Ordinal.lt"
    1.59 -  val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
    1.60 +  val mk_bal   = FOLogic.mk_binrel @{const_name Ordinal.lt}
    1.61 +  val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
    1.62    val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
    1.63    val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
    1.64    fun trans_tac _ = gen_trans_tac @{thm iff_trans}
    1.65 @@ -187,8 +187,8 @@
    1.66    struct
    1.67    open CancelNumeralsCommon
    1.68    val prove_conv = prove_conv "natdiff_cancel_numerals"
    1.69 -  val mk_bal   = FOLogic.mk_binop "Arith.diff"
    1.70 -  val dest_bal = FOLogic.dest_bin "Arith.diff" iT
    1.71 +  val mk_bal   = FOLogic.mk_binop @{const_name Arith.diff}
    1.72 +  val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
    1.73    val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
    1.74    val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
    1.75    fun trans_tac _ = gen_trans_tac @{thm trans}
     2.1 --- a/src/ZF/simpdata.ML	Wed Aug 18 11:55:27 2010 +0200
     2.2 +++ b/src/ZF/simpdata.ML	Wed Aug 18 12:08:21 2010 +0200
     2.3 @@ -19,27 +19,27 @@
     2.4                     | NONE => [th])
     2.5              | _ => [th]
     2.6    in case concl_of th of
     2.7 -         Const("Trueprop",_) $ P =>
     2.8 +         Const(@{const_name Trueprop},_) $ P =>
     2.9              (case P of
    2.10                   Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
    2.11 -               | Const("True",_)         => []
    2.12 -               | Const("False",_)        => []
    2.13 +               | Const(@{const_name True},_)         => []
    2.14 +               | Const(@{const_name False},_)        => []
    2.15                 | A => tryrules conn_pairs A)
    2.16         | _                       => [th]
    2.17    end;
    2.18  
    2.19  (*Analyse a rigid formula*)
    2.20  val ZF_conn_pairs =
    2.21 -  [("Ball",     [@{thm bspec}]),
    2.22 -   ("All",      [@{thm spec}]),
    2.23 -   ("op -->",   [@{thm mp}]),
    2.24 -   ("op &",     [@{thm conjunct1}, @{thm conjunct2}])];
    2.25 +  [(@{const_name Ball}, [@{thm bspec}]),
    2.26 +   (@{const_name All}, [@{thm spec}]),
    2.27 +   (@{const_name "op -->"}, [@{thm mp}]),
    2.28 +   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
    2.29  
    2.30  (*Analyse a:b, where b is rigid*)
    2.31  val ZF_mem_pairs =
    2.32 -  [("Collect",  [@{thm CollectD1}, @{thm CollectD2}]),
    2.33 -   (@{const_name Diff},     [@{thm DiffD1}, @{thm DiffD2}]),
    2.34 -   (@{const_name Int},   [@{thm IntD1}, @{thm IntD2}])];
    2.35 +  [(@{const_name Collect}, [@{thm CollectD1}, @{thm CollectD2}]),
    2.36 +   (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
    2.37 +   (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
    2.38  
    2.39  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    2.40