# HG changeset patch # User wenzelm # Date 1723722429 -7200 # Node ID 055ac404d48deb736c4c5be75bf7066f43c94b26 # Parent 43e0f32451ee18e98ee00e06d5d4af54a4c52471 original Congproc_Ex.thy by Norbert Schirmer: still inactive; diff -r 43e0f32451ee -r 055ac404d48d 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 Thu Aug 15 13:47:09 2024 +0200 @@ -0,0 +1,536 @@ +(* Title: HOL/Imperative_HOL/ex/Congproc.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}\ +congproc_setup passive if_cong (\if x then a else b\) = \ + (K (K (K (SOME (Simpdata.mk_meta_cong @{context} @{thm if_cong}))))) +\ + +experiment +begin +text \The congproc takes precedence over the cong rules\ +declare [[congproc 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.\ + +congproc_setup passive if_weak_cong_bad (\if x then a else b\) = \ + (K (K (K (SOME (Simpdata.mk_meta_cong @{context} @{thm if_weak_cong}))))) +\ + +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 [[congproc 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 + +congproc_setup passive weak if_weak_cong (\if x then a else b\) = \ + (K (K (K (SOME (Simpdata.mk_meta_cong @{context} @{thm if_weak_cong}))))) +\ + +experiment +begin +declare if_weak_cong [cong del] +declare [[congproc 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.\ +congproc_setup passive if_cong_canonical (\if x then a else b\) = \ + let + val if_True_weak_cong = Simpdata.mk_meta_cong @{context} @{thm if_True_weak_cong} + val if_False_weak_cong = Simpdata.mk_meta_cong @{context} @{thm if_False_weak_cong} + val if_cong = Simpdata.mk_meta_cong @{context} @{thm if_cong} + 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 [[congproc 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 [[congproc 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 [[congproc 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 + +congproc_setup passive if_cong_bad (\if x then a else b\) = \ + let + val if_True_cong = Simpdata.mk_meta_cong @{context} @{thm if_True_cong} + val if_False_cong = Simpdata.mk_meta_cong @{context} @{thm if_False_cong} + val if_cong = Simpdata.mk_meta_cong @{context} @{thm if_cong} + 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 [[congproc 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 [[congproc 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 + +congproc_setup passive if_cong_diy (\if x then a else b\) = \ + let + val if_True_diy_cong = Simpdata.mk_meta_cong @{context} @{thm if_True_diy_cong} + val if_False_diy_cong = Simpdata.mk_meta_cong @{context} @{thm if_False_diy_cong} + val if_cong = Simpdata.mk_meta_cong @{context} @{thm if_cong} + 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 [[congproc 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) + + + +congproc_setup passive assert_bind_cong (\(assert P x) \ f\) = \ + K (K (K (SOME (Simpdata.mk_meta_cong @{context} @{thm assert_bind_cong})))) +\ + +congproc_setup passive assert_bind_cong2 (\(assert P x) \ f\) = \ + K (K (K (SOME (Simpdata.mk_meta_cong @{context} @{thm assert_bind_cong2})))) +\ + +experiment +begin +declare [[congproc 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 [[congproc 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 [[congproc 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 "Proof.context -> thm -> (thm list * Proof.context)"} to give the user the +control to do additional modifications to the context: +@{ML Simplifier.context_mksimps}, @{ML Simplifier.map_context_mksimps} +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 \ True \ (UNPROTECT P \ True)" + by (simp add: EXTRACT_def UNPROTECT_def) + + +named_theorems my_theorems + +text \We modify @{ML Simplifier.context_mksimps} to derive a theorem about \<^term>\UNPROTECT P\ from + \<^term>\EXTRACT P\ and add it to the named theorems @{thm my_theorems}.\ + +setup \ +let + fun my_mk mk ctxt thm = + let + val (thms, ctxt') = mk ctxt thm + 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 +in + Context.theory_map (Simplifier.map_ss (Simplifier.map_context_mksimps my_mk)) +end +\ + +text \We provide a simproc that matches on \<^term>\UNPROTECT P\ and tries to solve it +with 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 \ +val conproc1 = \<^congproc_setup>\passive weak if_cong1 ("if x then a else b") = + \(K (K (K (SOME (Simpdata.mk_meta_cong @{context} @{thm if_cong})))))\\ + +\ + + + + +end