src/HOL/Library/Cancellation/cancel_data.ML
author wenzelm
Mon, 13 Apr 2020 22:08:14 +0200
changeset 71751 abf3e80bd815
parent 69593 3dda49e08b9d
child 74633 994a2b9daf1d
permissions -rw-r--r--
tuned NEWS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65367
83c30e290702 tuned headers;
wenzelm
parents: 65029
diff changeset
     1
(*  Title:      HOL/Library/Cancellation/cancel_data.ML
83c30e290702 tuned headers;
wenzelm
parents: 65029
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     3
    Author:     Mathias Fleury, MPII
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     4
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     5
Datastructure for the cancelation simprocs.
65367
83c30e290702 tuned headers;
wenzelm
parents: 65029
diff changeset
     6
*)
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     7
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     8
signature CANCEL_DATA =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     9
sig
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    10
  val mk_sum : typ -> term list -> term
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    11
  val dest_sum : term -> term list
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    12
  val mk_coeff : int * term -> term
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    13
  val dest_coeff : term -> int * term
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    14
  val find_first_coeff : term -> term list -> int * term list
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    15
  val trans_tac : Proof.context -> thm option -> tactic
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    16
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    17
  val norm_ss1 : simpset
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    18
  val norm_ss2: simpset
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    19
  val norm_tac: Proof.context -> tactic
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    20
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    21
  val numeral_simp_tac : Proof.context -> tactic
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    22
  val simplify_meta_eq : Proof.context -> thm -> thm
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    23
  val prove_conv : tactic list -> Proof.context -> thm list -> term * term -> thm option
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    24
end;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    25
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    26
structure Cancel_Data : CANCEL_DATA =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    27
struct
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    28
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    29
(*** Utilities ***)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    30
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    31
(*No reordering of the arguments.*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    32
fun fast_mk_iterate_add (n, mset) =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    33
  let val T = fastype_of mset
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    34
  in
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
    35
    Const (\<^const_name>\<open>iterate_add\<close>, \<^typ>\<open>nat\<close> --> T --> T) $ n $ mset
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    36
  end;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    37
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    38
(*iterate_add is not symmetric, unlike multiplication over natural numbers.*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    39
fun mk_iterate_add (t, u) =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
    40
  (if fastype_of t = \<^typ>\<open>nat\<close> then (t, u) else (u, t))
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    41
  |> fast_mk_iterate_add;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    42
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    43
(*Maps n to #n for n = 1, 2*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    44
val numeral_syms =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    45
  map (fn th => th RS sym) @{thms numeral_One numeral_2_eq_2 numeral_1_eq_Suc_0};
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    46
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    47
val numeral_sym_ss =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
    48
  simpset_of (put_simpset HOL_basic_ss \<^context> addsimps numeral_syms);
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    49
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    50
fun mk_number 1 = HOLogic.numeral_const HOLogic.natT $ HOLogic.one_const
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    51
  | mk_number n = HOLogic.mk_number HOLogic.natT n;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    52
fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    53
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    54
fun find_first_numeral past (t::terms) =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    55
    ((dest_number t, t, rev past @ terms)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    56
    handle TERM _ => find_first_numeral (t::past) terms)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    57
  | find_first_numeral _ [] = raise TERM("find_first_numeral", []);
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    58
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
    59
fun typed_zero T = Const (\<^const_name>\<open>Groups.zero\<close>, T);
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    60
fun typed_one T = HOLogic.numeral_const T $ HOLogic.one_const
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
    61
val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Groups.plus\<close>;
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    62
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    63
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero.*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    64
fun mk_sum T [] = typed_zero T
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    65
  | mk_sum _ [t,u] = mk_plus (t, u)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    66
  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    67
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
    68
val dest_plus = HOLogic.dest_bin \<^const_name>\<open>Groups.plus\<close> dummyT;
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    69
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    70
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    71
(*** Other simproc items ***)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    72
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    73
val bin_simps =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    74
  (@{thm numeral_One} RS sym) ::
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    75
  @{thms add_numeral_left diff_nat_numeral diff_0_eq_0 mult_numeral_left(1)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    76
      if_True if_False not_False_eq_True nat_0 nat_numeral nat_neg_numeral iterate_add_simps(1)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    77
      iterate_add_empty arith_simps rel_simps of_nat_numeral};
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    78
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    79
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    80
(*** CancelNumerals simprocs ***)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    81
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    82
val one = mk_number 1;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    83
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    84
fun mk_prod T [] = typed_one T
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    85
  | mk_prod _ [t] = t
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    86
  | mk_prod T (t :: ts) = if t = one then mk_prod T ts else mk_iterate_add (t, mk_prod T ts);
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    87
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
    88
val dest_iterate_add = HOLogic.dest_bin \<^const_name>\<open>iterate_add\<close> dummyT;
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    89
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    90
fun dest_iterate_adds t =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    91
  let val (t,u) = dest_iterate_add t in
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    92
    t :: dest_iterate_adds u end
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    93
  handle TERM _ => [t];
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    94
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    95
fun mk_coeff (k,t) = mk_iterate_add (mk_number k, t);
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    96
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    97
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    98
fun dest_coeff t =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    99
  let
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   100
    val T = fastype_of t
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   101
    val ts = sort Term_Ord.term_ord (dest_iterate_adds t);
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   102
    val (n, _, ts') =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   103
      find_first_numeral [] ts
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   104
      handle TERM _ => (1, one, ts);
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   105
  in (n, mk_prod T ts') end;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   106
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   107
(*Find first coefficient-term THAT MATCHES u*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   108
fun find_first_coeff _ _ [] = raise TERM("find_first_coeff", [])
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   109
  | find_first_coeff past u (t::terms) =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   110
    let val (n,u') = dest_coeff t in
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   111
      if u aconv u' then (n, rev past @ terms) else find_first_coeff (t::past) u terms end
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   112
    handle TERM _ => find_first_coeff (t::past) u terms;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   113
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   114
(*
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   115
  Split up a sum into the list of its constituent terms.
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   116
*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   117
fun dest_summation (t, ts) =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   118
    let val (t1,t2) = dest_plus t in
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   119
      dest_summation (t1, dest_summation (t2, ts)) end
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   120
    handle TERM _ => t :: ts;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   121
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   122
fun dest_sum t = dest_summation (t, []);
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   123
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
   124
val rename_numerals = simplify (put_simpset numeral_sym_ss \<^context>) o Thm.transfer \<^theory>;
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   125
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   126
(*Simplify \<open>iterate_add (Suc 0) n\<close>, \<open>iterate_add n (Suc 0)\<close>, \<open>n+0\<close>, and \<open>0+n\<close> to \<open>n\<close>*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   127
val add_0s  = map rename_numerals @{thms monoid_add_class.add_0_left monoid_add_class.add_0_right};
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   128
val mult_1s = map rename_numerals @{thms iterate_add_1 iterate_add_simps(2)[of 0]};
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   129
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   130
(*And these help the simproc return False when appropriate. We use the same list as the
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   131
simproc for natural numbers, but adapted.*)
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   132
fun contra_rules ctxt =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
   133
  @{thms le_zero_eq}  @ Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_eq_elim\<close>;
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   134
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   135
fun simplify_meta_eq ctxt =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   136
  Arith_Data.simplify_meta_eq
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   137
    (@{thms numeral_1_eq_Suc_0 Nat.add_0_right
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   138
         mult_0 mult_0_right mult_1 mult_1_right iterate_add_Numeral1 of_nat_numeral
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   139
         monoid_add_class.add_0_left iterate_add_simps(1) monoid_add_class.add_0_right
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   140
         iterate_add_Numeral1} @
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   141
     contra_rules ctxt) ctxt;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   142
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   143
val mk_sum = mk_sum;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   144
val dest_sum = dest_sum;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   145
val mk_coeff = mk_coeff;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   146
val dest_coeff = dest_coeff;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   147
val find_first_coeff = find_first_coeff [];
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   148
val trans_tac = Numeral_Simprocs.trans_tac;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   149
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   150
val norm_ss1 =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
   151
  simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> addsimps
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   152
    numeral_syms @ add_0s @ mult_1s @ @{thms ac_simps iterate_add_simps});
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   153
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   154
val norm_ss2 =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
   155
  simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context> addsimps
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   156
    bin_simps @
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   157
    @{thms ac_simps});
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   158
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   159
fun norm_tac ctxt =
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   160
  ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   161
  THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt));
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   162
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   163
val mset_simps_ss =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 65367
diff changeset
   164
  simpset_of (put_simpset HOL_basic_ss \<^context> addsimps bin_simps);
65029
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   165
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   166
fun numeral_simp_tac ctxt = ALLGOALS (simp_tac (put_simpset mset_simps_ss ctxt));
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   167
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   168
val simplify_meta_eq = simplify_meta_eq;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   169
val prove_conv = Arith_Data.prove_conv;
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   170
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   171
end
00731700e54f cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
   172