# HG changeset patch
# User wenzelm
# Date 1170097094 -3600
# Node ID 23bd1ed32ac056d10ab5ebc724d865229874bed8
# Parent  33da3a55c00e94ce4a05ac5306b57a7ae27e9e77
proper simproc_setup;
tuned ML setup;

diff -r 33da3a55c00e -r 23bd1ed32ac0 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Mon Jan 29 19:58:14 2007 +0100
+++ b/src/HOL/ex/Binary.thy	Mon Jan 29 19:58:14 2007 +0100
@@ -20,6 +20,30 @@
     "bit n True = 2 * n + 1"
   unfolding bit_def by simp_all
 
+ML {*
+  fun dest_bit (Const ("False", _)) = 0
+    | dest_bit (Const ("True", _)) = 1
+    | dest_bit t = raise TERM ("dest_bit", [t]);
+
+  fun dest_binary (Const ("HOL.zero", Type ("nat", _))) = 0
+    | dest_binary (Const ("HOL.one", Type ("nat", _))) = 1
+    | dest_binary (Const ("Binary.bit", _) $ bs $ b) =
+        2 * dest_binary bs + IntInf.fromInt (dest_bit b)
+    | dest_binary t = raise TERM ("dest_binary", [t]);
+
+  fun mk_bit 0 = @{term False}
+    | mk_bit 1 = @{term True}
+    | mk_bit _ = raise TERM ("mk_bit", []);
+
+  fun mk_binary 0 = @{term "0::nat"}
+    | mk_binary 1 = @{term "1::nat"}
+    | mk_binary n =
+        if n < 0 then raise TERM ("mk_binary", [])
+        else
+          let val (q, r) = IntInf.divMod (n, 2)
+          in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;
+*}
+
 
 subsection {* Direct operations -- plain normalization *}
 
@@ -87,92 +111,78 @@
 qed
 
 ML {*
-  fun dest_bit (Const ("False", _)) = 0
-    | dest_bit (Const ("True", _)) = 1
-    | dest_bit t = raise TERM ("dest_bit", [t]);
-
-  fun dest_binary (Const ("HOL.zero", Type ("nat", _))) = 0
-    | dest_binary (Const ("HOL.one", Type ("nat", _))) = 1
-    | dest_binary (Const ("Binary.bit", _) $ bs $ b) =
-        2 * dest_binary bs + IntInf.fromInt (dest_bit b)
-    | dest_binary t = raise TERM ("dest_binary", [t]);
+local
+  infix ==;
+  val op == = Logic.mk_equals;
+  fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
+  fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
 
-  fun mk_bit 0 = @{term False}
-    | mk_bit 1 = @{term True}
-    | mk_bit _ = raise TERM ("mk_bit", []);
-
-  fun mk_binary 0 = @{term "0::nat"}
-    | mk_binary 1 = @{term "1::nat"}
-    | mk_binary n =
-        if n < 0 then raise TERM ("mk_binary", [])
-        else
-          let val (q, r) = IntInf.divMod (n, 2)
-          in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;
-*}
-
-ML {*
-local
   val binary_ss = HOL_basic_ss addsimps @{thms binary_simps};
   fun prove ctxt prop =
     Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
 
-  infix ==;
-  val op == = Logic.mk_equals;
-
-  fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
-  fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
-
-
-  exception FAIL;
-  fun the_arg t = (t, dest_binary t handle TERM _ => raise FAIL);
+  fun binary_proc proc ss ct =
+    (case Thm.term_of ct of
+      _ $ t $ u =>
+      (case try (pairself (`dest_binary)) (t, u) of
+        SOME args => proc (Simplifier.the_context ss) args
+      | NONE => NONE)
+    | _ => NONE);
+in
 
-  val read = Thm.cterm_of @{theory} o Sign.read_term @{theory};
-  fun mk_proc name pat proc = Simplifier.mk_simproc' name [read pat]
-    (fn ss => fn ct =>
-      (case Thm.term_of ct of
-        _ $ t $ u =>
-          (SOME (proc (Simplifier.the_context ss) (the_arg t) (the_arg u)) handle FAIL => NONE)
-      | _ => NONE));
+val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
+  let val k = n - m in
+    if k >= 0 then
+      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
+    else
+      SOME (@{thm binary_less_eq(2)} OF
+        [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
+  end);
 
-
-  val less_eq_simproc = mk_proc "binary_nat_less_eq" "?m <= (?n::nat)"
-    (fn ctxt => fn (t, m) => fn (u, n) =>
-      let val k = n - m in
-        if k >= 0 then @{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))]
-        else @{thm binary_less_eq(2)} OF
-          [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))]
-      end);
+val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
+  let val k = m - n in
+    if k >= 0 then
+      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
+    else
+      SOME (@{thm binary_less(2)} OF
+        [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
+  end);
 
-  val less_simproc = mk_proc "binary_nat_less" "?m < (?n::nat)"
-    (fn ctxt => fn (t, m) => fn (u, n) =>
-      let val k = m - n in
-        if k >= 0 then @{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))]
-        else @{thm binary_less(2)} OF
-          [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))]
-      end);
+val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
+  let val k = m - n in
+    if k >= 0 then
+      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
+    else
+      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
+  end);
 
-  val diff_simproc = mk_proc "binary_nat_diff" "?m - (?n::nat)"
-    (fn ctxt => fn (t, m) => fn (u, n) =>
-      let val k = m - n in
-        if k >= 0 then @{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))]
-        else @{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))]
-      end);
+fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
+  if n = 0 then NONE
+  else
+    let val (k, l) = IntInf.divMod (m, n)
+    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
+
+end;
+*}
 
-  fun divmod_proc rule ctxt (t, m) (u, n) =
-    if n = 0 then raise FAIL
-    else
-      let val (k, l) = IntInf.divMod (m, n)
-      in rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))] end;
+simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *}
+simproc_setup binary_nat_less ("m < (n::nat)") = {* K less_proc *}
+simproc_setup binary_nat_diff ("m - (n::nat)") = {* K diff_proc *}
+simproc_setup binary_nat_div ("m div (n::nat)") = {* K (divmod_proc @{thm binary_divmod(1)}) *}
+simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
 
-  val div_simproc = mk_proc "binary_nat_div" "?m div (?n::nat)"
-    (divmod_proc @{thm binary_divmod(1)});
-  val mod_simproc = mk_proc "binary_nat_mod" "?m mod (?n::nat)"
-    (divmod_proc @{thm binary_divmod(2)});
-in
-  val binary_nat_simprocs =
-    [less_eq_simproc, less_simproc, diff_simproc, div_simproc, mod_simproc];
-end
-*}
+method_setup binary_simp = {*
+  Method.no_args (Method.SIMPLE_METHOD'
+    (full_simp_tac
+      (HOL_basic_ss
+        addsimps @{thms binary_simps}
+        addsimprocs
+         [@{simproc binary_nat_less_eq},
+          @{simproc binary_nat_less},
+          @{simproc binary_nat_diff},
+          @{simproc binary_nat_div},
+          @{simproc binary_nat_mod}])))
+*} "binary simplification"
 
 
 subsection {* Concrete syntax *}
@@ -198,12 +208,6 @@
 
 subsection {* Examples *}
 
-method_setup binary_simp = {*
-  Method.no_args (Method.SIMPLE_METHOD'
-    (full_simp_tac (HOL_basic_ss addsimps @{thms binary_simps} addsimprocs binary_nat_simprocs)))
-*} "binary simplification"
-
-
 lemma "$6 = 6"
   by (simp add: bit_simps)