cai (Jan 05 2024 at 17:30): cai (Jan 05 2024 at 17:30):What is the low-level way of replacing cterm with cterm in a goal? Suppose:
lemma
fixes P Q :: "nat ⇒ bool" and f g :: "nat ⇒ nat" and n :: nat
shows "Q (f (g n)) ⟹ P (g n)"
proof -
obtain x where x: "x = g n" by simp
show "Q (f (g n)) ⟹ P (g n)" ― ‹1›
apply (unfold atomize_imp)
apply (subst arg_cong[OF x, symmetric, of "λx. Q (f x) ⟶ P x"])
apply (fold atomize_imp) ― ‹2›
oops
The goal (1) contains several occurences of "g n" (in assumptions too which requires moving from imp to implies and back) which I want to replace to simplify the goal (2).
The cterms (eg. "g n") are known and I'm looking for the simplest way to achieve above in low-level ML. Preferrably, I don't have to define new terms but more importantly I'd prefer the goal not to include old bound variables.
So not from "⋀n. Q (f (g n)) ⟹ P (g n)" to "⋀n x. Q (f x) ⟹ P x" but rather "⋀x. Q (f x) ⟹ P x".
Jan van Brügge (Jan 05 2024 at 21:52):You can get rid of the extra bound var with unfold triv_forall_equality
Jan van Brügge (Jan 05 2024 at 21:52):and to replace I think subst or subst (asm) is probably the easiest
Last updated: May 04 2024 at 16:18 UTC