# HG changeset patch # User paulson # Date 1724245784 -3600 # Node ID 17d8b3f6d744330eabb0af85b306bff59c6d5005 # Parent 834849b5591063802d00f221551f10b8d4730758# Parent 3eda814762fc45d6725150af53580a7869e7db46 merged diff -r 3eda814762fc -r 17d8b3f6d744 Admin/cronjob/crontab.lxcisa0 --- a/Admin/cronjob/crontab.lxcisa0 Fri Aug 09 20:45:31 2024 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -SHELL=/bin/bash -MAILTO=wenzelm - -20 00 * * * $HOME/cronjob/plain_identify diff -r 3eda814762fc -r 17d8b3f6d744 Admin/cronjob/crontab.vmnipkow17 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/cronjob/crontab.vmnipkow17 Wed Aug 21 14:09:44 2024 +0100 @@ -0,0 +1,4 @@ +SHELL=/bin/bash +MAILTO=wenzelm + +20 00 * * * $HOME/cronjob/plain_identify diff -r 3eda814762fc -r 17d8b3f6d744 NEWS --- a/NEWS Fri Aug 09 20:45:31 2024 +0100 +++ b/NEWS Wed Aug 21 14:09:44 2024 +0100 @@ -7,6 +7,18 @@ New in this Isabelle version ---------------------------- +** General ** + +* The Simplifier now supports special "congprocs", using keyword +'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML +antiquotation of the same name). See also +~~/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy for further explanations +and examples. + +* The attribute "cong_format" produces the internal format of Simplifier +"cong" rules, notably for congproc implementations. + + ** HOL ** * Theory "HOL.Wellfounded": diff -r 3eda814762fc -r 17d8b3f6d744 src/Benchmarks/Record_Benchmark/Record_Benchmark.thy --- a/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Fri Aug 09 20:45:31 2024 +0100 +++ b/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Wed Aug 21 14:09:44 2024 +0100 @@ -356,12 +356,12 @@ lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" apply (tactic \simp_tac - (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.upd_simproc]) 1\) + (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc Record.upd_simproc) 1\) done lemma "(\r. P (A155 r)) \ (\x. P x)" apply (tactic \simp_tac - (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\) + (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\) apply simp done @@ -372,7 +372,7 @@ lemma "(\r. P (A155 r)) \ (\x. P x)" apply (tactic \simp_tac - (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\) + (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\) apply simp done @@ -383,7 +383,7 @@ lemma "\r. P (A155 r) \ (\x. P x)" apply (tactic \simp_tac - (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\) + (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\) apply auto done @@ -417,7 +417,7 @@ lemma "\r. A155 r = x" apply (tactic \simp_tac - (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.ex_sel_eq_simproc]) 1\) + (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.ex_sel_eq_simproc)) 1\) done print_record many_A diff -r 3eda814762fc -r 17d8b3f6d744 src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Fri Aug 09 20:45:31 2024 +0100 +++ b/src/Doc/Isar_Ref/Generic.thy Wed Aug 21 14:09:44 2024 +0100 @@ -803,12 +803,14 @@ \end{matharray} \<^rail>\ - @{syntax_def simproc_setup}: (@'passive')? @{syntax name} + @{syntax_def simproc_setup}: (@'passive')? proc_kind? @{syntax name} patterns '=' @{syntax embedded} ; @{syntax_def simproc_setup_id}: @{syntax simproc_setup} (@'identifier' @{syntax thms})? ; + proc_kind: @'congproc' | @'weak_congproc' + ; patterns: '(' (@{syntax term} + '|') ')' ; @@{command simproc_setup} @{syntax simproc_setup} @@ -836,6 +838,11 @@ thus \<^emph>\active\. The keyword \<^theory_text>\passive\ avoids that: it merely defines a simproc that can be activated in a different context later on. + Regular simprocs produce rewrite rules on the fly, but it is also possible + to congruence rules via the @{syntax proc_kind} keywords: \<^theory_text>\congproc\ or + \<^theory_text>\weak_congproc\. See also \<^file>\~~/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy\ + for further explanations and examples. + \<^descr> ML antiquotation @{ML_antiquotation_ref simproc_setup} is like command @{command simproc_setup}, with slightly extended syntax following @{syntax simproc_setup_id}. It allows to introduce a new simproc conveniently within diff -r 3eda814762fc -r 17d8b3f6d744 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Fri Aug 09 20:45:31 2024 +0100 +++ b/src/FOL/FOL.thy Wed Aug 21 14:09:44 2024 +0100 @@ -346,7 +346,8 @@ val IFOL_ss = put_simpset FOL_basic_ss \<^context> addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all} - addsimprocs [\<^simproc>\defined_All\, \<^simproc>\defined_Ex\] + |> Simplifier.add_proc \<^simproc>\defined_All\ + |> Simplifier.add_proc \<^simproc>\defined_Ex\ |> Simplifier.add_cong @{thm imp_cong} |> simpset_of; diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Aug 21 14:09:44 2024 +0100 @@ -53,7 +53,8 @@ div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1} addsimps @{thms ac_simps} - addsimprocs [\<^simproc>\cancel_div_mod_nat\, \<^simproc>\cancel_div_mod_int\] + |> Simplifier.add_proc \<^simproc>\cancel_div_mod_nat\ + |> Simplifier.add_proc \<^simproc>\cancel_div_mod_int\ val simpset0 = put_simpset HOL_basic_ss ctxt addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms} diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/Decision_Procs/langford.ML Wed Aug 21 14:09:44 2024 +0100 @@ -176,7 +176,7 @@ let val ctxt' = Context_Position.set_visible false (put_simpset dlo_ss ctxt) - addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc] + addsimps @{thms dnf_simps} |> Simplifier.add_proc reduce_ex_simproc val dnfex_conv = Simplifier.rewrite ctxt' val pcv = Simplifier.rewrite diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 21 14:09:44 2024 +0100 @@ -68,14 +68,16 @@ (* Transform the term*) val (t,np,nh) = prepare_for_mir q g (* Some simpsets for dealing with mod div abs and nat*) - val mod_div_simpset = put_simpset HOL_basic_ss ctxt - addsimps [refl, @{thm mod_add_eq}, - @{thm mod_self}, - @{thm div_0}, @{thm mod_0}, - @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0}, - @{thm "Suc_eq_plus1"}] - addsimps @{thms add.assoc add.commute add.left_commute} - addsimprocs [\<^simproc>\cancel_div_mod_nat\, \<^simproc>\cancel_div_mod_int\] + val mod_div_simpset = + put_simpset HOL_basic_ss ctxt + addsimps [refl, @{thm mod_add_eq}, + @{thm mod_self}, + @{thm div_0}, @{thm mod_0}, + @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0}, + @{thm "Suc_eq_plus1"}] + addsimps @{thms add.assoc add.commute add.left_commute} + |> Simplifier.add_proc \<^simproc>\cancel_div_mod_nat\ + |> Simplifier.add_proc \<^simproc>\cancel_div_mod_int\ val simpset0 = put_simpset HOL_basic_ss ctxt addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1} addsimps comp_ths diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/Eisbach/match_method.ML Wed Aug 21 14:09:44 2024 +0100 @@ -480,7 +480,7 @@ val tenv = Envir.term_env env; val tyenv = Envir.type_env env; in - forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv) + Vartab.forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) tenv end; fun term_eq_wrt (env1, env2) (t1, t2) = diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/Examples/Records.thy --- a/src/HOL/Examples/Records.thy Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/Examples/Records.thy Wed Aug 21 14:09:44 2024 +0100 @@ -244,7 +244,7 @@ lemma "(\r. P (xpos r)) \ (\x. P x)" apply (tactic \simp_tac (put_simpset HOL_basic_ss \<^context> - addsimprocs [Record.split_simproc (K ~1)]) 1\) + |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\) apply simp done @@ -255,7 +255,7 @@ lemma "(\r. P (xpos r)) \ (\x. P x)" apply (tactic \simp_tac (put_simpset HOL_basic_ss \<^context> - addsimprocs [Record.split_simproc (K ~1)]) 1\) + |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\) apply simp done @@ -266,7 +266,7 @@ lemma "\r. P (xpos r) \ (\x. P x)" apply (tactic \simp_tac (put_simpset HOL_basic_ss \<^context> - addsimprocs [Record.split_simproc (K ~1)]) 1\) + |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\) apply auto done diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/HOL.thy Wed Aug 21 14:09:44 2024 +0100 @@ -1567,11 +1567,12 @@ | _ => NONE)\ declaration \ - K (Induct.map_simpset (fn ss => ss - addsimprocs [\<^simproc>\swap_induct_false\, \<^simproc>\induct_equal_conj_curry\] - |> Simplifier.set_mksimps (fn ctxt => - Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> - map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))) + K (Induct.map_simpset + (Simplifier.add_proc \<^simproc>\swap_induct_false\ #> + Simplifier.add_proc \<^simproc>\induct_equal_conj_curry\ #> + Simplifier.set_mksimps (fn ctxt => + Simpdata.mksimps Simpdata.mksimps_pairs ctxt #> + map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))) \ text \Pre-simplification of induction and cases rules\ @@ -1942,7 +1943,7 @@ \<^Const_>\HOL.eq T\ => if is_Type T then SOME @{thm eq_equal} else NONE | _ => NONE)\ -setup \Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\equal\])\ +setup \Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\equal\)\ subsubsection \Generic code generator foundation\ diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Aug 21 14:09:44 2024 +0100 @@ -35,7 +35,7 @@ val beta_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms simp_thms} addsimprocs [\<^simproc>\beta_cfun_proc\]) + addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\beta_cfun_proc\) fun is_cpo thy T = Sign.of_sort thy (T, \<^sort>\cpo\) diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Aug 21 14:09:44 2024 +0100 @@ -108,7 +108,7 @@ val beta_ss = simpset_of (put_simpset HOL_basic_ss \<^context> - addsimps @{thms simp_thms} addsimprocs [\<^simproc>\beta_cfun_proc\]) + addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\beta_cfun_proc\) (******************************************************************************) (******************************** theory data *********************************) diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Fri Aug 09 20:45:31 2024 +0100 +++ b/src/HOL/Hoare/hoare_tac.ML Wed Aug 21 14:09:44 2024 +0100 @@ -157,7 +157,7 @@ fun basic_simp_tac ctxt var_names tac = simp_tac (put_simpset HOL_basic_ss ctxt - addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc]) + addsimps [mem_Collect_eq, @{thm split_conv}] |> Simplifier.add_proc Record.simproc) THEN_MAYBE' max_simp_tac ctxt var_names tac; diff -r 3eda814762fc -r 17d8b3f6d744 src/HOL/Imperative_HOL/ex/Congproc_Ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy Wed Aug 21 14:09:44 2024 +0100 @@ -0,0 +1,529 @@ +(* 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 +descends into the subterms to normalise those and then works its way up to the head of the term +trying to apply rewrite rules for the current redex (reducible expression) it encounters on the +way up. Descending into the term can be influenced by congruence rules. Before descending into the +subterms the simplifier checks for a congruence rule for the head of the term. If it finds one +it behaves according to that rule, otherwise the simplifier descends into each subterm subsequently. + +While rewrite rules can be complemented with simplification procedures (simprocs) to get even +more programmatic control, congruence rules can be complemented with congruence +procedures (congprocs): + +\<^item> 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"} +\<^item> 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. +\<^item> Congprocs have precedence over congruence rules (unlike simprocs) +\<^item> 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. +\<^item> 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 \ +fun assert expected eq = if (expected aconvc (Thm.rhs_of eq)) then eq else + raise error ("unexpected: " ^ @{make_string} eq) + +fun 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 +rule 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. +As 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. +As the simplifier analyses congruence rules this rule is classified as weak. Whenever a +redex 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 +congproc. To achieve the same result we can explicitly specify it as \<^emph>\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}. +It first simplifies the condition and depending on the result decides to either simplify only +one of the branches (in case the condition evaluates to \<^term>\True\ or \<^term>\False\, or otherwise +it 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 \<^emph>\weak\ as every relevant subterm is +simplified.\ +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: +\<^enum> First condition is simplified to True +\<^enum> Congruence rule is selected and then "then-branch" is simplified but "else-branch" is left untouched +\<^enum> Congruence step is finished and now rewriting with @{thm if_True} is done. +Note 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\ +we can observe some odd congruence behaviour: +\<^enum> First condition is simplified to True +\<^enum> 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" +\<^enum> Incidently simplification continues on the then-branch as there are simplification rules for + the redex @{term "22 + 2"}. So we were lucky. + +The 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 +triggering for the inner if-then-else once it is at the toplevel. Note that it does not +help to specify the congproc as \<^emph>\weak\. The last step of the simplifier was the application +of the congruence rule. No rewrite rule is triggered for the resulting redex so the simplifier +does not revisit the term. Note that congruence rules (and congprocs) are applied only when the +simplifier walks down the term (top-down), simplification rules (and simprocs) on the other hand +are only applied when the simplifier walks up the term (bottom-up). As the simplifier is on its +way up there is no reason to try a congruence rule on the resulting redex. +It only tries to apply simplification rules. + +So 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 +of 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 +context of the verification of imperative programs. We use Imperative_HOL as an example here. +In typical monadic programs we encounter lots of monadic binds and +guards aka assertions. Typical assertions protect against arithmetic overflows, dangling pointers +or might encode type information for some pointers. In particular when those assertions are +mechanically generated, e.g. by refinement proofs, there tends to be a lot of redundancy in +the assertions that are sprinkled all over the place in the program. Removing those redundant +guards by simplification can be utilised by congprocs. + +\ + +text \ +A first attempt for a congruence rule to propagate an assertion through a bind is the following: +We 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. +The 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 +for binds where the first monadic action is an \<^const>\assert\. Fortunately congprocs offer +that flexibility. Like simprocs they can be triggered by patterns not only the head constant. + +A 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 +the \<^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 +through the binds. The tuple is naturally stated in 'eta expanded' form like \<^term>\$x,y). f x y\ such that the +body 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 +analyse the arity of the \<^const>\bind\ and then derive a variant of @{thm assert_bind_cong2} with the +corresponding arity, 3, 4, 5... We leave this as a exercise for the reader. + +N.B. For the problem of tuple-splitting there sure are other solutions, e.g. normalising the +program with @{thm case_prod_conv} or @{thm case_prod_unfold}. The drawback is that this usually +diminishes the readability of the monadic expression. Moreover, from a performance perspective it +is usually better to split a rule like @{thm assert_bind_cong2}, which is abstract and of a fixed +known small size, compared to normalisation of an unknown user defined monadic expression which might +be quite sizeable. +\ + + +subsection \Customizing the context in congruence rules and congprocs\ + +text \ +When the simplifier works on a term it manages its context in the simpset. In +particular when 'going under' an abstraction \\x. ...\ it introduces a fresh free variable \<^term>\x\, +substitutes it in the body and continues. Also when going under an implication \<^term>\P \ C\ it +assumes \<^term>\P\, extracts simplification rules from \<^term>\P\ which it adds to the simpset and +simplifies the conclusion \<^term>\C\. This pattern is what we typically encounter in congruence rules +like @{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\, +assume \<^term>\P a b\, extract simplification rules from that, and continue to simplify \<^term>\f a b\. + +With congprocs we can go beyond this default behaviour of the simplifier as we are not restricted +to the format of congruence rules. In the end we have to deliver an equation but are free how we +derive it. A common building block of such more refined congprocs is that we +not only want to add \<^term>\P a b\ to the simpset but want to enhance some other application specific +data with that premise, e.g. add it to a collection of named theorems or come up with some derived facts +that we want to offer some other tool (like another simproc, or solver). +The simpset already offers the possiblity to customise @{ML \Simplifier.mksimps\} which is a +function of type @{ML_type "Proof.context -> thm -> thm list"}. This function is used to derive equations +from a premise like \<^term>\P a b\ when it is added by the simplifier. We have extended that +function to type @{ML_type "thm -> Proof.context -> thm list * Proof.context"} to give the user the +control to do additional modifications to the context: +@{ML Simplifier.get_mksimps_context}, @{ML Simplifier.set_mksimps_context} +The 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 \