theory Conversions
imports Main
begin

section {* Basic conversions *}

ML {* Conv.all_conv : cterm -> thm *}
ML {* Conv.all_conv *}

text {* Always succeeds *}

ML {* Conv.all_conv @{cterm "42::int"} *}

text {* Always fails *}

(*
ML {* Conv.no_conv @{cterm "42::int"} *}
*)

text {* Rewrite with a single rule *}

ML {*
val rev_Cons = mk_meta_eq @{thm rev.simps(2)}
*}

ML {*
Conv.rewr_conv rev_Cons @{cterm "rev [1::int, 2]"}
*}



section {* Combining conversions (``conversionals'') *}

text {* Sequencing *}

ML {*
val add_0_right = mk_meta_eq @{thm monoid_add_class.add_0_right}
*}

ML {*
val mult_1_left = mk_meta_eq @{thm monoid_mult_class.mult_1_left}
*}

ML {*
(Conv.rewr_conv add_0_right then_conv Conv.rewr_conv mult_1_left)
@{cterm "((1::int) * x) + 0"}
*}

text {* Alternative *}

ML {*
val rev_Nil = mk_meta_eq @{thm rev.simps(1)}
*}

ML {*
(Conv.rewr_conv rev_Nil else_conv Conv.rewr_conv rev_Cons)
@{cterm "rev [1::int, 2, 3]"}
*}

text {* Try conversion (yields reflexivity instead of exception) *}

ML {*
Conv.try_conv (Conv.rewr_conv rev_Nil) @{cterm "[1::int, 2]"}
*}

text {* Descend into subterms *}

ML {*
Conv.combination_conv
  (Conv.combination_conv
    Conv.all_conv
    (Conv.rewr_conv rev_Cons))
  (Conv.rewr_conv rev_Cons)
  @{cterm "rev [1::int, 2] @ rev [3, 4]"}
*}

ML {*
Conv.combination_conv
  (Conv.arg_conv
    (Conv.rewr_conv rev_Cons))
  (Conv.rewr_conv rev_Cons)
  @{cterm "rev [1::int, 2] @ rev [3, 4]"}
*}

ML {*
Conv.abs_conv (fn (v, ctxt) =>
  Conv.abs_conv (fn (v', ctxt') =>
    Conv.rewr_conv rev_Cons) ctxt)
  @{context}
  @{cterm "\<lambda>x y. rev [x, y]"}
*}



section {* Simple bottom-up rewriting, using Isabelle's conversion library *}

text {* Descend into immediate subterms *}

ML {*
fun subc conv ctxt = 
  Conv.comb_conv (conv ctxt) else_conv
  Conv.abs_conv (conv o snd) ctxt else_conv
  Conv.all_conv;
*}

text {* The ct argument is necessary to avoid nontermination! *}

ML {*
fun botc conv ctxt ct =
  (subc (botc conv) ctxt then_conv
   Conv.try_conv (conv then_conv botc conv ctxt)) ct
*}

text {* Running example: reversing lists *}

ML {*
val eqns = map mk_meta_eq (@{thms "append.simps"} @ @{thms "rev.simps"});
*}

ML {*
val rev_int = @{cterm "rev :: int list \<Rightarrow> int list"};
*}

text {* Produce lists of length i *}

ML {*
fun mk_upto thy i = Thm.cterm_of thy (HOLogic.mk_list HOLogic.intT
  (map (HOLogic.mk_number HOLogic.intT) (1 upto i)));
*}

ML {*
val ct = Thm.capply rev_int (mk_upto @{theory} 100)
*}

text {* Fully rewrite the term (slow, i.e. 40 secs on my laptop) *}

ML {*
timeit (fn () =>
  botc (Conv.first_conv (map Conv.rewr_conv eqns)) @{context} ct)
*}

text {* Also rewrites inside quantifiers, thanks to abs_conv *}

ML {*
botc (Conv.first_conv (map Conv.rewr_conv eqns)) @{context}
  @{cterm "\<forall>x y z. P (rev [x, y, z])"}
*}



section {* Using exceptions for signalling unchanged terms *}

text {*
  Motivation: avoid unnecessary applications of reflexivity
*}

ML {*
infix 1 then_conv';
infix 0 else_conv';

exception Fail;
exception Unchanged;

fun (cv1 else_conv' cv2) ct =
  cv1 ct handle Fail => cv2 ct;

fun all_conv' ct = raise Unchanged;

fun no_conv' ct = raise Fail;

fun try_conv' cv ct = cv ct handle Fail => raise Unchanged;

fun (cv1 then_conv' cv2) ct =
  let val eq = cv1 ct
  in Thm.transitive eq (cv2 (Thm.rhs_of eq)) handle Unchanged => eq
  end handle Unchanged => cv2 ct;

fun first_conv' cvs = fold_rev (curry op else_conv') cvs no_conv';

fun comb_conv' cv ct =
  let val (ct1, ct2) = Thm.dest_comb ct
  in
    let val eq1 = cv ct1
    in Thm.combination eq1 (cv ct2) handle Unchanged =>
       Thm.combination eq1 (Thm.reflexive ct2)
    end handle Unchanged =>
    let val eq2 = cv ct2
    in Thm.combination (Thm.reflexive ct1) eq2 end
  end handle CTERM _ => raise Fail;

fun abs_conv' cv ctxt ct =
  (case Thm.term_of ct of
    Abs (x, _, _) =>
      let
        val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
        val (v, ct') = Thm.dest_abs (SOME u) ct;
        val eq = cv (v, ctxt') ct';
      in Thm.abstract_rule x v eq end
  | _ => raise Fail);

fun subc' conv ctxt = 
  comb_conv' (conv ctxt) else_conv'
  abs_conv' (conv o snd) ctxt else_conv'
  all_conv';

fun botc' conv ctxt ct =
  (subc' (botc' conv) ctxt then_conv'
   try_conv' (conv then_conv' botc' conv ctxt)) ct

fun rewr_conv' rule ct =
  Conv.rewr_conv rule ct handle CTERM _ => raise Fail;
*}

text {* Fully rewrite the term (32 secs on my laptop) *}

ML {*
timeit (fn () =>
  botc' (first_conv' (map rewr_conv' eqns)) @{context} ct)
*}

ML {*
botc' (first_conv' (map rewr_conv' eqns)) @{context}
  @{cterm "\<forall>x y z. P (rev [x, y, z])"}
*}



section {* Bottom-up writing using skeletons *}

text {*
  Motivation: avoid re-inspecting terms that are already
  in normal form
  Skeleton = rhs of last rewrite rule applied
  decomposed in parallel with the term to be normalized
  if skeleton is a variable, then the corresponding
  term must already be in normal form.
*}

ML {*
infix 1 then_conv'';

fun (cv1 then_conv'' cv2) cts =
  let val (eq1, skel1) = cv1 cts
  in 
    let val (eq2, skel2) = cv2 (Thm.rhs_of eq1, skel1)
    in (Thm.transitive eq1 eq2, skel2) end handle Unchanged => (eq1, skel1)
  end handle Unchanged => cv2 cts;

val dummy_skel = Bound 0;

fun comb_conv'' cv (ct, skel) =
  let
    val (ct1, ct2) = Thm.dest_comb ct
    val (skel1, skel2) = (case skel of
        skel1 $ skel2 => (skel1, skel2)
      | _ => (dummy_skel, dummy_skel));
  in
    let val (eq1, skel1') = cv (ct1, skel1)
    in 
      let val (eq2, skel2') = cv (ct2, skel2)
      in (Thm.combination eq1 eq2, skel1' $ skel2') end
      handle Unchanged =>
      (Thm.combination eq1 (Thm.reflexive ct2), skel1' $ skel2)
    end handle Unchanged =>
    let val (eq2, skel2') = cv (ct2, skel2)
    in (Thm.combination (Thm.reflexive ct1) eq2, skel1 $ skel2') end
  end handle CTERM _ => raise Fail;

fun abs_conv'' cv ctxt (ct, skel) =
  (case Thm.term_of ct of
    Abs (x, T, _) =>
      let
        val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
        val (v, ct') = Thm.dest_abs (SOME u) ct;
        val skel' = (case skel of
            Abs (_, _, skel') => skel'
          | _ => dummy_skel)
        val (eq, skel'') = cv (v, ctxt') (ct', skel');
      in (Thm.abstract_rule x v eq, Abs (x, T, skel'')) end
  | _ => raise Fail);

fun subc'' conv ctxt =
  comb_conv'' (conv ctxt) else_conv'
  abs_conv'' (conv o snd) ctxt else_conv'
  all_conv';

fun botc'' conv ctxt (_, Var _) = raise Unchanged
  | botc'' conv ctxt cts =
      (subc'' (botc'' conv) ctxt then_conv''
       try_conv' (conv then_conv'' botc'' conv ctxt)) cts

fun rewr_conv'' rule (ct, _) =
  (Conv.rewr_conv rule ct, term_of (Thm.rhs_of rule))
  handle CTERM _ => raise Fail;
*}

text {* Fully rewrite the term (1.5 secs on my laptop) *}

ML {*
timeit (fn () =>
  fst (botc'' (first_conv' (map rewr_conv'' eqns)) @{context} (ct, dummy_skel)))
*}

ML {*
fst (botc'' (first_conv' (map rewr_conv'' eqns)) @{context}
  (@{cterm "\<forall>x y z. P (rev [x, y, z])"}, dummy_skel))
*}



section {* The simplifier *}

text {*
  The simplifier is a conversion itself, using many of
  the techniques just described.
*}

ML {*
Simplifier.rewrite (HOL_basic_ss addsimps eqns) ct
*}

ML {*
Simplifier.rewrite @{simpset}
  @{cterm "\<And>(x::int) (y::int). P x \<Longrightarrow> x = 42 \<Longrightarrow> Q x \<Longrightarrow> R (y + 0) \<Longrightarrow> S (1 * x)"}
*}

ML {*
Simplifier.asm_rewrite @{simpset}
  @{cterm "\<And>(x::int) (y::int). P x \<Longrightarrow> x = 42 \<Longrightarrow> Q x \<Longrightarrow> R (y + 0) \<Longrightarrow> S (1 * x)"}
*}

ML {*
Simplifier.full_rewrite @{simpset}
  @{cterm "\<And>(x::int) (y::int). P x \<Longrightarrow> x = 42 \<Longrightarrow> Q x \<Longrightarrow> R (y + 0) \<Longrightarrow> S (1 * x)"}
*}

ML {*
Simplifier.asm_full_rewrite @{simpset}
  @{cterm "\<And>(x::int) (y::int). P x \<Longrightarrow> x = 42 \<Longrightarrow> Q x \<Longrightarrow> R (y + 0) \<Longrightarrow> S (1 * x)"}
*}

ML {*
Simplifier.asm_lr_rewrite @{simpset}
  @{cterm "\<And>(x::int) (y::int). P x \<Longrightarrow> x = 42 \<Longrightarrow> Q x \<Longrightarrow> R (y + 0) \<Longrightarrow> S (1 * x)"}
*}

section {* Simplification procedures *}

text {*
  A simplification procedure is a function of type
  @{ML_type "cterm -> thm option"}
  It can be used to prove rewrite rules on-the-fly.
*}

text {* Example 1: One-point rules *}

text {*
  Problem: how to rewrite
  @{term "\<And>x y z. P y \<Longrightarrow> y = t \<Longrightarrow> Q y"}
  to
  @{term "\<And>x z. P t \<Longrightarrow> Q t"}
*}

lemma meta_onepoint1: "(\<And>x. x = t \<Longrightarrow> PROP P x) \<equiv> PROP P t"
proof
  assume R: "\<And>x. x = t \<Longrightarrow> PROP P x"
  show "PROP P t" by (rule R [OF refl])
next
  fix x assume "PROP P t" "x = t"
  then show "PROP P x" by simp
qed

lemma meta_onepoint2: "(\<And>x. t = x \<Longrightarrow> PROP P x) \<equiv> PROP P t"
proof
  assume R: "\<And>x. t = x \<Longrightarrow> PROP P x"
  show "PROP P t" by (rule R [OF refl])
next
  fix x assume "PROP P t" "t = x"
  then show "PROP P x" by simp
qed

lemmas meta_onepoint = meta_onepoint1 meta_onepoint2

text {*
  Note: only works with formulae like
  @{term "\<And>x z y. y = t \<Longrightarrow> P y \<Longrightarrow> Q y"}
  but not
  @{term "\<And>x y z. P y \<Longrightarrow> y = t \<Longrightarrow> Q y"}
  Solution: reorder quantifiers and premises
*}

ML {*
Simplifier.rewrite
  (HOL_basic_ss addsimps @{thms meta_onepoint})
  @{cterm "\<And>x z y. y = t \<Longrightarrow> P y \<Longrightarrow> Q y"}
*}

ML {*
Simplifier.rewrite
  (HOL_basic_ss addsimps @{thms meta_onepoint})
  @{cterm "\<And>x y z. P y \<Longrightarrow> y = t \<Longrightarrow> Q y"}
*}

text {* Move parameters to the right *}

ML {*
fun swap_params_conv ctxt i j cv =
  let
    fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
      | conv1 k ctxt =
          Conv.rewr_conv @{thm swap_params} then_conv
          Conv.forall_conv (conv1 (k-1) o snd) ctxt
    fun conv2 0 ctxt = conv1 j ctxt
      | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt
  in conv2 i ctxt end;
*}

ML {*
swap_params_conv @{context} 2 3 (K Conv.all_conv)
  @{cterm "\<And>a b c d e f. P a b c d e f"}
*}

text {* Move premises to the left *}

ML {*
fun swap_prems_conv 0 = Conv.all_conv
  | swap_prems_conv i =
      Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
      Conv.rewr_conv Drule.swap_prems_eq
*}

ML {*
swap_prems_conv 3
  @{cterm "A \<Longrightarrow> B \<Longrightarrow> C \<Longrightarrow> D \<Longrightarrow> E \<Longrightarrow> F"}
*}

text {* Find out which equation to move *}

ML {*
fun find_eq t =
  let
    val l = length (Logic.strip_params t);
    val Hs = Logic.strip_assums_hyp t;
    fun find (i, (_ $ (Const ("op =", _) $ Bound j $ _))) = SOME (i, j)
      | find (i, (_ $ (Const ("op =", _) $ _ $ Bound j))) = SOME (i, j)
      | find _ = NONE
  in
    case get_first find (map_index I Hs) of
      NONE => NONE
    | SOME (0, 0) => NONE
    | SOME (i, j) => SOME (i, l - j - 1, j)
  end;
*}

ML {*
find_eq @{term "\<And>x y z. P y \<Longrightarrow> y = t \<Longrightarrow> Q y"}
*}

text {* Turn it into a simproc *}

ML {*
fun mk_rrule ctxt ct = case find_eq (term_of ct) of
    NONE => NONE
  | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct);
*}

ML {*
val rearrange_eqs_simproc =
  Simplifier.simproc @{theory} "rearrange_eqs" ["all t"] (fn thy => fn ss => fn t =>
    mk_rrule (Simplifier.the_context ss) (cterm_of thy t))
*}

ML {*
Simplifier.rewrite
  (HOL_basic_ss addsimps @{thms meta_onepoint}
     addsimprocs [rearrange_eqs_simproc])
  @{cterm "\<And>x y z. P y \<Longrightarrow> y = t \<Longrightarrow> Q y"}
*}

subsection {* Example 2: Simplifying set comprehensions *}

text {*
  Problem: How to simplify
  @{term "{(x, y, z). (x, y, z) \<in> S}"}
  to
  @{term S}
*}

ML {* @{thm Collect_mem_eq} *}

text {*
  Note: does not work with pairs
*}

ML {*
Simplifier.rewrite
  (HOL_basic_ss addsimps @{thms Collect_mem_eq})
  @{cterm "P {x. x \<in> S}"}
*}

ML {*
Simplifier.rewrite
  (HOL_basic_ss addsimps @{thms Collect_mem_eq})
  @{cterm "P {(x, y). (x, y) \<in> S}"}
*}

text {*
  Write a simproc to prove
  @{term "{(x, y). (x, y) \<in> S} \<equiv> S"}
*}

lemma test: "{(x, y). (x, y) \<in> S} \<equiv> S"
  apply (rule eq_reflection)
  apply (rule subset_antisym)
  apply (rule subsetI)
  apply (drule CollectD)
  apply (simp only: split_paired_all split_conv)
  apply (rule subsetI)
  apply (rule CollectI)
  apply (simp only: split_paired_all split_conv)
  done

text {* The same in ML *}

ML {*
let
  val simp = full_simp_tac
    (HOL_basic_ss addsimps [split_paired_all, split_conv]) 1
in
  Goal.prove @{context} [] []
    @{term "{(x, y). (x, y) \<in> S} \<equiv> S"}
    (K (EVERY
      [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
       rtac subsetI 1, dtac CollectD 1, simp,
       rtac subsetI 1, rtac CollectI 1, simp]))
end
*}

ML {*
val (u, Ts, ps) = HOLogic.strip_split
  @{term "\<lambda>(x, y). (x, y) \<in> S"}
*}

ML {*
val collect_mem_simproc =
  Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
    fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
         let val (u, Ts, ps) = HOLogic.strip_split t
         in case u of
           (c as Const ("op :", _)) $ q $ S' =>
             (case try (HOLogic.dest_tuple' ps) q of
                NONE => NONE
              | SOME ts =>
                  if not (loose_bvar (S', 0)) andalso
                    ts = map Bound (length ps downto 0)
                  then
                    let val simp = full_simp_tac (Simplifier.inherit_context ss
                      (HOL_basic_ss addsimps [split_paired_all, split_conv])) 1
                    in
                      SOME (Goal.prove (Simplifier.the_context ss) [] []
                        (Const ("==", T --> T --> propT) $ S $ S')
                        (K (EVERY
                          [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
                           rtac subsetI 1, dtac CollectD 1, simp,
                           rtac subsetI 1, rtac CollectI 1, simp])))
                    end
                  else NONE)
         | _ => NONE
         end
     | _ => NONE);
*}

ML {*
Simplifier.rewrite
  (HOL_basic_ss addsimps @{thms Collect_mem_eq}
     addsimprocs [collect_mem_simproc])
  @{cterm "P {(x, y). (x, y) \<in> S}"}
*}

end