(*  Title:      HOL/Imperative_HOL/ex/Congproc_Ex.thy
    Author:     Norbert Schirmer, Apple, 2024
*)

section ‹Examples for congruence procedures (congprocs)›

theory Congproc_Ex
  imports "../Imperative_HOL"
begin

text ‹The simplifier works bottom up, which means that when invoked on a (compound) term it first
  into the subterms to normalise those and then works its way up to the head of the term
  to apply rewrite rules for the current redex (reducible expression) it encounters on the
  up. Descending into the term can be influenced by congruence rules. Before descending into the
  the simplifier checks for a congruence rule for the head of the term. If it finds one
  behaves according to that rule, otherwise the simplifier descends into each subterm subsequently.

  rewrite rules can be complemented with simplification procedures (simprocs) to get even
  programmatic control, congruence rules can be complemented with congruence
  (congprocs):

 ▪ Congprocs share the same ML signature as simprocs and provide a similar interface in
 Isabelle/ML as well as Isabelle/Isar:
 @{ML_type "morphism -> Proof.context -> thm option"}
 ▪ Congprocs are triggered by associated term patterns (just like simprocs) not just the head constant
 (which is the case for congruence rules). Like simprocs, congprocs are managed in a term net.
 ▪ Congprocs have precedence over congruence rules (unlike simprocs)
 ▪ In case the term net selects multiple candidates,
 the one with the more specific term pattern is tried first. A pattern
 ‹p1› is considered more specific than ‹p2› if ‹p2› matches ‹p1› but not vice versa.
 ▪ To avoid surprises the theorems returned by a congproc should follow the structure of
 ordinary congruence rule. Either the conclusion should return an equation where the head of the
 left hand side and right hand side coincide, or the right hand side is already in normal form.
 Otherwise, simplification might skip some relevant subterms or do repeated simplification of
 some subterms. Some fine points are illustrated by the following examples.
 ›


subsection ‹Congproc examples with if-then-else›

ML ‹
  assert expected eq = if (expected aconvc (Thm.rhs_of eq)) then eq else
 raise error ("unexpected: " ^ @{make_string} eq)

  assert_equiv expected eq =
 if Pattern.equiv @{theory} (Thm.term_of expected, Thm.term_of (Thm.rhs_of eq)) then eq else
 raise error ("unexpected: " ^ @{make_string} eq)

 ›
text ‹The standard setup uses @{thm if_weak_cong}. Only if the condition simplifies to
 term‹True› or term‹False› the branches are simplified.›
experiment fixes a::nat
begin
ML_val ‹
 {cterm "if a < 2 then a < 2 else ¬ a < 2"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "if a < 2 then a < 2 else ¬ a < 2"}
 ›
end

text ‹A congproc that supplies the 'strong' rule @{thm if_cong}›
simproc_setup passive congproc if_cong (‹if x then a else b›) = ‹
 (K (K (K (SOME @{thm if_cong [cong_format]}))))
 ›

experiment
begin
text ‹The congproc takes precedence over the cong rules›
declare [[simproc add: if_cong, simp_trace = false]]
ML_val ‹
 {cterm "if ((a::nat) < 2) then a < 2 else ¬ ((a::nat) < 2)"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm True}
 ›
end

text ‹When we replace the congruence rule with a congproc that provides the same
  we would expect that the result is the same.›

simproc_setup passive congproc if_weak_cong_bad (‹if x then a else b›) = ‹
 (K (K (K (SOME @{thm if_weak_cong [cong_format]}))))
 ›

experiment
begin

ML_val ‹
 {cterm "if True then (1::nat) + 2 else 2 + 3"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "Suc (Suc (Suc 0))"}
 ›


declare if_weak_cong [cong del]
declare [[simproc add: if_weak_cong_bad, simp_trace]]

ML_val ‹
 {cterm "if True then (1::nat) + 2 else 2 + 3"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "(1::nat) + 2"}
 ›
text ‹We do not get the same result. The then-branch is selected but not simplified.
  the simplifier works bottom up it can usually assume that the subterms are already in
 simp normal form'. So the simplifier avoids to revisit the then-branch when it applies
 {thm if_True}. However, the weak congruence rule
 {thm if_weak_cong} only simplifies the condition and neither branch.
  the simplifier analyses congruence rules this rule is classified as weak. Whenever a
  is simplified (for which a weak congruence rule is active) the simplifier deviates from its
 default behaviour and rewrites the result. However, the simplifier does not analyse the
 . To achieve the same result we can explicitly specify it as ∗‹weak›.›
end

simproc_setup passive weak_congproc if_weak_cong (‹if x then a else b›) = ‹
 (K (K (K (SOME @{thm if_weak_cong [cong_format]}))))
 ›

experiment
begin
declare if_weak_cong [cong del]
declare [[simproc add: if_weak_cong, simp_trace]]
ML_val ‹
 {cterm "if True then (1::nat) + 2 else 2 + 3"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "Suc (Suc (Suc 0))"}
 ›
end

text ‹Now some more ambitious congproc that combines the effect of @{thm if_weak_cong} and @{thm if_cong}.
  first simplifies the condition and depending on the result decides to either simplify only
  of the branches (in case the condition evaluates to term‹True› or term‹False›, or otherwise
  simplifies both branches.
 ›

lemma if_True_weak_cong:
  "P = True ==> x = x' ==> (if P then x else y) = (if True then x' else y)"
  by simp

lemma if_False_weak_cong:
  "P = False ==> y = y' ==> (if P then x else y) = (if False then x else y')"
  by simp

text ‹Note that we do not specify the congproc as ∗‹weak› as every relevant subterm is
 .›
simproc_setup passive congproc if_cong_canonical (‹if x then a else b›) = ‹
 let
 val if_True_weak_cong = @{thm if_True_weak_cong [cong_format]}
 val if_False_weak_cong = @{thm if_False_weak_cong [cong_format]}
 val if_cong = @{thm if_cong [cong_format]}
 in
 (K (fn ctxt => fn ct =>
 let
 val (_, [P, x, y]) = Drule.strip_comb ct
 val P_eq = Simplifier.asm_full_rewrite ctxt P
 val rhs = Thm.dest_equals_rhs (Thm.cprop_of P_eq)
 val rule = (case Thm.term_of rhs of
 @{term True} => if_True_weak_cong
 | @{term False} => if_False_weak_cong
 | _ => if_cong)
 in
 SOME (rule OF [P_eq])
 end))
 end
 ›

experiment
begin
declare if_weak_cong [cong del]
declare [[simproc add: if_cong_canonical, simp_trace]]
ML_val ‹
 {cterm "if True then (1::nat) + 2 else 2 + 3"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "Suc (Suc (Suc 0))"}
 ›
end

experiment
begin
declare if_weak_cong [cong del]
declare [[simproc add: if_cong_canonical, simp_trace]]
text ‹Canonical congruence behaviour:
 ▸ First condition is simplified to True
 ▸ Congruence rule is selected and then "then-branch" is simplified but "else-branch" is left untouched
 ▸ Congruence step is finished and now rewriting with @{thm if_True} is done.
  that there is no attempt to revisit the result, as congproc is not weak.›
ML_val ‹
 {cterm "if ((2::nat) < 3) then 22 + 2 else 21 + 1"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "24"}
 ›
end

experiment fixes a ::nat
begin
text ‹The weak congruence rule shows no effect.›
ML_val ‹
 {cterm "if a < b then a < b ⟶ True else ¬ a < b ⟶ True"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "if a < b then a < b ⟶ True else ¬ a < b ⟶ True"}
 ›

text ‹The congproc simplifies the term.›
declare if_weak_cong [cong del]
declare [[simproc add: if_cong_canonical, simp_trace]]
ML_val ‹
 {cterm "if a < b then a < b ⟶ True else ¬ a < b ⟶ True"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "True"}
 ›
end

text ‹Beware of congprocs that implement non-standard congruence rules, like:›

lemma if_True_cong: "P = True ==> (if P then x else y) = x"
  by simp

lemma if_False_cong: "P = False ==> (if P then x else y) = y"
  by simp

simproc_setup passive congproc if_cong_bad (‹if x then a else b›) = ‹
 let
 val if_True_cong = @{thm if_True_cong [cong_format]}
 val if_False_cong = @{thm if_False_cong [cong_format]}
 val if_cong = @{thm if_cong [cong_format]}
 in
 (K (fn ctxt => fn ct =>
 let
 val (_, [P, x, y]) = Drule.strip_comb ct
 val P_eq = Simplifier.asm_full_rewrite ctxt P
 val rhs = Thm.dest_equals_rhs (Thm.cprop_of P_eq)
 val rule = (case Thm.term_of rhs of
 @{term True} => if_True_cong
 | @{term False} => if_False_cong
 | _ => if_cong )
 in
 SOME (rule OF [P_eq])
 end))
 end
 ›

experiment
begin
declare if_weak_cong [cong del]
declare [[simproc add: if_cong_bad, simp_trace]]

ML_val ‹
 {cterm "if ((2::nat) < 3) then 22 + 2 else 21 + 1"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "24"}
 ›
text ‹The result is the same as with the canonical congproc. But when inspecting the ‹simp_trace›
  can observe some odd congruence behaviour:
 ▸ First condition is simplified to True
 ▸ Non-standard congruence rule @{thm if_True_cong} is selected which does
 not have the same head on the right hand side and simply gives back the "then-branch"
 ▸ Incidently simplification continues on the then-branch as there are simplification rules for
 the redex @{term "22 + 2"}. So we were lucky.

  following example with a nested if-then-else illustrates what can go wrong.
 ›

ML_val ‹
 {cterm "if ((2::nat) < 3) then (if ((3::nat) < 2) then 20 + 1 else 20 + 2) else 20 + 3"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "if (3::nat) < 2 then 20 + 1 else 20 + 2"}
 ›

text ‹For the a nested if-then-else we get stuck as there is no simplification rule
  for the inner if-then-else once it is at the toplevel. Note that it does not
  to specify the congproc as ∗‹weak›. The last step of the simplifier was the application
  the congruence rule. No rewrite rule is triggered for the resulting redex so the simplifier
  not revisit the term. Note that congruence rules (and congprocs) are applied only when the
  walks down the term (top-down), simplification rules (and simprocs) on the other hand
  only applied when the simplifier walks up the term (bottom-up). As the simplifier is on its
  up there is no reason to try a congruence rule on the resulting redex.
  only tries to apply simplification rules.

  congprocs should better behave canonically like ordinary congruence rules and
 preserve the head of the redex:
 ›
end

experiment
begin
declare if_weak_cong [cong del]
declare [[simproc add: if_cong, simp_trace]]

ML_val ‹
 {cterm "if ((2::nat) < 3) then (if ((3::nat) < 2) then 20 + 1 else 20 + 2) else 20 + 3"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "22"}
 ›
end

text ‹Alternatively one can supply a non standard rule if the congproc takes care of the normalisation
  the relevant subterms itself.›

lemma if_True_diy_cong: "P = True ==> x = x' ==> (if P then x else y) = x'"
  by simp

lemma if_False_diy_cong: "P = False ==> y = y' ==> (if P then x else y) = y'"
  by simp

simproc_setup passive congproc if_cong_diy (‹if x then a else b›) = ‹
 let
 val if_True_diy_cong = @{thm if_True_diy_cong [cong_format]}
 val if_False_diy_cong = @{thm if_False_diy_cong [cong_format]}
 val if_cong = @{thm if_cong [cong_format]}
 in
 (K (fn ctxt => fn ct =>
 let
 val (_, [P, x, y]) = Drule.strip_comb ct
 val P_eq = Simplifier.asm_full_rewrite ctxt P
 val rhs = Thm.dest_equals_rhs (Thm.cprop_of P_eq)
 val (rule, ts) = (case Thm.term_of rhs of
 @{term True} => (if_True_diy_cong, [x])
 | @{term False} => (if_False_diy_cong, [y])
 | _ => (if_cong, []) )
 val eqs = map (Simplifier.asm_full_rewrite ctxt) ts ― ‹explicitly simplify the subterms›
 in
 SOME (rule OF (P_eq::eqs))
 end))
 end
 ›

experiment
begin
declare if_weak_cong [cong del]
declare [[simproc add: if_cong_diy, simp_trace]]

ML_val ‹
 {cterm "if ((2::nat) < 3) then (if ((3::nat) < 2) then 20 + 1 else 20 + 2) else 20 + 3"}
 |> Simplifier.asm_full_rewrite @{context}
 |> assert @{cterm "22"}
 ›
end


subsection ‹Sketches for more meaningful congprocs›

text ‹One motivation for congprocs is the simplification of monadic terms which occur in the
  of the verification of imperative programs. We use Imperative_HOL as an example here.
  typical monadic programs we encounter lots of monadic binds and
  aka assertions. Typical assertions protect against arithmetic overflows, dangling pointers
  might encode type information for some pointers. In particular when those assertions are
  generated, e.g. by refinement proofs, there tends to be a lot of redundancy in
  assertions that are sprinkled all over the place in the program. Removing those redundant
  by simplification can be utilised by congprocs.

 ›

text ‹
  first attempt for a congruence rule to propagate an assertion through a bind is the following:
  can assume the predicate when simplifying the 'body' term‹f›:
 ›
lemma assert_bind_cong':
  "(P x = P' x) ==> (P x ==> f = f') ==> ((assert P x) ⤜ f) = ((assert P' x) ⤜ f')"
  by (auto simp add: assert_def bind_def simp add: execute_raise split: option.splits)

text ‹Unfortunately this is not a plain congruence rule that the simplifier can work with.
  problem is that congruence rules only work on the head constant of the left hand side of
 the equation in the conclusion. This is const‹bind›. But the rule is too specific as it only works
  binds where the first monadic action is an const‹assert›. Fortunately congprocs offer
  flexibility. Like simprocs they can be triggered by patterns not only the head constant.

  slightly more abstract version, generalises the parameter term‹x› for simplification of the body
 term‹f›. This also illustrates the introduction of bound variables that are passed along through
  const‹bind›.
 ›

lemma assert_bind_cong:
  "(P x = P' x) ==> (∧x. P x ==> f x = f' x) ==> ((assert P x) ⤜ f) = ((assert P' x) ⤜ f')"
  by (auto simp add: assert_def bind_def simp add: execute_raise execute_return split: option.splits)

text ‹Another typical use case is that a monadic action returns a tuple which is then propagated
  the binds. The tuple is naturally stated in 'eta expanded' form like term‹λ(x,y). f x y› such that the
  can directly refer to the bound variables term‹x› and term‹z› and not via const‹fst› and
 const‹snd›.›

lemma assert_bind_cong2':
  "(P a b = P' a b) ==> (P a b ==> f a b = f' a b) ==>
  ((assert (λ(x,y). P x y) (a,b)) ⤜ (λ(x,y). f x y)) = ((assert (λ(x,y). P' x y) (a,b)) ⤜ (λ(x,y). f' x y))"
  apply (auto simp add: assert_def bind_def simp add: execute_raise execute_return
      split: option.splits)
  done

lemma assert_bind_cong2:
  "(P a b = P' a b) ==> (∧a b. P a b ==> f a b = f' a b) ==>
  ((assert (λ(x,y). P x y) (a,b)) ⤜ (λ(x,y). f x y)) = ((assert (λ(x,y). P' x y) (a,b)) ⤜ (λ(x,y). f' x y))"
  apply (auto simp add: assert_def bind_def simp add: execute_raise execute_return
      split: option.splits)
  done

lemma assert_True_cond[simp]: "P x ==> ((assert P x) ⤜ f) = f x"
  by (auto simp add: assert_def bind_def
      simp add: execute_return execute_raise split: option.splits)

simproc_setup passive congproc assert_bind_cong (‹(assert P x) ⤜ f›) = ‹
 K (K (K (SOME @{thm assert_bind_cong [cong_format]})))
 ›

simproc_setup passive congproc assert_bind_cong2 (‹(assert P x) ⤜ f›) = ‹
 K (K (K (SOME @{thm assert_bind_cong2 [cong_format]})))
 ›

experiment
begin
declare [[simproc add: assert_bind_cong]]
text ‹The second assert is removed as expected.›
ML_val ‹
 {cterm "do {x <- assert P x; y <- assert P x; f y}"}
 |> (Simplifier.asm_full_rewrite @{context})
 |> assert_equiv @{cterm "assert P x ⤜ f"}
 ›
end

experiment fixes a::nat
begin
declare [[simproc add: assert_bind_cong]]
text ‹Does not work as expected due to issues with binding of the tuples›
ML_val ‹
 {cterm "do {(a, b) <- assert (λ(x,y). x < y) (a,b); (k,i) <- assert (λ(x,y). x < y) (a, b); return (k < i)}"}
 |> (Simplifier.asm_full_rewrite @{context})
 |> assert_equiv @{cterm "assert (λc. a < b) (a, b) ⤜
 (λx. case x of (a, b) → assert (λc. a < b) (a, b) ⤜ (λx. case x of (k, i) → return (k < i)))"}
 ›
end

experiment fixes a::nat
begin
declare [[simproc add: assert_bind_cong2]]
text ‹Works as expected. The second assert is removed and the condition is propagated to the final
 const‹return››
ML_val ‹
 {cterm "do {(a, b) <- assert (λ(x,y). x < y) (a,b); (k,i) <- assert (λ(x,y). x < y) (a, b); return (k < i)}"}
 |> (Simplifier.asm_full_rewrite @{context})
 |> assert_equiv @{cterm "assert (λ(x, y). x < y) (a, b) ⤜ (λ(x, y). return True)"}
 ›
end

text ‹To properly handle tuples in general we cold of course refine our congproc to
  the arity of the const‹bind› and then derive a variant of @{thm assert_bind_cong2} with the
  arity, 3, 4, 5... We leave this as a exercise for the reader.

 .B. For the problem of tuple-splitting there sure are other solutions, e.g. normalising the
  with @{thm case_prod_conv} or @{thm case_prod_unfold}. The drawback is that this usually
  the readability of the monadic expression. Moreover, from a performance perspective it
  usually better to split a rule like @{thm assert_bind_cong2}, which is abstract and of a fixed
  small size, compared to normalisation of an unknown user defined monadic expression which might
  quite sizeable.
 ›


subsection ‹Customizing the context in congruence rules and congprocs›

text ‹
  the simplifier works on a term it manages its context in the simpset. In
  when 'going under' an abstraction ‹λx. ...› it introduces a fresh free variable term‹x›,
  it in the body and continues. Also when going under an implication term‹P ==> C› it
  term‹P›, extracts simplification rules from term‹P› which it adds to the simpset and
  the conclusion term‹C›. This pattern is what we typically encounter in congruence rules
  @{thm assert_bind_cong2} where we have a precondition like
 term‹∧a b. P a b ==> f a b = f' a b›. This advises the simplifier to fix term‹a› and term‹b›,
  term‹P a b›, extract simplification rules from that, and continue to simplify term‹f a b›.

  congprocs we can go beyond this default behaviour of the simplifier as we are not restricted
  the format of congruence rules. In the end we have to deliver an equation but are free how we
  it. A common building block of such more refined congprocs is that we
  only want to add term‹P a b› to the simpset but want to enhance some other application specific
  with that premise, e.g. add it to a collection of named theorems or come up with some derived facts
  we want to offer some other tool (like another simproc, or solver).
  simpset already offers the possiblity to customise @{ML ‹Simplifier.mksimps›} which is a
  of type @{ML_type "Proof.context -> thm -> thm list"}. This function is used to derive equations
  a premise like term‹P a b› when it is added by the simplifier. We have extended that
  to type @{ML_type "thm -> Proof.context -> thm list * Proof.context"} to give the user the
  to do additional modifications to the context:
 {ML Simplifier.get_mksimps_context}, @{ML Simplifier.set_mksimps_context}
  following contrived example illustrates the potential usage:
 ›

definition EXTRACT :: "bool → bool" where "EXTRACT P = P"
definition UNPROTECT :: "bool → bool" where "UNPROTECT P = P"

lemma EXTRACT_TRUE_UNPROTECT_D: "EXTRACT P ≡ True ==> (UNPROTECT P ≡ True)"
  by (simp add: EXTRACT_def UNPROTECT_def)

named_theorems my_theorems

text ‹We modify @{ML Simplifier.mksimps} to derive a theorem about term‹UNPROTECT P› from
 term‹EXTRACT P› and add it to the named theorems @{thm my_theorems}.›

setup ‹
 
 fun my_mksimps old_mksimps thm ctxt =
 let
 val (thms, ctxt') = old_mksimps thm ctxt
 val thms' = map_filter (try (fn thm => @{thm EXTRACT_TRUE_UNPROTECT_D} OF [thm])) thms
 val _ = tracing ("adding: " ^ @{make_string} thms' ^ " to my_theorems")
 val ctxt'' = ctxt' |> Context.proof_map (fold (Named_Theorems.add_thm @{named_theorems my_theorems}) thms')
 in
 (thms, ctxt'' )
 end
 
 Context.theory_map (fn context =>
 let val old_mksimps = Simplifier.get_mksimps_context (Context.proof_of context)
 in context |> Simplifier.map_ss (Simplifier.set_mksimps_context (my_mksimps old_mksimps)) end)
 
 ›

text ‹We provide a simproc that matches on term‹UNPROTECT P› and tries to solve it
  rules in named theorems @{thm my_theorems}.›
simproc_setup UNPROTECT (‹UNPROTECT P›) = ‹fn _ => fn ctxt => fn ct =>
 let
 val thms = Named_Theorems.get ctxt @{named_theorems my_theorems}
 val _ = tracing ("my_theorems: " ^ @{make_string} thms)
 val eq = Simplifier.rewrite (ctxt addsimps thms) ct
 in if Thm.is_reflexive eq then NONE else SOME eq end›

lemma "EXTRACT P ==> UNPROTECT P"
  supply [[simp_trace]]
  apply (simp)
  done

text ‹Illustrate the antiquotation.›
ML ‹
  conproc1 = 🚫‹passive weak_congproc if_cong1 ("if x then a else b") =
 ‹(K (K (K (SOME @{thm if_cong [cong_format]}))))››
 ›

end